finsub_1.miz

    begin

    reserve X,Y,x for set;

    definition

      let IT be set;

      :: FINSUB_1:def1

      attr IT is cup-closed means

      : Def1: for X,Y be set st X in IT & Y in IT holds (X \/ Y) in IT;

      :: FINSUB_1:def2

      attr IT is cap-closed means for X,Y be set st X in IT & Y in IT holds (X /\ Y) in IT;

      :: FINSUB_1:def3

      attr IT is diff-closed means

      : Def3: for X,Y be set st X in IT & Y in IT holds (X \ Y) in IT;

    end

    definition

      let IT be set;

      :: FINSUB_1:def4

      attr IT is preBoolean means IT is cup-closed diff-closed;

    end

    registration

      cluster preBoolean -> cup-closed diff-closed for set;

      coherence ;

      cluster cup-closed diff-closed -> preBoolean for set;

      coherence ;

    end

    registration

      cluster non empty cup-closed cap-closed diff-closed for set;

      existence

      proof

        take { {} };

        thus { {} } is non empty;

        thus { {} } is cup-closed

        proof

          let X,Y be set;

          assume that

           A1: X in { {} } and

           A2: Y in { {} };

          X = {} by A1, TARSKI:def 1;

          hence thesis by A2;

        end;

        thus { {} } is cap-closed

        proof

          let X,Y be set;

          assume that

           A3: X in { {} } and Y in { {} };

          X = {} by A3, TARSKI:def 1;

          hence thesis by TARSKI:def 1;

        end;

        thus { {} } is diff-closed

        proof

          let X,Y be set;

          assume that

           A4: X in { {} } and Y in { {} };

          X = {} by A4, TARSKI:def 1;

          hence thesis by TARSKI:def 1;

        end;

      end;

    end

    theorem :: FINSUB_1:1



     Th1: for A be set holds A is preBoolean iff for X,Y be set st X in A & Y in A holds (X \/ Y) in A & (X \ Y) in A

    proof

      let A be set;

      thus A is preBoolean implies for X,Y be set st X in A & Y in A holds (X \/ Y) in A & (X \ Y) in A by Def1, Def3;

      assume

       A1: for X,Y be set st X in A & Y in A holds (X \/ Y) in A & (X \ Y) in A;



       A2: A is diff-closed by A1;

      A is cup-closed by A1;

      hence thesis by A2;

    end;

    reserve A for non empty preBoolean set;

    definition

      let A;

      let X,Y be Element of A;

      :: original: \/

      redefine

      func X \/ Y -> Element of A ;

      correctness by Th1;

      :: original: \

      redefine

      func X \ Y -> Element of A ;

      correctness by Th1;

    end

    theorem :: FINSUB_1:2



     Th2: X is Element of A & Y is Element of A implies (X /\ Y) is Element of A

    proof

      assume X is Element of A & Y is Element of A;

      then

      reconsider X, Y as Element of A;

      (X /\ Y) = (X \ (X \ Y)) by XBOOLE_1: 48;

      hence thesis;

    end;

    theorem :: FINSUB_1:3



     Th3: X is Element of A & Y is Element of A implies (X \+\ Y) is Element of A

    proof

      assume X is Element of A & Y is Element of A;

      then

      reconsider X, Y as Element of A;

      (X \+\ Y) = ((X \ Y) \/ (Y \ X));

      hence thesis;

    end;

    theorem :: FINSUB_1:4

    for A be non empty set st for X,Y be Element of A holds (X \+\ Y) in A & (X \ Y) in A holds A is preBoolean

    proof

      let A be non empty set such that

       A1: for X,Y be Element of A holds (X \+\ Y) in A & (X \ Y) in A;

      now

        let X,Y be set;

        assume that

         A2: X in A and

         A3: 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;

        thus (X \ Y) in A by A1, A2, A3;

      end;

      hence thesis by Th1;

    end;

    theorem :: FINSUB_1:5

    for A be non empty set st for X,Y be Element of A holds (X \+\ Y) in A & (X /\ Y) in A holds A is preBoolean

    proof

      let A be non empty set such that

       A1: for X,Y be Element of A holds (X \+\ Y) in A & (X /\ Y) in A;

      now

        let X,Y be set;

        assume that

         A2: X in A and

         A3: 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;

        (X \ Y) = (X \+\ Z2) by XBOOLE_1: 100;

        hence (X \ Y) in A by A1, A2;

      end;

      hence thesis by Th1;

    end;

    theorem :: FINSUB_1:6

    for A be non empty set st for X,Y be Element of A holds (X \+\ Y) in A & (X \/ Y) in A holds A is preBoolean

    proof

      let A be non empty set such that

       A1: for X,Y be Element of A holds (X \+\ Y) in A & (X \/ Y) in A;

      now

        let X,Y be set;

        assume that

         A2: X in A and

         A3: Y in A;

        thus (X \/ Y) in A by A1, A2, A3;

        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;

      end;

      hence thesis by Th1;

    end;

    definition

      let A;

      let X,Y be Element of A;

      :: original: /\

      redefine

      func X /\ Y -> Element of A ;

      coherence by Th2;

      :: original: \+\

      redefine

      func X \+\ Y -> Element of A ;

      coherence by Th3;

    end

    theorem :: FINSUB_1:7



     Th7: {} in A

    proof

      set x = the Element of A;

      (x \ x) = {} by XBOOLE_1: 37;

      hence thesis;

    end;

    theorem :: FINSUB_1:8



     Th8: for A be set holds ( bool A) is preBoolean

    proof

      let A be set;

      now

        let X,Y be set;

        assume X in ( bool A) & 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);

      end;

      hence thesis by Th1;

    end;

    registration

      let A be set;

      cluster ( bool A) -> preBoolean;

      coherence by Th8;

    end

    theorem :: FINSUB_1:9

    for A,B be non empty preBoolean set holds (A /\ B) is non empty preBoolean

    proof

      let A,B be non empty preBoolean set;

       {} in A & {} in B by Th7;

      then

      reconsider C = (A /\ B) as non empty set by XBOOLE_0:def 4;

      now

        let X,Y be set;

        assume

         A1: X in C & 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;

        (X \ Y) in A by A5, Th1;

        hence (X \ Y) in C by A4, XBOOLE_0:def 4;

      end;

      hence thesis by Th1;

    end;

    definition

      let A be set;

      :: FINSUB_1:def5

      func Fin A -> preBoolean set means

      : Def5: for X be set holds X in it iff X c= A & X is finite;

      existence

      proof

        defpred P[ object] means ex y be set st y = $1 & y c= A & y is finite;

        consider P be set such that

         A1: for x be object holds x in P iff x in ( bool A) & P[x] from XBOOLE_0:sch 1;

         {} c= A;

        then

        reconsider Q = P as non empty set by A1;

        for X,Y be set st X in Q & Y in Q holds (X \/ Y) in Q & (X \ Y) in Q

        proof

          let X,Y be set;

          assume that

           A2: X in Q and

           A3: Y in Q;

          consider Z1 be set such that

           A4: Z1 = X and

           A5: Z1 c= A and

           A6: Z1 is finite by A1, A2;

          consider Z2 be 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;

          (Z1 \/ Z2) c= A by A5, A8, XBOOLE_1: 8;

          hence thesis by A1, A4, A6, A7, A9, A10;

        end;

        then

        reconsider R = Q as non empty preBoolean set by Th1;

        for X be set holds X in R iff X c= A & X is finite

        proof

          let X be set;

          thus X in R implies X c= A & X is finite

          proof

            assume X in R;

            then ex Y be set st Y = X & Y c= A & Y is finite by A1;

            hence thesis;

          end;

          thus thesis by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let P,Q be preBoolean set;

        assume that

         A11: for X be set holds X in P iff X c= A & X is finite and

         A12: for X be set holds X in Q iff X c= A & X is finite;

        for x be object holds x in P iff x in Q

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          thus x in P implies x in Q

          proof

            assume x in P;

            then xx c= A & xx is finite by A11;

            hence thesis by A12;

          end;

          thus x in Q implies x in P

          proof

            assume x in Q;

            then xx c= A & xx is finite by A12;

            hence thesis by A11;

          end;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let A be set;

      cluster ( Fin A) -> non empty;

      coherence

      proof

         {} c= A;

        hence thesis by Def5;

      end;

    end

    registration

      let A be set;

      cluster -> finite for Element of ( Fin A);

      coherence by Def5;

    end

    theorem :: FINSUB_1:10



     Th10: for A,B be set st A c= B holds ( Fin A) c= ( Fin B)

    proof

      let A,B be set;

      assume

       A1: A c= B;

      let X be object;

      reconsider XX = X as set by TARSKI: 1;

      assume

       A2: X in ( Fin A);

      then XX c= A by Def5;

      then XX c= B by A1;

      hence X in ( Fin B) by A2, Def5;

    end;

    theorem :: FINSUB_1:11

    for A,B be set holds ( Fin (A /\ B)) = (( Fin A) /\ ( Fin B))

    proof

      let A,B be set;

      ( 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;

      let X be object;

      reconsider XX = X as set by TARSKI: 1;

      assume

       A1: X in (( Fin A) /\ ( Fin B));

      then X in ( Fin B) by XBOOLE_0:def 4;

      then

       A2: XX c= B by Def5;



       A3: X in ( Fin A) by A1, XBOOLE_0:def 4;

      then XX c= A by Def5;

      then XX c= (A /\ B) by A2, XBOOLE_1: 19;

      hence X in ( Fin (A /\ B)) by A3, Def5;

    end;

    theorem :: FINSUB_1:12

    for A,B be set holds (( Fin A) \/ ( Fin B)) c= ( Fin (A \/ B))

    proof

      let A,B be set;

      ( Fin A) c= ( Fin (A \/ B)) & ( Fin B) c= ( Fin (A \/ B)) by Th10, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: FINSUB_1:13



     Th13: for A be set holds ( Fin A) c= ( bool A)

    proof

      let A be set;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in ( Fin A);

      then xx c= A by Def5;

      hence thesis;

    end;

    theorem :: FINSUB_1:14



     Th14: for A be set st A is finite holds ( Fin A) = ( bool A)

    proof

      let A be set;

      assume

       A1: A is finite;



       A2: ( bool A) c= ( Fin A) by A1, Def5;

      ( Fin A) c= ( bool A) by Th13;

      hence thesis by A2;

    end;

    theorem :: FINSUB_1:15

    ( Fin {} ) = { {} } by Th14, ZFMISC_1: 1;

    theorem :: FINSUB_1:16

    for A be set, X be Element of ( Fin A) holds X is Subset of A by Def5;

    theorem :: FINSUB_1:17

    for A be set, X be Subset of A st A is finite holds X is Element of ( Fin A) by Def5;