:: FINSUB_1 semantic presentation begin definition let IT be set ; attrIT is cup-closed means :Def1: :: FINSUB_1:def 1 for X, Y being set st X in IT & Y in IT holds X \/ Y in IT; attrIT is cap-closed means :: FINSUB_1:def 2 for X, Y being set st X in IT & Y in IT holds X /\ Y in IT; attrIT is diff-closed means :Def3: :: FINSUB_1:def 3 for X, Y being set st X in IT & Y in IT holds X \ Y in IT; end; :: deftheorem Def1 defines cup-closed FINSUB_1:def_1_:_ for IT being set holds ( IT is cup-closed iff for X, Y being set st X in IT & Y in IT holds X \/ Y in IT ); :: deftheorem defines cap-closed FINSUB_1:def_2_:_ for IT being set holds ( IT is cap-closed iff for X, Y being set st X in IT & Y in IT holds X /\ Y in IT ); :: deftheorem Def3 defines diff-closed FINSUB_1:def_3_:_ for IT being set holds ( IT is diff-closed iff for X, Y being set st X in IT & Y in IT holds X \ Y in IT ); definition let IT be set ; attrIT is preBoolean means :Def4: :: FINSUB_1:def 4 ( IT is cup-closed & IT is diff-closed ); end; :: deftheorem Def4 defines preBoolean FINSUB_1:def_4_:_ for IT being set holds ( IT is preBoolean iff ( IT is cup-closed & IT is diff-closed ) ); registration cluster preBoolean -> cup-closed diff-closed for set ; coherence for b1 being set st b1 is preBoolean holds ( b1 is cup-closed & b1 is diff-closed ) by Def4; cluster cup-closed diff-closed -> preBoolean for set ; coherence for b1 being set st b1 is cup-closed & b1 is diff-closed holds b1 is preBoolean by Def4; end; registration cluster non empty cup-closed cap-closed diff-closed for set ; existence ex b1 being set st ( not b1 is empty & b1 is cup-closed & b1 is cap-closed & b1 is diff-closed ) proof take {{}} ; ::_thesis: ( not {{}} is empty & {{}} is cup-closed & {{}} is cap-closed & {{}} is diff-closed ) thus not {{}} is empty ; ::_thesis: ( {{}} is cup-closed & {{}} is cap-closed & {{}} is diff-closed ) thus {{}} is cup-closed ::_thesis: ( {{}} is cap-closed & {{}} is diff-closed ) proof let X, Y be set ; :: according to FINSUB_1:def_1 ::_thesis: ( X in {{}} & Y in {{}} implies X \/ Y in {{}} ) assume that A1: X in {{}} and A2: Y in {{}} ; ::_thesis: X \/ Y in {{}} X = {} by A1, TARSKI:def_1; hence X \/ Y in {{}} by A2; ::_thesis: verum end; thus {{}} is cap-closed ::_thesis: {{}} is diff-closed proof let X, Y be set ; :: according to FINSUB_1:def_2 ::_thesis: ( X in {{}} & Y in {{}} implies X /\ Y in {{}} ) assume that A3: X in {{}} and Y in {{}} ; ::_thesis: X /\ Y in {{}} X = {} by A3, TARSKI:def_1; hence X /\ Y in {{}} by TARSKI:def_1; ::_thesis: verum end; thus {{}} is diff-closed ::_thesis: verum proof let X, Y be set ; :: according to FINSUB_1:def_3 ::_thesis: ( X in {{}} & Y in {{}} implies X \ Y in {{}} ) assume that A4: X in {{}} and Y in {{}} ; ::_thesis: X \ Y in {{}} X = {} by A4, TARSKI:def_1; hence X \ Y in {{}} by TARSKI:def_1; ::_thesis: verum end; end; end; theorem Th1: :: FINSUB_1:1 for A being set holds ( A is preBoolean iff for X, Y being set st X in A & Y in A holds ( X \/ Y in A & X \ Y in A ) ) proof let A be set ; ::_thesis: ( A is preBoolean iff for X, Y being set st X in A & Y in A holds ( X \/ Y in A & X \ Y in A ) ) thus ( A is preBoolean implies for X, Y being set st X in A & Y in A holds ( X \/ Y in A & X \ Y in A ) ) by Def1, Def3; ::_thesis: ( ( for X, Y being set st X in A & Y in A holds ( X \/ Y in A & X \ Y in A ) ) implies A is preBoolean ) assume A1: for X, Y being set st X in A & Y in A holds ( X \/ Y in A & X \ Y in A ) ; ::_thesis: A is preBoolean A2: A is diff-closed proof let X, Y be set ; :: according to FINSUB_1:def_3 ::_thesis: ( X in A & Y in A implies X \ Y in A ) assume ( X in A & Y in A ) ; ::_thesis: X \ Y in A hence X \ Y in A by A1; ::_thesis: verum end; A is cup-closed proof let X, Y be set ; :: according to FINSUB_1:def_1 ::_thesis: ( X in A & Y in A implies X \/ Y in A ) assume ( X in A & Y in A ) ; ::_thesis: X \/ Y in A hence X \/ Y in A by A1; ::_thesis: verum end; hence A is preBoolean by A2; ::_thesis: verum end; definition let A be non empty preBoolean set ; let X, Y be Element of A; :: original: \/ redefine funcX \/ Y -> Element of A; correctness coherence X \/ Y is Element of A; by Th1; :: original: \ redefine funcX \ Y -> Element of A; correctness coherence X \ Y is Element of A; by Th1; end; theorem Th2: :: FINSUB_1:2 for X, Y being set for A being non empty preBoolean set st X is Element of A & Y is Element of A holds X /\ Y is Element of A proof let X, Y be set ; ::_thesis: for A being non empty preBoolean set st X is Element of A & Y is Element of A holds X /\ Y is Element of A let A be non empty preBoolean set ; ::_thesis: ( X is Element of A & Y is Element of A implies X /\ Y is Element of A ) assume ( X is Element of A & Y is Element of A ) ; ::_thesis: X /\ Y is Element of A then reconsider X = X, Y = Y as Element of A ; X /\ Y = X \ (X \ Y) by XBOOLE_1:48; hence X /\ Y is Element of A ; ::_thesis: verum end; theorem Th3: :: FINSUB_1:3 for X, Y being set for A being non empty preBoolean set st X is Element of A & Y is Element of A holds X \+\ Y is Element of A proof let X, Y be set ; ::_thesis: for A being non empty preBoolean set st X is Element of A & Y is Element of A holds X \+\ Y is Element of A let A be non empty preBoolean set ; ::_thesis: ( X is Element of A & Y is Element of A implies X \+\ Y is Element of A ) assume ( X is Element of A & Y is Element of A ) ; ::_thesis: X \+\ Y is Element of A then reconsider X = X, Y = Y as Element of A ; X \+\ Y = (X \ Y) \/ (Y \ X) ; hence X \+\ Y is Element of A ; ::_thesis: verum end; theorem :: FINSUB_1:4 for A being non empty set st ( for X, Y being Element of A holds ( X \+\ Y in A & X \ Y in A ) ) holds A is preBoolean proof let A be non empty set ; ::_thesis: ( ( for X, Y being Element of A holds ( X \+\ Y in A & X \ Y in A ) ) implies A is preBoolean ) assume A1: for X, Y being Element of A holds ( X \+\ Y in A & X \ Y in A ) ; ::_thesis: A is preBoolean now__::_thesis:_for_X,_Y_being_set_st_X_in_A_&_Y_in_A_holds_ (_X_\/_Y_in_A_&_X_\_Y_in_A_) let X, Y be set ; ::_thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) ) assume that A2: X in A and A3: Y in A ; ::_thesis: ( X \/ Y in A & X \ Y in A ) reconsider Z = Y \ X as Element of A by A1, A2, A3; X \/ Y = X \+\ Z by XBOOLE_1:98; hence X \/ Y in A by A1, A2; ::_thesis: X \ Y in A thus X \ Y in A by A1, A2, A3; ::_thesis: verum end; hence A is preBoolean by Th1; ::_thesis: verum end; theorem :: FINSUB_1:5 for A being non empty set st ( for X, Y being Element of A holds ( X \+\ Y in A & X /\ Y in A ) ) holds A is preBoolean proof let A be non empty set ; ::_thesis: ( ( for X, Y being Element of A holds ( X \+\ Y in A & X /\ Y in A ) ) implies A is preBoolean ) assume A1: for X, Y being Element of A holds ( X \+\ Y in A & X /\ Y in A ) ; ::_thesis: A is preBoolean now__::_thesis:_for_X,_Y_being_set_st_X_in_A_&_Y_in_A_holds_ (_X_\/_Y_in_A_&_X_\_Y_in_A_) let X, Y be set ; ::_thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) ) assume that A2: X in A and A3: Y in A ; ::_thesis: ( X \/ Y in A & X \ Y in A ) reconsider Z1 = X \+\ Y, Z2 = X /\ Y as Element of A by A1, A2, A3; X \/ Y = Z1 \+\ Z2 by XBOOLE_1:94; hence X \/ Y in A by A1; ::_thesis: X \ Y in A X \ Y = X \+\ Z2 by XBOOLE_1:100; hence X \ Y in A by A1, A2; ::_thesis: verum end; hence A is preBoolean by Th1; ::_thesis: verum end; theorem :: FINSUB_1:6 for A being non empty set st ( for X, Y being Element of A holds ( X \+\ Y in A & X \/ Y in A ) ) holds A is preBoolean proof let A be non empty set ; ::_thesis: ( ( for X, Y being Element of A holds ( X \+\ Y in A & X \/ Y in A ) ) implies A is preBoolean ) assume A1: for X, Y being Element of A holds ( X \+\ Y in A & X \/ Y in A ) ; ::_thesis: A is preBoolean now__::_thesis:_for_X,_Y_being_set_st_X_in_A_&_Y_in_A_holds_ (_X_\/_Y_in_A_&_X_\_Y_in_A_) let X, Y be set ; ::_thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) ) assume that A2: X in A and A3: Y in A ; ::_thesis: ( X \/ Y in A & X \ Y in A ) thus X \/ Y in A by A1, A2, A3; ::_thesis: X \ Y in A reconsider Z1 = X \+\ Y, Z2 = X \/ Y as Element of A by A1, A2, A3; X /\ Y = Z1 \+\ Z2 by XBOOLE_1:95; then reconsider Z = X /\ Y as Element of A by A1; X \ Y = X \+\ Z by XBOOLE_1:100; hence X \ Y in A by A1, A2; ::_thesis: verum end; hence A is preBoolean by Th1; ::_thesis: verum end; definition let A be non empty preBoolean set ; let X, Y be Element of A; :: original: /\ redefine funcX /\ Y -> Element of A; coherence X /\ Y is Element of A by Th2; :: original: \+\ redefine funcX \+\ Y -> Element of A; coherence X \+\ Y is Element of A by Th3; end; theorem Th7: :: FINSUB_1:7 for A being non empty preBoolean set holds {} in A proof let A be non empty preBoolean set ; ::_thesis: {} in A set x = the Element of A; the Element of A \ the Element of A = {} by XBOOLE_1:37; hence {} in A ; ::_thesis: verum end; theorem Th8: :: FINSUB_1:8 for A being set holds bool A is preBoolean proof let A be set ; ::_thesis: bool A is preBoolean now__::_thesis:_for_X,_Y_being_set_st_X_in_bool_A_&_Y_in_bool_A_holds_ (_X_\/_Y_in_bool_A_&_X_\_Y_in_bool_A_) let X, Y be set ; ::_thesis: ( X in bool A & Y in bool A implies ( X \/ Y in bool A & X \ Y in bool A ) ) assume ( X in bool A & Y in bool A ) ; ::_thesis: ( X \/ Y in bool A & X \ Y in bool A ) then reconsider X9 = X, Y9 = Y as Subset of A ; ( X9 \/ Y9 in bool A & X9 \ Y9 in bool A ) ; hence ( X \/ Y in bool A & X \ Y in bool A ) ; ::_thesis: verum end; hence bool A is preBoolean by Th1; ::_thesis: verum end; registration let A be set ; cluster bool A -> preBoolean ; coherence bool A is preBoolean by Th8; end; theorem :: FINSUB_1:9 for A, B being non empty preBoolean set holds ( not A /\ B is empty & A /\ B is preBoolean ) proof let A, B be non empty preBoolean set ; ::_thesis: ( not A /\ B is empty & A /\ B is preBoolean ) ( {} in A & {} in B ) by Th7; then reconsider C = A /\ B as non empty set by XBOOLE_0:def_4; now__::_thesis:_for_X,_Y_being_set_st_X_in_C_&_Y_in_C_holds_ (_X_\/_Y_in_C_&_X_\_Y_in_C_) let X, Y be set ; ::_thesis: ( X in C & Y in C implies ( X \/ Y in C & X \ Y in C ) ) assume A1: ( X in C & Y in C ) ; ::_thesis: ( X \/ Y in C & X \ Y in C ) then A2: ( X in B & Y in B ) by XBOOLE_0:def_4; then A3: X \/ Y in B by Th1; A4: X \ Y in B by A2, Th1; A5: ( X in A & Y in A ) by A1, XBOOLE_0:def_4; then X \/ Y in A by Th1; hence X \/ Y in C by A3, XBOOLE_0:def_4; ::_thesis: X \ Y in C X \ Y in A by A5, Th1; hence X \ Y in C by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence ( not A /\ B is empty & A /\ B is preBoolean ) by Th1; ::_thesis: verum end; definition let A be set ; func Fin A -> preBoolean set means :Def5: :: FINSUB_1:def 5 for X being set holds ( X in it iff ( X c= A & X is finite ) ); existence ex b1 being preBoolean set st for X being set holds ( X in b1 iff ( X c= A & X is finite ) ) proof defpred S1[ set ] means ex y being set st ( y = \$1 & y c= A & y is finite ); consider P being set such that A1: for x being set holds ( x in P iff ( x in bool A & S1[x] ) ) from XBOOLE_0:sch_1(); {} c= A by XBOOLE_1:2; then reconsider Q = P as non empty set by A1; for X, Y being set st X in Q & Y in Q holds ( X \/ Y in Q & X \ Y in Q ) proof let X, Y be set ; ::_thesis: ( X in Q & Y in Q implies ( X \/ Y in Q & X \ Y in Q ) ) assume that A2: X in Q and A3: Y in Q ; ::_thesis: ( X \/ Y in Q & X \ Y in Q ) consider Z1 being set such that A4: Z1 = X and A5: Z1 c= A and A6: Z1 is finite by A1, A2; consider Z2 being set such that A7: Z2 = Y and A8: Z2 c= A and A9: Z2 is finite by A1, A3; A10: Z1 \ Z2 c= A by A5, XBOOLE_1:1; Z1 \/ Z2 c= A by A5, A8, XBOOLE_1:8; hence ( X \/ Y in Q & X \ Y in Q ) by A1, A4, A6, A7, A9, A10; ::_thesis: verum end; then reconsider R = Q as non empty preBoolean set by Th1; for X being set holds ( X in R iff ( X c= A & X is finite ) ) proof let X be set ; ::_thesis: ( X in R iff ( X c= A & X is finite ) ) thus ( X in R implies ( X c= A & X is finite ) ) ::_thesis: ( X c= A & X is finite implies X in R ) proof assume X in R ; ::_thesis: ( X c= A & X is finite ) then ex Y being set st ( Y = X & Y c= A & Y is finite ) by A1; hence ( X c= A & X is finite ) ; ::_thesis: verum end; thus ( X c= A & X is finite implies X in R ) by A1; ::_thesis: verum end; hence ex b1 being preBoolean set st for X being set holds ( X in b1 iff ( X c= A & X is finite ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being preBoolean set st ( for X being set holds ( X in b1 iff ( X c= A & X is finite ) ) ) & ( for X being set holds ( X in b2 iff ( X c= A & X is finite ) ) ) holds b1 = b2 proof let P, Q be preBoolean set ; ::_thesis: ( ( for X being set holds ( X in P iff ( X c= A & X is finite ) ) ) & ( for X being set holds ( X in Q iff ( X c= A & X is finite ) ) ) implies P = Q ) assume that A11: for X being set holds ( X in P iff ( X c= A & X is finite ) ) and A12: for X being set holds ( X in Q iff ( X c= A & X is finite ) ) ; ::_thesis: P = Q for x being set holds ( x in P iff x in Q ) proof let x be set ; ::_thesis: ( x in P iff x in Q ) thus ( x in P implies x in Q ) ::_thesis: ( x in Q implies x in P ) proof assume x in P ; ::_thesis: x in Q then ( x c= A & x is finite ) by A11; hence x in Q by A12; ::_thesis: verum end; thus ( x in Q implies x in P ) ::_thesis: verum proof assume x in Q ; ::_thesis: x in P then ( x c= A & x is finite ) by A12; hence x in P by A11; ::_thesis: verum end; end; hence P = Q by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def5 defines Fin FINSUB_1:def_5_:_ for A being set for b2 being preBoolean set holds ( b2 = Fin A iff for X being set holds ( X in b2 iff ( X c= A & X is finite ) ) ); registration let A be set ; cluster Fin A -> non empty preBoolean ; coherence not Fin A is empty proof {} c= A by XBOOLE_1:2; hence not Fin A is empty by Def5; ::_thesis: verum end; end; registration let A be set ; cluster -> finite for Element of Fin A; coherence for b1 being Element of Fin A holds b1 is finite by Def5; end; theorem Th10: :: FINSUB_1:10 for A, B being set st A c= B holds Fin A c= Fin B proof let A, B be set ; ::_thesis: ( A c= B implies Fin A c= Fin B ) assume A1: A c= B ; ::_thesis: Fin A c= Fin B now__::_thesis:_for_X_being_set_st_X_in_Fin_A_holds_ X_in_Fin_B let X be set ; ::_thesis: ( X in Fin A implies X in Fin B ) assume A2: X in Fin A ; ::_thesis: X in Fin B then X c= A by Def5; then X c= B by A1, XBOOLE_1:1; hence X in Fin B by A2, Def5; ::_thesis: verum end; hence Fin A c= Fin B by TARSKI:def_3; ::_thesis: verum end; theorem :: FINSUB_1:11 for A, B being set holds Fin (A /\ B) = (Fin A) /\ (Fin B) proof let A, B be set ; ::_thesis: Fin (A /\ B) = (Fin A) /\ (Fin B) ( Fin (A /\ B) c= Fin A & Fin (A /\ B) c= Fin B ) by Th10, XBOOLE_1:17; hence Fin (A /\ B) c= (Fin A) /\ (Fin B) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (Fin A) /\ (Fin B) c= Fin (A /\ B) now__::_thesis:_for_X_being_set_st_X_in_(Fin_A)_/\_(Fin_B)_holds_ X_in_Fin_(A_/\_B) let X be set ; ::_thesis: ( X in (Fin A) /\ (Fin B) implies X in Fin (A /\ B) ) assume A1: X in (Fin A) /\ (Fin B) ; ::_thesis: X in Fin (A /\ B) then X in Fin B by XBOOLE_0:def_4; then A2: X c= B by Def5; A3: X in Fin A by A1, XBOOLE_0:def_4; then X c= A by Def5; then X c= A /\ B by A2, XBOOLE_1:19; hence X in Fin (A /\ B) by A3, Def5; ::_thesis: verum end; hence (Fin A) /\ (Fin B) c= Fin (A /\ B) by TARSKI:def_3; ::_thesis: verum end; theorem :: FINSUB_1:12 for A, B being set holds (Fin A) \/ (Fin B) c= Fin (A \/ B) proof let A, B be set ; ::_thesis: (Fin A) \/ (Fin B) c= Fin (A \/ B) ( Fin A c= Fin (A \/ B) & Fin B c= Fin (A \/ B) ) by Th10, XBOOLE_1:7; hence (Fin A) \/ (Fin B) c= Fin (A \/ B) by XBOOLE_1:8; ::_thesis: verum end; theorem Th13: :: FINSUB_1:13 for A being set holds Fin A c= bool A proof let A be set ; ::_thesis: Fin A c= bool A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fin A or x in bool A ) assume x in Fin A ; ::_thesis: x in bool A then x c= A by Def5; hence x in bool A ; ::_thesis: verum end; theorem Th14: :: FINSUB_1:14 for A being set st A is finite holds Fin A = bool A proof let A be set ; ::_thesis: ( A is finite implies Fin A = bool A ) assume A1: A is finite ; ::_thesis: Fin A = bool A A2: bool A c= Fin A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool A or x in Fin A ) assume x in bool A ; ::_thesis: x in Fin A hence x in Fin A by A1, Def5; ::_thesis: verum end; Fin A c= bool A by Th13; hence Fin A = bool A by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FINSUB_1:15 Fin {} = {{}} by Th14, ZFMISC_1:1; definition let A be set ; mode Finite_Subset of A is Element of Fin A; end; theorem :: FINSUB_1:16 for A being set for X being Finite_Subset of A holds X is finite ; theorem :: FINSUB_1:17 for A being set for X being Finite_Subset of A holds X is Subset of A by Def5; theorem :: FINSUB_1:18 for A being set for X being Subset of A st A is finite holds X is Finite_Subset of A by Def5;