set g = the Grothendieck of X;

defpred S_{1}[ set ] means $1 is Grothendieck of X;

consider Gclasses being set such that

A1: for Y being set holds

( Y in Gclasses iff ( Y in bool the Grothendieck of X & S_{1}[Y] ) )
from XFAMILY:sch 1();

A2: the Grothendieck of X in bool the Grothendieck of X by ZFMISC_1:def 1;

then reconsider Gclasses = Gclasses as non empty set by A1;

set M = meet Gclasses;

A3: meet Gclasses is epsilon-transitive

M is Grothendieck of X

take M ; :: thesis: for G being Grothendieck of X holds M c= G

let G1 be Grothendieck of X; :: thesis: M c= G1

A10: M /\ G1 is Grothendieck of X by Th1;

( M /\ G1 c= M & M c= the Grothendieck of X ) by SETFAM_1:3, A2, A1, XBOOLE_1:17;

then A11: ( M /\ G1 c= the Grothendieck of X & M /\ G1 c= G1 ) by XBOOLE_1:17;

then M c= M /\ G1 by A10, A1, SETFAM_1:3;

hence M c= G1 by A11; :: thesis: verum

defpred S

consider Gclasses being set such that

A1: for Y being set holds

( Y in Gclasses iff ( Y in bool the Grothendieck of X & S

A2: the Grothendieck of X in bool the Grothendieck of X by ZFMISC_1:def 1;

then reconsider Gclasses = Gclasses as non empty set by A1;

set M = meet Gclasses;

A3: meet Gclasses is epsilon-transitive

proof

A5:
meet Gclasses is power-closed
let Y be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Y in meet Gclasses or Y c= meet Gclasses )

assume A4: Y in meet Gclasses ; :: thesis: Y c= meet Gclasses

for Z being set st Z in Gclasses holds

Y c= Z

end;assume A4: Y in meet Gclasses ; :: thesis: Y c= meet Gclasses

for Z being set st Z in Gclasses holds

Y c= Z

proof

hence
Y c= meet Gclasses
by SETFAM_1:5; :: thesis: verum
let Z be set ; :: thesis: ( Z in Gclasses implies Y c= Z )

assume Z in Gclasses ; :: thesis: Y c= Z

then ( Y in Z & Z is epsilon-transitive ) by SETFAM_1:def 1, A4, A1;

hence Y c= Z ; :: thesis: verum

end;assume Z in Gclasses ; :: thesis: Y c= Z

then ( Y in Z & Z is epsilon-transitive ) by SETFAM_1:def 1, A4, A1;

hence Y c= Z ; :: thesis: verum

proof

meet Gclasses is FamUnion-closed
let Z be set ; :: according to CLASSES3:def 1 :: thesis: ( Z in meet Gclasses implies bool Z in meet Gclasses )

assume A6: Z in meet Gclasses ; :: thesis: bool Z in meet Gclasses

for Y being set st Y in Gclasses holds

bool Z in Y

end;assume A6: Z in meet Gclasses ; :: thesis: bool Z in meet Gclasses

for Y being set st Y in Gclasses holds

bool Z in Y

proof

hence
bool Z in meet Gclasses
by SETFAM_1:def 1; :: thesis: verum
let Y be set ; :: thesis: ( Y in Gclasses implies bool Z in Y )

assume Y in Gclasses ; :: thesis: bool Z in Y

then ( Z in Y & Y is power-closed ) by A1, A6, SETFAM_1:def 1;

hence bool Z in Y ; :: thesis: verum

end;assume Y in Gclasses ; :: thesis: bool Z in Y

then ( Z in Y & Y is power-closed ) by A1, A6, SETFAM_1:def 1;

hence bool Z in Y ; :: thesis: verum

proof

then reconsider M = meet Gclasses as Grothendieck by A3, A5;
let Z be set ; :: according to CLASSES3:def 3 :: thesis: for f being Function st dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses holds

union (rng f) in meet Gclasses

let f be Function; :: thesis: ( dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses implies union (rng f) in meet Gclasses )

assume A7: ( dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses ) ; :: thesis: union (rng f) in meet Gclasses

for Y being set st Y in Gclasses holds

union (rng f) in Y

end;union (rng f) in meet Gclasses

let f be Function; :: thesis: ( dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses implies union (rng f) in meet Gclasses )

assume A7: ( dom f = Z & rng f c= meet Gclasses & Z in meet Gclasses ) ; :: thesis: union (rng f) in meet Gclasses

for Y being set st Y in Gclasses holds

union (rng f) in Y

proof

hence
union (rng f) in meet Gclasses
by SETFAM_1:def 1; :: thesis: verum
let Y be set ; :: thesis: ( Y in Gclasses implies union (rng f) in Y )

assume A8: Y in Gclasses ; :: thesis: union (rng f) in Y

A9: ( Z in Y & Y is FamUnion-closed ) by A8, A1, A7, SETFAM_1:def 1;

( rng f c= meet Gclasses & meet Gclasses c= Y ) by A8, A7, SETFAM_1:7;

then rng f c= Y ;

hence union (rng f) in Y by A7, A9; :: thesis: verum

end;assume A8: Y in Gclasses ; :: thesis: union (rng f) in Y

A9: ( Z in Y & Y is FamUnion-closed ) by A8, A1, A7, SETFAM_1:def 1;

( rng f c= meet Gclasses & meet Gclasses c= Y ) by A8, A7, SETFAM_1:7;

then rng f c= Y ;

hence union (rng f) in Y by A7, A9; :: thesis: verum

M is Grothendieck of X

proof

end;

then reconsider M = M as Grothendieck of X ;now :: thesis: for Y being set st Y in Gclasses holds

X in Y

hence
X in M
by SETFAM_1:def 1; :: according to CLASSES3:def 4 :: thesis: verumX in Y

let Y be set ; :: thesis: ( Y in Gclasses implies X in Y )

assume Y in Gclasses ; :: thesis: X in Y

then Y is Grothendieck of X by A1;

hence X in Y by Def4; :: thesis: verum

end;assume Y in Gclasses ; :: thesis: X in Y

then Y is Grothendieck of X by A1;

hence X in Y by Def4; :: thesis: verum

take M ; :: thesis: for G being Grothendieck of X holds M c= G

let G1 be Grothendieck of X; :: thesis: M c= G1

A10: M /\ G1 is Grothendieck of X by Th1;

( M /\ G1 c= M & M c= the Grothendieck of X ) by SETFAM_1:3, A2, A1, XBOOLE_1:17;

then A11: ( M /\ G1 c= the Grothendieck of X & M /\ G1 c= G1 ) by XBOOLE_1:17;

then M c= M /\ G1 by A10, A1, SETFAM_1:3;

hence M c= G1 by A11; :: thesis: verum