consider Big being set such that
A1:
A in Big
and
A2:
for X, Y being set st X in Big & Y c= X holds
Y in Big
and
A3:
( ( for X being set st X in Big holds
bool X in Big ) & ( for X being set holds
( not X c= Big or X,Big are_equipotent or X in Big ) ) )
by ZFMISC_1:112;
A4:
Big is Tarski
by A3, A2, Def1;
defpred S1[ set ] means $1 is_Tarski-Class_of A;
consider Classes being set such that
A5:
for X being set holds
( X in Classes iff ( X in bool Big & S1[X] ) )
from XFAMILY:sch 1();
set IT = meet Classes;
A6:
( Big in bool Big & Big is_Tarski-Class_of A )
by A1, A4, ZFMISC_1:def 1;
then A7:
Big in Classes
by A5;
A8:
Classes <> {}
by A5, A6;
A9:
now for X being set st X in Classes holds
A in Xend;
then A10:
A in meet Classes
by A8, SETFAM_1:def 1;
take
meet Classes
; ( meet Classes is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus
A in meet Classes
by A8, A9, SETFAM_1:def 1; CLASSES1:def 3 ( meet Classes is Tarski & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus A11:
for X, Y being set st X in meet Classes & Y c= X holds
Y in meet Classes
CLASSES1:def 1,CLASSES1:def 2 ( ( for X being set st X in meet Classes holds
bool X in meet Classes ) & ( for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ) & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus A16:
for X being set st X in meet Classes holds
bool X in meet Classes
( ( for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ) & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus A20:
for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes )
for D being set st D is_Tarski-Class_of A holds
meet Classes c= D
let D be set ; ( D is_Tarski-Class_of A implies meet Classes c= D )
assume A26:
D is_Tarski-Class_of A
; meet Classes c= D
then A27:
A in D
;
A28:
D is Tarski
by A26;
then A29:
D is subset-closed
;
A30:
(meet Classes) /\ D is_Tarski-Class_of A
proof
thus
A in (meet Classes) /\ D
by A10, A27, XBOOLE_0:def 4;
CLASSES1:def 3 (meet Classes) /\ D is Tarski
thus
for
X,
Y being
set st
X in (meet Classes) /\ D &
Y c= X holds
Y in (meet Classes) /\ D
CLASSES1:def 1,
CLASSES1:def 2 ( ( for X being set st X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D ) & ( for X being set holds
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D ) ) )
thus
for
X being
set st
X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D
for X being set holds
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D )
let X be
set ;
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D )
assume that A40:
X c= (meet Classes) /\ D
and A41:
not
X,
(meet Classes) /\ D are_equipotent
;
X in (meet Classes) /\ D
A42:
(meet Classes) /\ D c= meet Classes
by XBOOLE_1:17;
A43:
(meet Classes) /\ D c= D
by XBOOLE_1:17;
A44:
not
X,
meet Classes are_equipotent
by A40, A41, A42, CARD_1:24;
A45:
(
X c= D & not
X,
D are_equipotent )
by A40, A41, A43, CARD_1:24;
A46:
X in meet Classes
by A20, A40, A42, A44, XBOOLE_1:1;
X in D
by A28, A45;
hence
X in (meet Classes) /\ D
by A46, XBOOLE_0:def 4;
verum
end;
(meet Classes) /\ D c= Big
then A47:
meet Classes c= (meet Classes) /\ D
by SETFAM_1:3, A5, A30;
(meet Classes) /\ D c= D
by XBOOLE_1:17;
hence
meet Classes c= D
by A47; verum