:: XBOOLE_0 semantic presentation begin scheme :: XBOOLE_0:sch 1 Separation{ F1() -> set , P1[ set ] } : ex X being set st for x being set holds ( x in X iff ( x in F1() & P1[x] ) ) proof defpred S1[ set , set ] means ( \$1 = \$2 & P1[\$2] ); A1: for x, y, z being set st S1[x,y] & S1[x,z] holds y = z ; consider X being set such that A2: for x being set holds ( x in X iff ex y being set st ( y in F1() & S1[y,x] ) ) from TARSKI:sch_1(A1); take X ; ::_thesis: for x being set holds ( x in X iff ( x in F1() & P1[x] ) ) let x be set ; ::_thesis: ( x in X iff ( x in F1() & P1[x] ) ) ( x in X iff ex y being set st ( y in F1() & y = x & P1[x] ) ) by A2; hence ( x in X iff ( x in F1() & P1[x] ) ) ; ::_thesis: verum end; definition let X be set ; attrX is empty means :Def1: :: XBOOLE_0:def 1 for x being set holds not x in X; end; :: deftheorem Def1 defines empty XBOOLE_0:def_1_:_ for X being set holds ( X is empty iff for x being set holds not x in X ); registration cluster empty for set ; existence ex b1 being set st b1 is empty proof defpred S1[ set ] means contradiction; consider Y being set such that A1: for x being set holds ( x in Y iff ( x in the set & S1[x] ) ) from XBOOLE_0:sch_1(); take Y ; ::_thesis: Y is empty thus for x being set holds not x in Y by A1; :: according to XBOOLE_0:def_1 ::_thesis: verum end; end; definition func {} -> set equals :: XBOOLE_0:def 2 the empty set ; coherence the empty set is set ; let X, Y be set ; funcX \/ Y -> set means :Def3: :: XBOOLE_0:def 3 for x being set holds ( x in it iff ( x in X or x in Y ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in X or x in Y ) ) proof take union {X,Y} ; ::_thesis: for x being set holds ( x in union {X,Y} iff ( x in X or x in Y ) ) let x be set ; ::_thesis: ( x in union {X,Y} iff ( x in X or x in Y ) ) thus ( not x in union {X,Y} or x in X or x in Y ) ::_thesis: ( ( x in X or x in Y ) implies x in union {X,Y} ) proof assume x in union {X,Y} ; ::_thesis: ( x in X or x in Y ) then ex Z being set st ( x in Z & Z in {X,Y} ) by TARSKI:def_4; hence ( x in X or x in Y ) by TARSKI:def_2; ::_thesis: verum end; ( X in {X,Y} & Y in {X,Y} ) by TARSKI:def_2; hence ( ( x in X or x in Y ) implies x in union {X,Y} ) by TARSKI:def_4; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in X or x in Y ) ) ) & ( for x being set holds ( x in b2 iff ( x in X or x in Y ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff ( x in X or x in Y ) ) ) & ( for x being set holds ( x in A2 iff ( x in X or x in Y ) ) ) implies A1 = A2 ) assume that A3: for x being set holds ( x in A1 iff ( x in X or x in Y ) ) and A4: for x being set holds ( x in A2 iff ( x in X or x in Y ) ) ; ::_thesis: A1 = A2 now__::_thesis:_for_x_being_set_holds_ (_x_in_A1_iff_x_in_A2_) let x be set ; ::_thesis: ( x in A1 iff x in A2 ) ( x in A1 iff ( x in X or x in Y ) ) by A3; hence ( x in A1 iff x in A2 ) by A4; ::_thesis: verum end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; commutativity for b1, X, Y being set st ( for x being set holds ( x in b1 iff ( x in X or x in Y ) ) ) holds for x being set holds ( x in b1 iff ( x in Y or x in X ) ) ; idempotence for X, x being set holds ( x in X iff ( x in X or x in X ) ) ; funcX /\ Y -> set means :Def4: :: XBOOLE_0:def 4 for x being set holds ( x in it iff ( x in X & x in Y ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in X & x in Y ) ) proof defpred S1[ set ] means \$1 in Y; thus ex Z being set st for x being set holds ( x in Z iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in X & x in Y ) ) ) & ( for x being set holds ( x in b2 iff ( x in X & x in Y ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff ( x in X & x in Y ) ) ) & ( for x being set holds ( x in A2 iff ( x in X & x in Y ) ) ) implies A1 = A2 ) assume that A5: for x being set holds ( x in A1 iff ( x in X & x in Y ) ) and A6: for x being set holds ( x in A2 iff ( x in X & x in Y ) ) ; ::_thesis: A1 = A2 now__::_thesis:_for_x_being_set_holds_ (_x_in_A1_iff_x_in_A2_) let x be set ; ::_thesis: ( x in A1 iff x in A2 ) ( x in A1 iff ( x in X & x in Y ) ) by A5; hence ( x in A1 iff x in A2 ) by A6; ::_thesis: verum end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; commutativity for b1, X, Y being set st ( for x being set holds ( x in b1 iff ( x in X & x in Y ) ) ) holds for x being set holds ( x in b1 iff ( x in Y & x in X ) ) ; idempotence for X, x being set holds ( x in X iff ( x in X & x in X ) ) ; funcX \ Y -> set means :Def5: :: XBOOLE_0:def 5 for x being set holds ( x in it iff ( x in X & not x in Y ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in X & not x in Y ) ) proof defpred S1[ set ] means not \$1 in Y; thus ex Z being set st for x being set holds ( x in Z iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in X & not x in Y ) ) ) & ( for x being set holds ( x in b2 iff ( x in X & not x in Y ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff ( x in X & not x in Y ) ) ) & ( for x being set holds ( x in A2 iff ( x in X & not x in Y ) ) ) implies A1 = A2 ) assume that A7: for x being set holds ( x in A1 iff ( x in X & not x in Y ) ) and A8: for x being set holds ( x in A2 iff ( x in X & not x in Y ) ) ; ::_thesis: A1 = A2 now__::_thesis:_for_x_being_set_holds_ (_x_in_A1_iff_x_in_A2_) let x be set ; ::_thesis: ( x in A1 iff x in A2 ) ( x in A1 iff ( x in X & not x in Y ) ) by A7; hence ( x in A1 iff x in A2 ) by A8; ::_thesis: verum end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines {} XBOOLE_0:def_2_:_ {} = the empty set ; :: deftheorem Def3 defines \/ XBOOLE_0:def_3_:_ for X, Y, b3 being set holds ( b3 = X \/ Y iff for x being set holds ( x in b3 iff ( x in X or x in Y ) ) ); :: deftheorem Def4 defines /\ XBOOLE_0:def_4_:_ for X, Y, b3 being set holds ( b3 = X /\ Y iff for x being set holds ( x in b3 iff ( x in X & x in Y ) ) ); :: deftheorem Def5 defines \ XBOOLE_0:def_5_:_ for X, Y, b3 being set holds ( b3 = X \ Y iff for x being set holds ( x in b3 iff ( x in X & not x in Y ) ) ); definition let X, Y be set ; funcX \+\ Y -> set equals :: XBOOLE_0:def 6 (X \ Y) \/ (Y \ X); correctness coherence (X \ Y) \/ (Y \ X) is set ; ; commutativity for b1, X, Y being set st b1 = (X \ Y) \/ (Y \ X) holds b1 = (Y \ X) \/ (X \ Y) ; predX misses Y means :Def7: :: XBOOLE_0:def 7 X /\ Y = {} ; symmetry for X, Y being set st X /\ Y = {} holds Y /\ X = {} ; predX c< Y means :Def8: :: XBOOLE_0:def 8 ( X c= Y & X <> Y ); irreflexivity for X being set holds ( not X c= X or not X <> X ) ; asymmetry for X, Y being set st X c= Y & X <> Y & Y c= X holds not Y <> X proof let X, Y be set ; ::_thesis: ( X c= Y & X <> Y & Y c= X implies not Y <> X ) assume A1: X c= Y ; ::_thesis: ( not X <> Y or not Y c= X or not Y <> X ) assume X <> Y ; ::_thesis: ( not Y c= X or not Y <> X ) assume Y c= X ; ::_thesis: not Y <> X then for x being set holds ( x in X iff x in Y ) by A1, TARSKI:def_3; hence not Y <> X by TARSKI:1; ::_thesis: verum end; predX,Y are_c=-comparable means :: XBOOLE_0:def 9 ( X c= Y or Y c= X ); reflexivity for X being set holds ( X c= X or X c= X ) ; symmetry for X, Y being set holds ( ( not X c= Y & not Y c= X ) or Y c= X or X c= Y ) ; redefine pred X = Y means :: XBOOLE_0:def 10 ( X c= Y & Y c= X ); compatibility ( X = Y iff ( X c= Y & Y c= X ) ) proof thus ( X = Y implies ( X c= Y & Y c= X ) ) ; ::_thesis: ( X c= Y & Y c= X implies X = Y ) assume ( X c= Y & Y c= X ) ; ::_thesis: X = Y then for x being set holds ( x in X iff x in Y ) by TARSKI:def_3; hence X = Y by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines \+\ XBOOLE_0:def_6_:_ for X, Y being set holds X \+\ Y = (X \ Y) \/ (Y \ X); :: deftheorem Def7 defines misses XBOOLE_0:def_7_:_ for X, Y being set holds ( X misses Y iff X /\ Y = {} ); :: deftheorem Def8 defines c< XBOOLE_0:def_8_:_ for X, Y being set holds ( X c< Y iff ( X c= Y & X <> Y ) ); :: deftheorem defines are_c=-comparable XBOOLE_0:def_9_:_ for X, Y being set holds ( X,Y are_c=-comparable iff ( X c= Y or Y c= X ) ); :: deftheorem defines = XBOOLE_0:def_10_:_ for X, Y being set holds ( X = Y iff ( X c= Y & Y c= X ) ); notation let X, Y be set ; antonym X meets Y for X misses Y; end; theorem :: XBOOLE_0:1 for x, X, Y being set holds ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) ) proof let x, X, Y be set ; ::_thesis: ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) ) ( x in X \+\ Y iff ( x in X \ Y or x in Y \ X ) ) by Def3; hence ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) ) by Def5; ::_thesis: verum end; theorem :: XBOOLE_0:2 for X, Y, Z being set st ( for x being set holds ( not x in X iff ( x in Y iff x in Z ) ) ) holds X = Y \+\ Z proof let X, Y, Z be set ; ::_thesis: ( ( for x being set holds ( not x in X iff ( x in Y iff x in Z ) ) ) implies X = Y \+\ Z ) assume A1: for x being set holds ( not x in X iff ( x in Y iff x in Z ) ) ; ::_thesis: X = Y \+\ Z now__::_thesis:_for_x_being_set_holds_ (_x_in_X_iff_x_in_Y_\+\_Z_) let x be set ; ::_thesis: ( x in X iff x in Y \+\ Z ) ( x in X iff ( ( x in Y & not x in Z ) or ( x in Z & not x in Y ) ) ) by A1; then ( x in X iff ( x in Y \ Z or x in Z \ Y ) ) by Def5; hence ( x in X iff x in Y \+\ Z ) by Def3; ::_thesis: verum end; hence X = Y \+\ Z by TARSKI:1; ::_thesis: verum end; registration cluster {} -> empty ; coherence {} is empty ; end; registration let x1 be set ; cluster{x1} -> non empty ; coherence not {x1} is empty proof x1 in {x1} by TARSKI:def_1; hence ex x being set st x in {x1} ; :: according to XBOOLE_0:def_1 ::_thesis: verum end; let x2 be set ; cluster{x1,x2} -> non empty ; coherence not {x1,x2} is empty proof x1 in {x1,x2} by TARSKI:def_2; hence ex x being set st x in {x1,x2} ; :: according to XBOOLE_0:def_1 ::_thesis: verum end; end; registration cluster non empty for set ; existence not for b1 being set holds b1 is empty proof take { the set } ; ::_thesis: not { the set } is empty thus not { the set } is empty ; ::_thesis: verum end; end; registration let D be non empty set ; let X be set ; clusterD \/ X -> non empty ; coherence not D \/ X is empty proof consider x being set such that A1: x in D by Def1; x in D \/ X by A1, Def3; hence ex x being set st x in D \/ X ; :: according to XBOOLE_0:def_1 ::_thesis: verum end; clusterX \/ D -> non empty ; coherence not X \/ D is empty ; end; Lm1: for X being set st X is empty holds X = {} proof let X be set ; ::_thesis: ( X is empty implies X = {} ) assume for x being set holds not x in X ; :: according to XBOOLE_0:def_1 ::_thesis: X = {} then for x being set holds ( x in {} iff x in X ) by Def1; hence X = {} by TARSKI:1; ::_thesis: verum end; theorem Th3: :: XBOOLE_0:3 for X, Y being set holds ( X meets Y iff ex x being set st ( x in X & x in Y ) ) proof let X, Y be set ; ::_thesis: ( X meets Y iff ex x being set st ( x in X & x in Y ) ) hereby ::_thesis: ( ex x being set st ( x in X & x in Y ) implies X meets Y ) assume X meets Y ; ::_thesis: ex x being set st ( x in X & x in Y ) then X /\ Y <> {} by Def7; then not X /\ Y is empty by Lm1; then consider x being set such that A1: x in X /\ Y by Def1; take x = x; ::_thesis: ( x in X & x in Y ) thus ( x in X & x in Y ) by A1, Def4; ::_thesis: verum end; given x being set such that A2: ( x in X & x in Y ) ; ::_thesis: X meets Y x in X /\ Y by A2, Def4; then X /\ Y <> {} by Def1; hence X meets Y by Def7; ::_thesis: verum end; theorem :: XBOOLE_0:4 for X, Y being set holds ( X meets Y iff ex x being set st x in X /\ Y ) proof let X, Y be set ; ::_thesis: ( X meets Y iff ex x being set st x in X /\ Y ) hereby ::_thesis: ( ex x being set st x in X /\ Y implies X meets Y ) assume X meets Y ; ::_thesis: ex x being set st x in X /\ Y then X /\ Y <> {} by Def7; then not X /\ Y is empty by Lm1; then consider x being set such that A1: x in X /\ Y by Def1; take x = x; ::_thesis: x in X /\ Y thus x in X /\ Y by A1; ::_thesis: verum end; assume ex x being set st x in X /\ Y ; ::_thesis: X meets Y then X /\ Y <> {} by Def1; hence X meets Y by Def7; ::_thesis: verum end; theorem :: XBOOLE_0:5 for X, Y, x being set st X misses Y & x in X \/ Y & not ( x in X & not x in Y ) holds ( x in Y & not x in X ) by Def3, Th3; scheme :: XBOOLE_0:sch 2 Extensionality{ F1() -> set , F2() -> set , P1[ set ] } : F1() = F2() provided A1: for x being set holds ( x in F1() iff P1[x] ) and A2: for x being set holds ( x in F2() iff P1[x] ) proof A3: for x being set st x in F2() holds x in F1() proof let x be set ; ::_thesis: ( x in F2() implies x in F1() ) assume x in F2() ; ::_thesis: x in F1() then P1[x] by A2; hence x in F1() by A1; ::_thesis: verum end; for x being set st x in F1() holds x in F2() proof let x be set ; ::_thesis: ( x in F1() implies x in F2() ) assume x in F1() ; ::_thesis: x in F2() then P1[x] by A1; hence x in F2() by A2; ::_thesis: verum end; hence F1() = F2() by A3, TARSKI:1; ::_thesis: verum end; scheme :: XBOOLE_0:sch 3 SetEq{ P1[ set ] } : for X1, X2 being set st ( for x being set holds ( x in X1 iff P1[x] ) ) & ( for x being set holds ( x in X2 iff P1[x] ) ) holds X1 = X2 proof let X1, X2 be set ; ::_thesis: ( ( for x being set holds ( x in X1 iff P1[x] ) ) & ( for x being set holds ( x in X2 iff P1[x] ) ) implies X1 = X2 ) assume that A1: for x being set holds ( x in X1 iff P1[x] ) and A2: for x being set holds ( x in X2 iff P1[x] ) ; ::_thesis: X1 = X2 thus X1 = X2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum end; begin theorem :: XBOOLE_0:6 for X, Y being set st X c< Y holds ex x being set st ( x in Y & not x in X ) proof let X, Y be set ; ::_thesis: ( X c< Y implies ex x being set st ( x in Y & not x in X ) ) assume X c< Y ; ::_thesis: ex x being set st ( x in Y & not x in X ) then ( not for x being set holds ( x in X iff x in Y ) & X c= Y ) by Def8, TARSKI:1; hence ex x being set st ( x in Y & not x in X ) by TARSKI:def_3; ::_thesis: verum end; theorem :: XBOOLE_0:7 for X being set st X <> {} holds ex x being set st x in X proof let X be set ; ::_thesis: ( X <> {} implies ex x being set st x in X ) assume A1: X <> {} ; ::_thesis: ex x being set st x in X assume for x being set holds not x in X ; ::_thesis: contradiction then X is empty by Def1; hence contradiction by A1, Lm1; ::_thesis: verum end;