let X, Y be non empty TopSpace; :: thesis: for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
let F be Subset-Family of X; :: thesis: for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
let H be Subset-Family of [:X,Y:]; :: thesis: ( F is finite & F c= (Pr1 (X,Y)) .: H implies ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G ) )
assume that
A1: F is finite and
A2: F c= (Pr1 (X,Y)) .: H ; :: thesis: ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
defpred S1[ object , object ] means ( $2 in dom (Pr1 (X,Y)) & $2 in H & $1 = (Pr1 (X,Y)) . $2 );
A3: for e being object st e in F holds
ex u being object st S1[e,u] by A2, FUNCT_1:def 6;
consider f being Function such that
A4: dom f = F and
A5: for e being object st e in F holds
S1[e,f . e] from CLASSES1:sch 1(A3);
 A6: f .: F c= H
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in f .: F or e in H )
assume e in f .: F ; :: thesis: e in H
then ex u being object st
( u in dom f & u in F & e = f . u ) by FUNCT_1:def 6;
hence e in H by A5; :: thesis: verum
end;
then reconsider G = f .: F as Subset-Family of [:X,Y:] by XBOOLE_1:1;
take G ; :: thesis: ( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )
thus G c= H by A6; :: thesis: ( G is finite & F = (Pr1 (X,Y)) .: G )
thus G is finite by A1; :: thesis: F = (Pr1 (X,Y)) .: G
now :: thesis: for e being object holds
( e in F iff ex u being object st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )
let e be object ; :: thesis: ( e in F iff ex u being object st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) )
thus ( e in F iff ex u being object st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) :: thesis: verum
proof
thus ( e in F implies ex u being object st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) ) :: thesis: ( ex u being object st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u ) implies e in F )
proof
assume A7: e in F ; :: thesis: ex u being object st
( u in dom (Pr1 (X,Y)) & u in G & e = (Pr1 (X,Y)) . u )
take f . e ; :: thesis: ( f . e in dom (Pr1 (X,Y)) & f . e in G & e = (Pr1 (X,Y)) . (f . e) )
thus f . e in dom (Pr1 (X,Y)) by A5, A7; :: thesis: ( f . e in G & e = (Pr1 (X,Y)) . (f . e) )
thus f . e in G by A4, A7, FUNCT_1:def 6; :: thesis: e = (Pr1 (X,Y)) . (f . e)
thus e = (Pr1 (X,Y)) . (f . e) by A5, A7; :: thesis: verum
end;
given u being object such that u in dom (Pr1 (X,Y)) and
A8: u in G and
A9: e = (Pr1 (X,Y)) . u ; :: thesis: e in F
ex v being object st
( v in dom f & v in F & u = f . v ) by A8, FUNCT_1:def 6;
hence e in F by A5, A9; :: thesis: verum
end;
end;
hence F = (Pr1 (X,Y)) .: G by FUNCT_1:def 6; :: thesis: verum