set F = { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ;
take D = meet { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ; :: thesis: ( A c= D & ( for x, y being set st [x,y] in D holds
x c= D ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
D c= B ) )
A3: A c= Rank (the_rank_of A) by CLASSES1:def 9;
A4: now :: thesis: for x, y being set st [x,y] in Rank (the_rank_of A) holds
x c= Rank (the_rank_of A)
let x, y be set ; :: thesis: ( [x,y] in Rank (the_rank_of A) implies x c= Rank (the_rank_of A) )
assume A5: [x,y] in Rank (the_rank_of A) ; :: thesis: x c= Rank (the_rank_of A)
A6: {x} in {{x,y},{x}} by TARSKI:def 2;
A7: {{x,y},{x}} c= Rank (the_rank_of A) by A5, ORDINAL1:def 2;
A8: x in {x} by TARSKI:def 1;
{x} c= Rank (the_rank_of A) by A6, A7, ORDINAL1:def 2;
hence x c= Rank (the_rank_of A) by A8, ORDINAL1:def 2; :: thesis: verum
end;
Rank (the_rank_of A) c= Rank (the_rank_of A) ;
then A9: Rank (the_rank_of A) in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } by A3, A4;
hereby :: according to TARSKI:def 3 :: thesis: ( ( for x, y being set st [x,y] in D holds
x c= D ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
D c= B ) )
let x be object ; :: thesis: ( x in A implies x in D )
assume A10: x in A ; :: thesis: x in D
now :: thesis: for C being set st C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } holds
x in C
let C be set ; :: thesis: ( C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } implies x in C )
assume C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ; :: thesis: x in C
then ex B being Subset of (Rank (the_rank_of A)) st
( C = B & A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) ) ;
hence x in C by A10; :: thesis: verum
end;
hence x in D by A9, SETFAM_1:def 1; :: thesis: verum
end;
hereby :: thesis: for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
D c= B
let x, y be set ; :: thesis: ( [x,y] in D implies x c= D )
assume A11: [x,y] in D ; :: thesis: x c= D
thus x c= D :: thesis: verum
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in D )
assume A12: z in x ; :: thesis: z in D
now :: thesis: for X being set st X in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } holds
z in X
let X be set ; :: thesis: ( X in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } implies z in X )
assume A13: X in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ; :: thesis: z in X
then A14: [x,y] in X by A11, SETFAM_1:def 1;
ex B being Subset of (Rank (the_rank_of A)) st
( X = B & A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) ) by A13;
then x c= X by A14;
hence z in X by A12; :: thesis: verum
end;
hence z in D by A9, SETFAM_1:def 1; :: thesis: verum
end;
end;
let B be set ; :: thesis: ( A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) implies D c= B )
assume that
A15: A c= B and
A16: for x, y being set st [x,y] in B holds
x c= B ; :: thesis: D c= B
set C = B /\ (Rank (the_rank_of A));
reconsider C = B /\ (Rank (the_rank_of A)) as Subset of (Rank (the_rank_of A)) by XBOOLE_1:17;
A17: A c= C by A3, A15, XBOOLE_1:19;
now :: thesis: for x, y being set st [x,y] in C holds
x c= C
let x, y be set ; :: thesis: ( [x,y] in C implies x c= C )
assume A18: [x,y] in C ; :: thesis: x c= C
then [x,y] in B by XBOOLE_0:def 4;
then A19: x c= B by A16;
x c= Rank (the_rank_of A) by A4, A18;
hence x c= C by A19, XBOOLE_1:19; :: thesis: verum
end;
then C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } by A17;
then A20: D c= C by SETFAM_1:3;
C c= B by XBOOLE_1:17;
hence D c= B by A20; :: thesis: verum