card_fil.miz



    begin

    theorem :: CARD_FIL:1

    for x be set holds for X be infinite set holds ( card {x}) in ( card X) by CARD_3: 86;

    scheme :: CARD_FIL:sch1

    ElemProp { D() -> non empty set , x() -> set , P[ set] } :

P[x()]

      provided

       A1: x() in { y where y be Element of D() : P[y] };

      ex y be Element of D() st x() = y & P[y] by A1;

      hence thesis;

    end;

    reserve N for Cardinal;

    reserve M for Aleph;

    reserve X for non empty set;

    reserve Y,Z,Z1,Z2,Y1,Y2,Y3,Y4 for Subset of X;

    reserve S for Subset-Family of X;

    reserve x for set;

    theorem :: CARD_FIL:2

    

     Th2: {X} is non empty Subset-Family of X & not {} in {X} & for Y1, Y2 holds (Y1 in {X} & Y2 in {X} implies (Y1 /\ Y2) in {X}) & (Y1 in {X} & Y1 c= Y2 implies Y2 in {X})

    proof

      

       A1: X c= X;

       {X} c= ( bool X)

      proof

        let x be object;

        assume x in {X};

        then x = X by TARSKI:def 1;

        hence thesis by A1;

      end;

      hence {X} is non empty Subset-Family of X;

      thus not {} in {X} by TARSKI:def 1;

      let Y1, Y2;

      thus Y1 in {X} & Y2 in {X} implies (Y1 /\ Y2) in {X}

      proof

        assume Y1 in {X} & Y2 in {X};

        then Y1 = X & Y2 = X by TARSKI:def 1;

        hence thesis by TARSKI:def 1;

      end;

      thus Y1 in {X} & Y1 c= Y2 implies Y2 in {X}

      proof

        assume Y1 in {X} & Y1 c= Y2;

        then X c= Y2 by TARSKI:def 1;

        then Y2 = X;

        hence thesis by TARSKI:def 1;

      end;

    end;

    definition

      let X;

      :: CARD_FIL:def1

      mode Filter of X -> non empty Subset-Family of X means

      : Def1: ( not {} in it ) & for Y1, Y2 holds (Y1 in it & Y2 in it implies (Y1 /\ Y2) in it ) & (Y1 in it & Y1 c= Y2 implies Y2 in it );

      existence

      proof

        take {X};

        thus thesis by Th2;

      end;

    end

    theorem :: CARD_FIL:3

    for F be set holds F is Filter of X iff (F is non empty Subset-Family of X & not {} in F & for Y1, Y2 holds (Y1 in F & Y2 in F implies (Y1 /\ Y2) in F) & (Y1 in F & Y1 c= Y2 implies Y2 in F)) by Def1;

    theorem :: CARD_FIL:4

    

     Th4: {X} is Filter of X

    proof

      

       A1: for Y1, Y2 holds (Y1 in {X} & Y2 in {X} implies (Y1 /\ Y2) in {X}) & (Y1 in {X} & Y1 c= Y2 implies Y2 in {X}) by Th2;

       {X} is non empty Subset-Family of X & not {} in {X} by Th2;

      hence thesis by A1, Def1;

    end;

    reserve F,Uf for Filter of X;

    theorem :: CARD_FIL:5

    

     Th5: X in F

    proof

      set Y = the Element of F;

      Y in F & X c= X;

      hence thesis by Def1;

    end;

    theorem :: CARD_FIL:6

    

     Th6: Y in F implies not (X \ Y) in F

    proof

      assume

       A1: Y in F;

      assume (X \ Y) in F;

      then

       A2: (Y /\ (X \ Y)) in F by A1, Def1;

      Y misses (X \ Y) by XBOOLE_1: 79;

      then {} in F by A2;

      hence contradiction by Def1;

    end;

    theorem :: CARD_FIL:7

    

     Th7: for I be non empty Subset-Family of X st (for Y holds Y in I iff (Y ` ) in F) holds ( not X in I) & for Y1, Y2 holds (Y1 in I & Y2 in I implies (Y1 \/ Y2) in I) & (Y1 in I & Y2 c= Y1 implies Y2 in I)

    proof

      let I be non empty Subset-Family of X such that

       A1: for Y holds (Y in I iff (Y ` ) in F);

       not ((( {} X) ` ) ` ) in F by Def1;

      hence not X in I by A1;

      let Y1, Y2;

      thus Y1 in I & Y2 in I implies (Y1 \/ Y2) in I

      proof

        assume Y1 in I & Y2 in I;

        then (Y1 ` ) in F & (Y2 ` ) in F by A1;

        then ((Y1 ` ) /\ (Y2 ` )) in F by Def1;

        then ((Y1 \/ Y2) ` ) in F by XBOOLE_1: 53;

        hence thesis by A1;

      end;

      assume that

       A2: Y1 in I and

       A3: Y2 c= Y1;

      

       A4: (Y1 ` ) c= (Y2 ` ) by A3, SUBSET_1: 12;

      (Y1 ` ) in F by A1, A2;

      then (Y2 ` ) in F by A4, Def1;

      hence thesis by A1;

    end;

    notation

      let X, S;

      synonym dual S for COMPLEMENT S;

    end

    reserve S for non empty Subset-Family of X;

    registration

      let X, S;

      cluster ( COMPLEMENT S) -> non empty;

      coherence by SETFAM_1: 32;

    end

    theorem :: CARD_FIL:8

    ( dual S) = { Y : (Y ` ) in S }

    proof

      thus ( dual S) c= { Y : (Y ` ) in S }

      proof

        let X1 be object such that

         A1: X1 in ( dual S);

        reconsider Y1 = X1 as Subset of X by A1;

        (Y1 ` ) in S by A1, SETFAM_1:def 7;

        hence thesis;

      end;

      let X1 be object;

      assume X1 in { Y : (Y ` ) in S };

      then ex Y st Y = X1 & (Y ` ) in S;

      hence thesis by SETFAM_1:def 7;

    end;

    theorem :: CARD_FIL:9

    

     Th9: ( dual S) = { (Y ` ) : Y in S }

    proof

      thus ( dual S) c= { (Y ` ) : Y in S }

      proof

        let X1 be object such that

         A1: X1 in ( dual S);

        reconsider Y1 = X1 as Subset of X by A1;

        (Y1 ` ) in S by A1, SETFAM_1:def 7;

        then ((Y1 ` ) ` ) in { (Y ` ) : Y in S };

        hence thesis;

      end;

      let X1 be object;

      assume X1 in { (Y ` ) : Y in S };

      then

      consider Y such that

       A2: (Y ` ) = X1 and

       A3: Y in S;

      ((Y ` ) ` ) in S by A3;

      hence thesis by A2, SETFAM_1:def 7;

    end;

    definition

      let X;

      :: CARD_FIL:def2

      mode Ideal of X -> non empty Subset-Family of X means

      : Def2: ( not X in it ) & for Y1, Y2 holds (Y1 in it & Y2 in it implies (Y1 \/ Y2) in it ) & (Y1 in it & Y2 c= Y1 implies Y2 in it );

      existence

      proof

        set F = the Filter of X;

        take ( dual F);

        for Y1 holds Y1 in ( dual F) iff (Y1 ` ) in F by SETFAM_1:def 7;

        hence thesis by Th7;

      end;

    end

    definition

      let X, F;

      :: original: dual

      redefine

      func dual F -> Ideal of X ;

      coherence

      proof

        for Y1 holds Y1 in ( dual F) iff (Y1 ` ) in F by SETFAM_1:def 7;

        then ( not X in ( dual F)) & for Y1, Y2 holds (Y1 in ( dual F) & Y2 in ( dual F) implies (Y1 \/ Y2) in ( dual F)) & (Y1 in ( dual F) & Y2 c= Y1 implies Y2 in ( dual F)) by Th7;

        hence thesis by Def2;

      end;

    end

    reserve I for Ideal of X;

    theorem :: CARD_FIL:10

    

     Th10: (for Y holds not (Y in F & Y in ( dual F))) & for Y holds not (Y in I & Y in ( dual I))

    proof

      thus for Y holds not (Y in F & Y in ( dual F))

      proof

        let Y;

        assume that

         A1: Y in F and

         A2: Y in ( dual F);

        (Y ` ) in F by A2, SETFAM_1:def 7;

        then

         A3: ((Y ` ) /\ Y) in F by A1, Def1;

        (Y ` ) misses Y by XBOOLE_1: 79;

        then ( {} X) in F by A3;

        hence contradiction by Def1;

      end;

      let Y;

      assume that

       A4: Y in I and

       A5: Y in ( dual I);

      (Y ` ) in I by A5, SETFAM_1:def 7;

      then ((Y ` ) \/ Y) in I by A4, Def2;

      then ( [#] X) in I by SUBSET_1: 10;

      hence contradiction by Def2;

    end;

    theorem :: CARD_FIL:11

    

     Th11: {} in I

    proof

      set Y = the Element of I;

       {} c= Y & {} c= X;

      hence thesis by Def2;

    end;

    definition

      let X, N, S;

      :: CARD_FIL:def3

      pred S is_multiplicative_with N means for S1 be non empty set st S1 c= S & ( card S1) in N holds ( meet S1) in S;

    end

    definition

      let X, N, S;

      :: CARD_FIL:def4

      pred S is_additive_with N means for S1 be non empty set st S1 c= S & ( card S1) in N holds ( union S1) in S;

    end

    notation

      let X, N, F;

      synonym F is_complete_with N for F is_multiplicative_with N;

    end

    notation

      let X, N, I;

      synonym I is_complete_with N for I is_additive_with N;

    end

    theorem :: CARD_FIL:12

    

     Th12: S is_multiplicative_with N implies ( dual S) is_additive_with N

    proof

      assume

       A1: S is_multiplicative_with N;

      deffunc F( Subset of X) = ($1 ` );

      let S1 be non empty set such that

       A2: S1 c= ( dual S) and

       A3: ( card S1) in N;

      reconsider S2 = S1 as non empty Subset-Family of X by A2, XBOOLE_1: 1;

      set S3 = ( dual S2);

      

       A4: ( card { F(Y) : Y in S2 }) c= ( card S2) from TREES_2:sch 2;

      { (Y ` ) : Y in S2 } = S3 by Th9;

      then

       A5: ( card S3) in N by A3, A4, ORDINAL1: 12;

      

       A6: (( union S2) ` ) = (( [#] X) \ ( union S2))

      .= ( meet S3) by SETFAM_1: 33;

      S3 c= S by A2, SETFAM_1: 37;

      then ((( meet S3) ` ) ` ) in S by A1, A5;

      hence thesis by A6, SETFAM_1:def 7;

    end;

    definition

      let X, F;

      :: CARD_FIL:def5

      attr F is uniform means for Y holds Y in F implies ( card Y) = ( card X);

      :: CARD_FIL:def6

      attr F is principal means ex Y st Y in F & for Z holds Z in F implies Y c= Z;

      :: CARD_FIL:def7

      attr F is being_ultrafilter means

      : Def7: for Y holds Y in F or (X \ Y) in F;

    end

    definition

      let X, F, Z;

      :: CARD_FIL:def8

      func Extend_Filter (F,Z) -> non empty Subset-Family of X equals { Y : ex Y2 st (Y2 in { (Y1 /\ Z) : Y1 in F } & Y2 c= Y) };

      coherence

      proof

        defpred P[ set] means ex Y2 st (Y2 in { (Y1 /\ Z) : Y1 in F } & Y2 c= $1);

        set IT = { Y : P[Y] };

        X in F by Th5;

        then (X /\ Z) in { (Y1 /\ Z) : Y1 in F };

        then Z in { (Y1 /\ Z) : Y1 in F } by XBOOLE_1: 28;

        then

         A1: Z in { Y : ex Y2 st (Y2 in { (Y1 /\ Z) : Y1 in F } & Y2 c= Y) };

        IT is Subset-Family of X from DOMAIN_1:sch 7;

        hence thesis by A1;

      end;

    end

    theorem :: CARD_FIL:13

    

     Th13: for Z1 holds (Z1 in ( Extend_Filter (F,Z)) iff ex Z2 st Z2 in F & (Z2 /\ Z) c= Z1)

    proof

      let Z1;

      thus Z1 in ( Extend_Filter (F,Z)) implies ex Z2 st Z2 in F & (Z2 /\ Z) c= Z1

      proof

        defpred P[ set] means ex Y2 st (Y2 in { (Y1 /\ Z) : Y1 in F } & Y2 c= $1);

        assume Z1 in ( Extend_Filter (F,Z));

        then

         A1: Z1 in { Y : P[Y] };

         P[Z1] from ElemProp( A1);

        then

        consider Y2 such that

         A2: Y2 in { (Y1 /\ Z) : Y1 in F } and

         A3: Y2 c= Z1;

        consider Y3 such that

         A4: Y2 = (Y3 /\ Z) and

         A5: Y3 in F by A2;

        take Y3;

        thus Y3 in F by A5;

        thus thesis by A3, A4;

      end;

      given Z2 such that

       A6: Z2 in F and

       A7: (Z2 /\ Z) c= Z1;

      ex Y2 st Y2 in { (Y1 /\ Z) : Y1 in F } & Y2 c= Z1

      proof

        take (Z2 /\ Z);

        thus (Z2 /\ Z) in { (Y1 /\ Z) : Y1 in F } by A6;

        thus thesis by A7;

      end;

      hence thesis;

    end;

    theorem :: CARD_FIL:14

    

     Th14: (for Y1 st Y1 in F holds Y1 meets Z) implies Z in ( Extend_Filter (F,Z)) & ( Extend_Filter (F,Z)) is Filter of X & F c= ( Extend_Filter (F,Z))

    proof

      assume

       A1: for Y1 st Y1 in F holds Y1 meets Z;

      X in F & (X /\ Z) c= Z by Th5, XBOOLE_1: 17;

      hence Z in ( Extend_Filter (F,Z)) by Th13;

      thus ( Extend_Filter (F,Z)) is Filter of X

      proof

        thus not {} in ( Extend_Filter (F,Z))

        proof

          assume {} in ( Extend_Filter (F,Z));

          then

          consider Z2 such that

           A2: Z2 in F and

           A3: (Z2 /\ Z) c= {} by Th13;

          Z2 meets Z by A1, A2;

          then (Z2 /\ Z) <> {} ;

          hence contradiction by A3;

        end;

        let Y1, Y2;

        thus Y1 in ( Extend_Filter (F,Z)) & Y2 in ( Extend_Filter (F,Z)) implies (Y1 /\ Y2) in ( Extend_Filter (F,Z))

        proof

          assume that

           A4: Y1 in ( Extend_Filter (F,Z)) and

           A5: Y2 in ( Extend_Filter (F,Z));

          consider Y3 such that

           A6: Y3 in F and

           A7: (Y3 /\ Z) c= Y1 by A4, Th13;

          consider Y4 such that

           A8: Y4 in F and

           A9: (Y4 /\ Z) c= Y2 by A5, Th13;

          ((Y3 /\ Z) /\ (Y4 /\ Z)) = (Y3 /\ (Z /\ (Y4 /\ Z))) by XBOOLE_1: 16

          .= (Y3 /\ (Y4 /\ (Z /\ Z))) by XBOOLE_1: 16

          .= ((Y3 /\ Y4) /\ Z) by XBOOLE_1: 16;

          then

           A10: ((Y3 /\ Y4) /\ Z) c= (Y1 /\ Y2) by A7, A9, XBOOLE_1: 27;

          (Y3 /\ Y4) in F by A6, A8, Def1;

          hence thesis by A10, Th13;

        end;

        thus Y1 in ( Extend_Filter (F,Z)) & Y1 c= Y2 implies Y2 in ( Extend_Filter (F,Z))

        proof

          

           A11: (X \ Z) misses Z by XBOOLE_1: 79;

          ((Y2 \/ (X \ Z)) /\ Z) = ((Y2 /\ Z) \/ ((X \ Z) /\ Z)) by XBOOLE_1: 23

          .= ((Y2 /\ Z) \/ {} ) by A11

          .= (Y2 /\ Z);

          then

           A12: ((Y2 \/ (X \ Z)) /\ Z) c= Y2 by XBOOLE_1: 17;

          assume that

           A13: Y1 in ( Extend_Filter (F,Z)) and

           A14: Y1 c= Y2;

          consider Y3 such that

           A15: Y3 in F and

           A16: (Y3 /\ Z) c= Y1 by A13, Th13;

          Y3 = ((Y3 /\ Z) \/ (Y3 \ Z)) & (Y3 \ Z) c= (X \ Z) by XBOOLE_1: 33, XBOOLE_1: 51;

          then

           A17: Y3 c= ((Y3 /\ Z) \/ (X \ Z)) by XBOOLE_1: 9;

          (Y3 /\ Z) c= Y2 by A14, A16;

          then ((Y3 /\ Z) \/ (X \ Z)) c= (Y2 \/ (X \ Z)) by XBOOLE_1: 9;

          then Y3 c= (Y2 \/ (X \ Z)) by A17;

          then (Y2 \/ (X \ Z)) in F by A15, Def1;

          hence thesis by A12, Th13;

        end;

      end;

      thus F c= ( Extend_Filter (F,Z))

      proof

        let Y be object;

        assume

         A18: Y in F;

        then

        reconsider Y as Subset of X;

        (Y /\ Z) c= Y by XBOOLE_1: 17;

        hence thesis by A18, Th13;

      end;

    end;

    reserve S,S1 for Subset-Family of X;

    definition

      let X;

      :: CARD_FIL:def9

      func Filters (X) -> non empty Subset-Family of ( bool X) equals { S where S be Subset-Family of X : S is Filter of X };

      coherence

      proof

        defpred P[ set] means $1 is Filter of X;

         {X} is Filter of X by Th4;

        then

         A1: {X} in { S : S is Filter of X };

        { S : P[S] } is Subset-Family of ( bool X) from DOMAIN_1:sch 7;

        hence thesis by A1;

      end;

    end

    theorem :: CARD_FIL:15

    

     Th15: for S be set holds S in ( Filters X) iff S is Filter of X

    proof

      let S be set;

      thus S in ( Filters X) implies S is Filter of X

      proof

        defpred P[ set] means $1 is Filter of X;

        assume S in ( Filters X);

        then

         A1: S in { S1 : P[S1] };

        thus P[S] from ElemProp( A1);

      end;

      assume S is Filter of X;

      hence thesis;

    end;

    reserve FS for non empty Subset of ( Filters X);

    theorem :: CARD_FIL:16

    

     Th16: FS is c=-linear implies ( union FS) is Filter of X

    proof

      

       A1: for S be set st S in FS holds S c= ( bool X)

      proof

        let S be set;

        assume S in FS;

        then S is Element of ( Filters X);

        hence thesis;

      end;

      consider S be object such that

       A2: S in FS by XBOOLE_0:def 1;

      assume

       A3: FS is c=-linear;

      

       A4: for Y1, Y2 holds (Y1 in ( union FS) & Y2 in ( union FS) implies (Y1 /\ Y2) in ( union FS)) & (Y1 in ( union FS) & Y1 c= Y2 implies Y2 in ( union FS))

      proof

        let Y1, Y2;

        thus Y1 in ( union FS) & Y2 in ( union FS) implies (Y1 /\ Y2) in ( union FS)

        proof

          assume that

           A5: Y1 in ( union FS) and

           A6: Y2 in ( union FS);

          consider S1 be set such that

           A7: Y1 in S1 and

           A8: S1 in FS by A5, TARSKI:def 4;

          

           A9: S1 is Filter of X by A8, Th15;

          consider S2 be set such that

           A10: Y2 in S2 and

           A11: S2 in FS by A6, TARSKI:def 4;

          

           A12: (S1,S2) are_c=-comparable by A3, A8, A11;

          

           A13: S2 is Filter of X by A11, Th15;

          per cases by A12;

            suppose S1 c= S2;

            then (Y1 /\ Y2) in S2 by A7, A10, A13, Def1;

            hence thesis by A11, TARSKI:def 4;

          end;

            suppose S2 c= S1;

            then (Y1 /\ Y2) in S1 by A7, A10, A9, Def1;

            hence thesis by A8, TARSKI:def 4;

          end;

        end;

        assume that

         A14: Y1 in ( union FS) and

         A15: Y1 c= Y2;

        consider S1 be set such that

         A16: Y1 in S1 and

         A17: S1 in FS by A14, TARSKI:def 4;

        S1 is Filter of X by A17, Th15;

        then Y2 in S1 by A15, A16, Def1;

        hence thesis by A17, TARSKI:def 4;

      end;

      

       A18: not {} in ( union FS)

      proof

        assume {} in ( union FS);

        then

        consider S be set such that

         A19: {} in S and

         A20: S in FS by TARSKI:def 4;

        S is Filter of X by A20, Th15;

        hence contradiction by A19, Def1;

      end;

      reconsider S as set by TARSKI: 1;

      S is Filter of X by A2, Th15;

      then X in S by Th5;

      then ( union FS) is non empty Subset-Family of X by A1, A2, TARSKI:def 4, ZFMISC_1: 76;

      hence thesis by A18, A4, Def1;

    end;

    theorem :: CARD_FIL:17

    

     Th17: for F holds ex Uf st F c= Uf & Uf is being_ultrafilter

    proof

      let F;

      set LargerF = { S : F c= S & S is Filter of X };

      

       A1: F in LargerF;

      { S : F c= S & S is Filter of X } c= ( Filters X)

      proof

        defpred P[ set] means F c= $1 & $1 is Filter of X;

        let F2 be object;

        reconsider FF = F2 as set by TARSKI: 1;

        assume F2 in { S : F c= S & S is Filter of X };

        then

         A2: FF in { S : P[S] };

         P[FF] from ElemProp( A2);

        hence thesis;

      end;

      then

      reconsider LargerF as non empty Subset of ( Filters X) by A1;

      defpred P[ set] means F c= $1 & $1 is Filter of X;

      for Z be set st Z c= LargerF & Z is c=-linear holds ex Y be set st Y in LargerF & for X1 be set st X1 in Z holds X1 c= Y

      proof

        let X1 be set;

        assume that

         A3: X1 c= LargerF and

         A4: X1 is c=-linear;

        per cases ;

          suppose

           A5: X1 = {} ;

          take F;

          thus thesis by A5;

        end;

          suppose X1 is non empty;

          then

          reconsider X2 = X1 as non empty Subset of ( Filters X) by A3, XBOOLE_1: 1;

          

           A6: F c= ( union X2)

          proof

            defpred P[ set] means F c= $1 & $1 is Filter of X;

            consider F1 be object such that

             A7: F1 in X2 by XBOOLE_0:def 1;

            reconsider F1 as set by TARSKI: 1;

            

             A8: F1 in { S : P[S] } by A3, A7;

            

             A9: P[F1] from ElemProp( A8);

            F1 c= ( union X2) by A7, ZFMISC_1: 74;

            hence thesis by A9;

          end;

          ( union X2) is Filter of X by A4, Th16;

          then ( union X2) in { S : F c= S & S is Filter of X } by A6;

          then

          reconsider MF = ( union X2) as Element of LargerF;

          take MF;

          thus thesis by ZFMISC_1: 74;

        end;

      end;

      then

      consider Uf1 be set such that

       A10: Uf1 in LargerF and

       A11: for Z be set st Z in LargerF & Z <> Uf1 holds not Uf1 c= Z by ORDERS_1: 65;

      reconsider Uf1 as Element of LargerF by A10;

      reconsider Uf = Uf1 as Filter of X by Th15;

      take Uf;

      

       A12: Uf in { S : P[S] };

      

       A13: P[Uf] from ElemProp( A12);

      hence F c= Uf;

      thus Uf is being_ultrafilter

      proof

        let Z;

        per cases ;

          suppose Z in Uf;

          hence thesis;

        end;

          suppose

           A14: not Z in Uf;

          (X \ Z) in Uf

          proof

            assume

             A15: not (X \ Z) in Uf;

            

             A16: for Y1 st Y1 in Uf holds Y1 meets Z

            proof

              let Y1;

              assume

               A17: Y1 in Uf;

              assume Y1 misses Z;

              then Y1 = (Y1 \ Z) by XBOOLE_1: 83;

              then Y1 c= (X \ Z) by XBOOLE_1: 33;

              hence contradiction by A15, A17, Def1;

            end;

            then

             A18: ( Extend_Filter (Uf,Z)) is Filter of X by Th14;

            

             A19: Z in ( Extend_Filter (Uf,Z)) by A16, Th14;

            

             A20: Uf c= ( Extend_Filter (Uf,Z)) by A16, Th14;

            then F c= ( Extend_Filter (Uf,Z)) by A13;

            then ( Extend_Filter (Uf,Z)) in LargerF by A18;

            hence contradiction by A11, A14, A20, A19;

          end;

          hence thesis;

        end;

      end;

    end;

    reserve X for infinite set;

    reserve Y,Y1,Y2,Z for Subset of X;

    reserve F,Uf for Filter of X;

    definition

      let X;

      :: CARD_FIL:def10

      func Frechet_Filter (X) -> Filter of X equals { Y : ( card (X \ Y)) in ( card X) };

      coherence

      proof

        defpred P[ set] means ( card (X \ $1)) in ( card X);

        set IT = { Y : P[Y] };

        

         A1: IT is Subset-Family of X from DOMAIN_1:sch 7;

        ( card (X \ X)) = ( card {} ) by XBOOLE_1: 37

        .= 0 ;

        then

         A2: ( card (X \ X)) in ( card X) by ORDINAL3: 8;

        X c= X;

        then X in IT by A2;

        then

        reconsider IT as non empty Subset-Family of X by A1;

        

         A3: for Y1 st Y1 in IT holds ( card (X \ Y1)) in ( card X)

        proof

          let Y1;

          assume Y1 in IT;

          then

           A4: Y1 in { Y : P[Y] };

          thus P[Y1] from ElemProp( A4);

        end;

        IT is Filter of X

        proof

          thus not {} in IT

          proof

            assume {} in IT;

            then ( card (X \ {} )) in ( card X) by A3;

            hence contradiction;

          end;

          let Y1, Y2;

          thus Y1 in IT & Y2 in IT implies (Y1 /\ Y2) in IT

          proof

            assume Y1 in IT & Y2 in IT;

            then ( card (X \ Y1)) in ( card X) & ( card (X \ Y2)) in ( card X) by A3;

            then (( card (X \ Y1)) +` ( card (X \ Y2))) in (( card X) +` ( card X)) by CARD_2: 96;

            then

             A5: (( card (X \ Y1)) +` ( card (X \ Y2))) in ( card X) by CARD_2: 75;

            ( card (X \ (Y1 /\ Y2))) = ( card ((X \ Y1) \/ (X \ Y2))) by XBOOLE_1: 54;

            then ( card (X \ (Y1 /\ Y2))) in ( card X) by A5, CARD_2: 34, ORDINAL1: 12;

            hence thesis;

          end;

          thus Y1 in IT & Y1 c= Y2 implies Y2 in IT

          proof

            assume Y1 in IT & Y1 c= Y2;

            then ( card (X \ Y1)) in ( card X) & (X \ Y2) c= (X \ Y1) by A3, XBOOLE_1: 34;

            then ( card (X \ Y2)) in ( card X) by CARD_1: 11, ORDINAL1: 12;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let X;

      :: CARD_FIL:def11

      func Frechet_Ideal (X) -> Ideal of X equals ( dual ( Frechet_Filter X));

      coherence ;

    end

    theorem :: CARD_FIL:18

    

     Th18: Y in ( Frechet_Filter X) iff ( card (X \ Y)) in ( card X)

    proof

      thus Y in ( Frechet_Filter X) implies ( card (X \ Y)) in ( card X)

      proof

        defpred P[ set] means ( card (X \ $1)) in ( card X);

        assume Y in ( Frechet_Filter X);

        then

         A1: Y in { Y1 : P[Y1] };

        thus P[Y] from ElemProp( A1);

      end;

      thus thesis;

    end;

    theorem :: CARD_FIL:19

    

     Th19: Y in ( Frechet_Ideal X) iff ( card Y) in ( card X)

    proof

      Y in ( Frechet_Ideal X) iff (Y ` ) in ( Frechet_Filter X) by SETFAM_1:def 7;

      then Y in ( Frechet_Ideal X) iff ( card ((Y ` ) ` )) in ( card X) by Th18;

      hence thesis;

    end;

    theorem :: CARD_FIL:20

    

     Th20: ( Frechet_Filter X) c= F implies F is uniform

    proof

      assume

       A1: ( Frechet_Filter X) c= F;

      let Y;

      assume Y in F;

      then not (X \ Y) in ( Frechet_Filter X) by A1, Th6;

      then

       A2: not ( card (X \ (X \ Y))) in ( card X);

      

       A3: ( card Y) c= ( card X) by CARD_1: 11;

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

      .= Y by XBOOLE_1: 28;

      then ( card X) c= ( card Y) by A2, CARD_1: 4;

      hence thesis by A3;

    end;

    theorem :: CARD_FIL:21

    Uf is uniform being_ultrafilter implies ( Frechet_Filter X) c= Uf

    proof

      assume

       A1: Uf is uniform being_ultrafilter;

      thus ( Frechet_Filter X) c= Uf

      proof

        let Y be object;

        reconsider YY = Y as set by TARSKI: 1;

        assume

         A2: Y in ( Frechet_Filter X);

        then ( card (X \ YY)) in ( card X) by Th18;

        then ( card (X \ YY)) <> ( card X);

        then not (X \ YY) in Uf by A1;

        hence thesis by A1, A2;

      end;

    end;

    registration

      let X;

      cluster non principal being_ultrafilter for Filter of X;

      existence

      proof

        consider Uf be Filter of X such that

         A1: ( Frechet_Filter X) c= Uf and

         A2: Uf is being_ultrafilter by Th17;

        take Uf;

        

         A3: Uf is uniform by A1, Th20;

        Uf is non principal

        proof

          assume Uf is principal;

          then

          consider Y such that

           A4: Y in Uf and

           A5: for Z holds Z in Uf implies Y c= Z;

          

           A6: for x be Element of X holds (X \ {x}) in Uf

          proof

            let x be Element of X;

            

             A7: ( card X) <> ( card {x});

             {x} is finite Subset of X by SUBSET_1: 33;

            then

             A8: (X \ {x}) in Uf or {x} in Uf by A2;

            assume not (X \ {x}) in Uf;

            hence contradiction by A3, A8, A7;

          end;

          

           A9: for x be Element of X holds not x in Y

          proof

            let x be Element of X;

            assume

             A10: x in Y;

            Y c= (X \ {x}) by A5, A6;

            then not x in {x} by A10, XBOOLE_0:def 5;

            hence contradiction by TARSKI:def 1;

          end;

          Y = {}

          proof

            assume Y <> {} ;

            then ex x be object st x in Y by XBOOLE_0:def 1;

            hence contradiction by A9;

          end;

          hence contradiction by A4, Def1;

        end;

        hence thesis by A2;

      end;

    end

    registration

      let X;

      cluster uniform being_ultrafilter -> non principal for Filter of X;

      coherence

      proof

        let F;

        assume

         A1: F is uniform being_ultrafilter;

        assume F is principal;

        then

        consider Y such that

         A2: Y in F and

         A3: for Z holds Z in F implies Y c= Z;

        Y = {}

        proof

          assume Y <> {} ;

          then

          consider x be object such that

           A4: x in Y by XBOOLE_0:def 1;

          

           A5: for Z holds Z in F implies x in Z

          proof

            let Z;

            assume Z in F;

            then Y c= Z by A3;

            hence thesis by A4;

          end;

          ( card {x}) in ( card X) by CARD_3: 86;

          then

           A6: not {x} in F by A1;

           {x} is Subset of X by A4, SUBSET_1: 33;

          then (X \ {x}) in F by A1, A6;

          then x in (X \ {x}) by A5;

          then not x in {x} by XBOOLE_0:def 5;

          hence contradiction by TARSKI:def 1;

        end;

        hence contradiction by A2, Def1;

      end;

    end

    theorem :: CARD_FIL:22

    

     Th22: for F be being_ultrafilter Filter of X holds for Y holds Y in F iff not Y in ( dual F)

    proof

      let F be being_ultrafilter Filter of X;

      let Y;

      thus Y in F implies not Y in ( dual F)

      proof

        assume Y in F;

        then not (Y ` ) in F by Th6;

        hence thesis by SETFAM_1:def 7;

      end;

      assume not Y in ( dual F);

      then not (Y ` ) in F by SETFAM_1:def 7;

      hence thesis by Def7;

    end;

    reserve x for Element of X;

    theorem :: CARD_FIL:23

    

     Th23: F is non principal being_ultrafilter & F is_complete_with ( card X) implies F is uniform

    proof

      defpred P[ object, object] means ex A be set st A = $2 & not $1 in A & $2 in F;

      assume

       A1: F is non principal being_ultrafilter;

      

       A2: for x be object st x in X holds ex Z be object st Z in F & P[x, Z]

      proof

        let x be object;

        assume x in X;

        then

         A3: {x} is Subset of X by SUBSET_1: 33;

        assume

         A4: for Z be object st Z in F holds not P[x, Z];

         not (X \ {x}) in F

        proof

          assume (X \ {x}) in F;

          then x in (X \ {x}) by A4;

          then not x in {x} by XBOOLE_0:def 5;

          hence contradiction by TARSKI:def 1;

        end;

        then

         A5: {x} in F by A1, A3;

        for Z st Z in F holds {x} c= Z by A4, ZFMISC_1: 31;

        hence contradiction by A1, A5;

      end;

      consider h be Function such that

       A6: ( dom h) = X and ( rng h) c= F and

       A7: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A2);

      assume

       A8: F is_complete_with ( card X);

      assume not F is uniform;

      then

      consider Y such that

       A9: Y in F and

       A10: not ( card Y) = ( card X);

      

       A11: { (h . x) : x in Y } c= F

      proof

        let y be object;

        assume y in { (h . x) : x in Y };

        then

        consider x such that

         A12: y = (h . x) & x in Y;

         P[x, (h . x)] by A7;

        then ex B be set st B = (h . x) & not x in B & (h . x) in F;

        hence thesis by A12;

      end;

      for y be object holds not y in (Y /\ ( meet { (h . x) : x in Y }))

      proof

        let y be object such that

         A13: y in (Y /\ ( meet { (h . x) : x in Y }));

        y in Y by A13, XBOOLE_0:def 4;

        then

         A14: (h . y) in { (h . x) : x in Y };

        now

          assume

           A15: y in (h . y);

           P[y, (h . y)] by A7, A13;

          then

          consider A be set such that

           A16: A = (h . y) & not y in A & (h . y) in F;

           not y in (h . y) & (h . y) in F by A16;

          hence contradiction by A15;

        end;

        then not y in ( meet { (h . x) : x in Y }) by A14, SETFAM_1:def 1;

        hence contradiction by A13, XBOOLE_0:def 4;

      end;

      then

       A17: (Y /\ ( meet { (h . x) : x in Y })) = {} by XBOOLE_0:def 1;

      

       A18: Y is non empty by A9, Def1;

      

       A19: { (h . x) : x in Y } is non empty

      proof

        set y = the Element of Y;

        y in Y by A18;

        then (h . y) in { (h . x) : x in Y };

        hence thesis;

      end;

      { (h . x) : x in Y } c= (h .: Y)

      proof

        let y be object;

        assume y in { (h . x) : x in Y };

        then ex x st y = (h . x) & x in Y;

        hence thesis by A6, FUNCT_1:def 6;

      end;

      then

       A20: ( card { (h . x) : x in Y }) c= ( card Y) by CARD_1: 66;

      ( card Y) c= ( card X) by CARD_1: 11;

      then ( card Y) in ( card X) by A10, CARD_1: 3;

      then ( card { (h . x) : x in Y }) in ( card X) by A20, ORDINAL1: 12;

      then ( meet { (h . x) : x in Y }) in F by A8, A11, A19;

      then {} in F by A9, A17, Def1;

      hence contradiction by Def1;

    end;

    begin

    theorem :: CARD_FIL:24

    

     Th24: ( nextcard N) c= ( exp (2,N))

    proof

      ( card N) in ( exp (2,N)) by CARD_5: 14;

      hence thesis by CARD_1:def 3;

    end;

    definition

      :: CARD_FIL:def12

      pred GCH means for N be Aleph holds ( nextcard N) = ( exp (2,N));

    end

    definition

      let IT be Aleph;

      :: CARD_FIL:def13

      attr IT is inaccessible means IT is regular limit_cardinal;

    end

    registration

      cluster inaccessible -> regular limit_cardinal for Aleph;

      coherence ;

    end

    theorem :: CARD_FIL:25

     omega is inaccessible by CARD_5: 30;

    definition

      let IT be Aleph;

      :: CARD_FIL:def14

      attr IT is strong_limit means for N st N in IT holds ( exp (2,N)) in IT;

    end

    theorem :: CARD_FIL:26

    

     Th26: omega is strong_limit

    proof

      let N;

      assume N in omega ;

      then ( card ( bool N)) is finite;

      then ( exp (2,( card N))) is finite by CARD_2: 31;

      then ( exp (2,N)) is finite;

      hence thesis by CARD_1: 61;

    end;

    theorem :: CARD_FIL:27

    

     Th27: M is strong_limit implies M is limit_cardinal

    proof

      assume

       A1: M is strong_limit;

      assume not M is limit_cardinal;

      then

      consider N such that

       A2: M = ( nextcard N);

      M c= ( exp (2,N)) by A2, Th24;

      then

       A3: not ( exp (2,N)) in M by CARD_1: 4;

      N in M by A2, CARD_1: 18;

      hence contradiction by A1, A3;

    end;

    registration

      cluster strong_limit -> limit_cardinal for Aleph;

      coherence by Th27;

    end

    theorem :: CARD_FIL:28

    

     Th28: GCH implies (M is limit_cardinal implies M is strong_limit)

    proof

      assume

       A1: GCH ;

      assume

       A2: M is limit_cardinal;

      assume not M is strong_limit;

      then

      consider N be Cardinal such that

       A3: N in M and

       A4: not ( exp (2,N)) in M;

      

       A5: ( nextcard N) c= M by A3, CARD_3: 90;

      

       A6: N is infinite

      proof

        assume N is finite;

        then ( Funcs (N,2)) is finite by FRAENKEL: 6;

        then ( card ( Funcs (N,2))) is finite;

        then ( exp (2,N)) is finite by CARD_2:def 3;

        hence thesis by A4, CARD_3: 86;

      end;

      M c= ( exp (2,N)) by A4, CARD_1: 4;

      then M c= ( nextcard N) by A1, A6;

      then ( nextcard N) = M by A5;

      hence contradiction by A2;

    end;

    definition

      let IT be Aleph;

      :: CARD_FIL:def15

      attr IT is strongly_inaccessible means IT is regular strong_limit;

    end

    registration

      cluster strongly_inaccessible -> regular strong_limit for Aleph;

      coherence ;

    end

    theorem :: CARD_FIL:29

     omega is strongly_inaccessible by Th26, CARD_5: 30;

    theorem :: CARD_FIL:30

    M is strongly_inaccessible implies M is inaccessible;

    registration

      cluster strongly_inaccessible -> inaccessible for Aleph;

      coherence ;

    end

    theorem :: CARD_FIL:31

     GCH implies (M is inaccessible implies M is strongly_inaccessible) by Th28;

    definition

      let M;

      :: CARD_FIL:def16

      attr M is measurable means ex Uf be Filter of M st Uf is_complete_with M & Uf is non principal being_ultrafilter;

    end

    theorem :: CARD_FIL:32

    

     Th32: for A be limit_ordinal Ordinal holds for X be set st X c= A holds ( sup X) = A implies ( union X) = A

    proof

      let A be limit_ordinal Ordinal;

      let X be set;

      assume X c= A;

      then

       A1: ( union X) c= ( union A) by ZFMISC_1: 77;

      assume

       A2: ( sup X) = A;

      thus ( union X) c= A by A1, ORDINAL1:def 6;

      thus A c= ( union X)

      proof

        let X1 be object such that

         A3: X1 in A;

        reconsider X2 = X1 as Ordinal by A3;

        ( succ X2) in A by A3, ORDINAL1: 28;

        then

         A4: ex B be Ordinal st B in X & ( succ X2) c= B by A2, ORDINAL2: 21;

        X2 in ( succ X2) by ORDINAL1: 6;

        hence thesis by A4, TARSKI:def 4;

      end;

    end;

    theorem :: CARD_FIL:33

    

     Th33: M is measurable implies M is regular

    proof

      

       A1: ( cf M) c= M by CARD_5:def 1;

      assume M is measurable;

      then

      consider Uf be Filter of M such that

       A2: Uf is_complete_with M and

       A3: Uf is non principal being_ultrafilter;

      assume not M is regular;

      then ( cf M) <> M by CARD_5:def 3;

      then

       A4: ( cf M) in M by A1, CARD_1: 3;

      then

      consider xi be Ordinal-Sequence such that

       A5: ( dom xi) = ( cf M) and

       A6: ( rng xi) c= M and xi is increasing and

       A7: M = ( sup xi) and xi is Cardinal-Function and not 0 in ( rng xi) by CARD_5: 29;

      M = ( sup ( rng xi)) by A7, ORDINAL2:def 5;

      then

       A8: M = ( union ( rng xi)) by A6, Th32;

      Uf is_complete_with ( card M) by A2;

      then

       A9: Uf is uniform by A3, Th23;

      

       A10: ( rng xi) c= ( dual Uf)

      proof

        let X be object such that

         A11: X in ( rng xi);

        reconsider X1 = X as Subset of M by A6, A11, ORDINAL1:def 2;

        

         A12: ( card X1) in M by A6, A11, CARD_1: 9;

         not X1 in Uf

        proof

          assume X1 in Uf;

          then ( card X1) = ( card M) by A9;

          then ( card X1) = M;

          hence contradiction by A12;

        end;

        hence thesis by A3, Th22;

      end;

      ( card ( rng xi)) c= ( card ( dom xi)) by CARD_2: 61;

      then ( card ( rng xi)) c= ( cf M) by A5;

      then

       A13: ( card ( rng xi)) in M by A4, ORDINAL1: 12;

      ( dual Uf) is_complete_with M by A2, Th12;

      then ( union ( rng xi)) in ( dual Uf) by A8, A13, A10, ZFMISC_1: 2;

      hence contradiction by A8, Def2;

    end;

    registration

      let M;

      cluster ( nextcard M) -> non limit_cardinal;

      coherence ;

    end

    registration

      cluster non limit_cardinal infinite for Cardinal;

      existence

      proof

        take ( aleph ( succ 0 ));

        ( aleph ( succ 0 )) = ( nextcard omega ) by CARD_1: 19, CARD_1: 46;

        hence thesis;

      end;

    end

    registration

      cluster non limit_cardinal -> regular for Aleph;

      coherence

      proof

        let M such that

         A1: M is non limit_cardinal;

        assume not M is regular;

        then

         A2: ( cf M) <> M by CARD_5:def 3;

        ( cf M) c= M by CARD_5:def 1;

        then ( cf M) in M by A2, CARD_1: 3;

        hence contradiction by A1, CARD_5: 28;

      end;

    end

    definition

      let M be non limit_cardinal Cardinal;

      :: CARD_FIL:def17

      func predecessor M -> Cardinal means

      : Def17: M = ( nextcard it );

      existence by CARD_1:def 4;

      uniqueness by CARD_3: 89;

    end

    registration

      let M be non limit_cardinal Aleph;

      cluster ( predecessor M) -> infinite;

      coherence

      proof

        assume

         A1: ( predecessor M) is finite;

        M = ( nextcard ( predecessor M)) by Def17;

        hence contradiction by A1, CARD_1: 45;

      end;

    end

    definition

      let X be set;

      let N,N1 be Cardinal;

      mode Inf_Matrix of N,N1,X is Function of [:N, N1:], X;

    end

    reserve X for set;

    reserve M for non limit_cardinal Aleph;

    reserve F for Filter of M;

    reserve N1,N2,N3 for Element of ( predecessor M);

    reserve K1,K2 for Element of M;

    reserve T for Inf_Matrix of ( predecessor M), M, ( bool M);

    definition

      let M, T;

      :: CARD_FIL:def18

      pred T is_Ulam_Matrix_of M means (for N1, K1, K2 holds K1 <> K2 implies ((T . (N1,K1)) /\ (T . (N1,K2))) is empty) & (for K1, N1, N2 holds N1 <> N2 implies ((T . (N1,K1)) /\ (T . (N2,K1))) is empty) & (for N1 holds ( card (M \ ( union { (T . (N1,K1)) : K1 in M }))) c= ( predecessor M)) & for K1 holds ( card (M \ ( union { (T . (N1,K1)) : N1 in ( predecessor M) }))) c= ( predecessor M);

    end

    theorem :: CARD_FIL:34

    

     Th34: ex T st T is_Ulam_Matrix_of M

    proof

      set N = ( predecessor M);

      set GT = (( nextcard N) \ N);

      defpred P[ object, object] means ex f be Function st $2 = f & f is one-to-one & ( dom f) = N & ( rng f) = $1;

      

       A1: for K1 be object st K1 in GT holds ex x be object st x in ( Funcs (N,( nextcard N))) & P[K1, x]

      proof

        let K1 be object such that

         A2: K1 in (( nextcard N) \ N);

        reconsider K2 = K1 as Element of ( nextcard N) by A2;

         not K1 in N by A2, XBOOLE_0:def 5;

        then ( card N) c= ( card K2) by CARD_1: 11, ORDINAL1: 16;

        then

         A3: N c= ( card K2);

        ( card K2) in ( nextcard N) by CARD_1: 9;

        then ( card K2) c= N by CARD_3: 91;

        

        then ( card K2) = N by A3

        .= ( card N);

        then (K2,N) are_equipotent by CARD_1: 5;

        then

        consider f be Function such that

         A4: f is one-to-one and

         A5: ( dom f) = N and

         A6: ( rng f) = K1 by WELLORD2:def 4;

        ( rng f) c= ( nextcard N) by A2, A6, ORDINAL1:def 2;

        then f in ( Funcs (N,( nextcard N))) by A5, FUNCT_2:def 2;

        hence thesis by A4, A5, A6;

      end;

      consider h1 be Function such that

       A7: ( dom h1) = GT and ( rng h1) c= ( Funcs (N,( nextcard N))) and

       A8: for K1 be object st K1 in GT holds P[K1, (h1 . K1)] from FUNCT_1:sch 6( A1);

      for K1 be object st K1 in ( dom h1) holds (h1 . K1) is Function

      proof

        let K1 be object;

        assume K1 in ( dom h1);

        then ex f be Function st (h1 . K1) = f & f is one-to-one & ( dom f) = N & ( rng f) = K1 by A7, A8;

        hence thesis;

      end;

      then

      reconsider h = h1 as Function-yielding Function by FUNCOP_1:def 6;

      N in ( nextcard N) & not N in N by CARD_1: 18;

      then

      reconsider GT1 = (( nextcard N) \ N) as non empty set by XBOOLE_0:def 5;

      deffunc g( set, set) = ((h . $2) . $1);

      defpred P[ set, set, set] means $3 = { K2 where K2 be Element of GT1 : g($1,K2) = $2 };

      

       A9: for N1, K1 holds ex S1 be Subset of GT1 st P[N1, K1, S1]

      proof

        let N1, K1;

        defpred P[ set] means g(N1,$1) = K1;

        take { K2 where K2 be Element of GT1 : g(N1,K2) = K1 };

        { K2 where K2 be Element of GT1 : P[K2] } is Subset of GT1 from DOMAIN_1:sch 7;

        hence thesis;

      end;

      consider T1 be Function of [:( predecessor M), M:], ( bool GT1) such that

       A10: for N1, K1 holds P[N1, K1, (T1 . (N1,K1))] from BINOP_1:sch 3( A9);

      GT1 c= ( nextcard N);

      then GT1 c= M by Def17;

      then ( bool GT1) c= ( bool M) by ZFMISC_1: 67;

      then

      reconsider T = T1 as Function of [:( predecessor M), M:], ( bool M) by FUNCT_2: 7;

      take T;

      

       A11: for N1, N2, K1, K2 holds for K3 be set holds K3 in ((T . (N1,K1)) /\ (T . (N2,K2))) implies ex K4 be Element of GT1 st K4 = K3 & g(N1,K4) = K1 & g(N2,K4) = K2

      proof

        let N1, N2, K1, K2;

        let K3 be set;

        defpred A[ Element of GT1] means g(N1,$1) = K1;

        defpred B[ Element of GT1] means g(N2,$1) = K2;

        assume

         A12: K3 in ((T . (N1,K1)) /\ (T . (N2,K2)));

        then

         A13: K3 in (T1 . (N1,K1)) by XBOOLE_0:def 4;

        then

        reconsider K4 = K3 as Element of GT1;

        take K4;

        thus K4 = K3;

        

         A14: K4 in { K5 where K5 be Element of GT1 : A[K5] } by A10, A13;

        thus A[K4] from ElemProp( A14);

        K3 in (T1 . (N2,K2)) by A12, XBOOLE_0:def 4;

        then

         A15: K4 in { K5 where K5 be Element of GT1 : B[K5] } by A10;

        thus B[K4] from ElemProp( A15);

      end;

      thus for N1, K1, K2 holds K1 <> K2 implies ((T . (N1,K1)) /\ (T . (N1,K2))) is empty

      proof

        let N1, K1, K2;

        assume

         A16: K1 <> K2;

        assume not ((T . (N1,K1)) /\ (T . (N1,K2))) is empty;

        then

        consider K3 be object such that

         A17: K3 in ((T . (N1,K1)) /\ (T . (N1,K2)));

        ex K4 be Element of GT1 st K4 = K3 & g(N1,K4) = K1 & g(N1,K4) = K2 by A11, A17;

        hence contradiction by A16;

      end;

      thus for K1, N1, N2 holds N1 <> N2 implies ((T . (N1,K1)) /\ (T . (N2,K1))) is empty

      proof

        let K1, N1, N2;

        assume

         A18: N1 <> N2;

        assume not ((T . (N1,K1)) /\ (T . (N2,K1))) is empty;

        then

        consider K3 be object such that

         A19: K3 in ((T . (N1,K1)) /\ (T . (N2,K1)));

        consider K4 be Element of GT1 such that K4 = K3 and

         A20: g(N1,K4) = K1 & g(N2,K4) = K1 by A11, A19;

        ex f be Function st (h1 . K4) = f & f is one-to-one & ( dom f) = N & ( rng f) = K4 by A8;

        hence contradiction by A18, A20;

      end;

      

       A21: for N1 holds for K1 be Element of GT1 holds ( dom (h . K1)) = N & ( rng (h . K1)) = K1

      proof

        let N1;

        let K1 be Element of GT1;

        ex f be Function st (h1 . K1) = f & f is one-to-one & ( dom f) = N & ( rng f) = K1 by A8;

        hence thesis;

      end;

      thus for N1 holds ( card (M \ ( union { (T . (N1,K1)) : K1 in M }))) c= N

      proof

        let N1;

        ( union { (T . (N1,K1)) : K1 in M }) = GT1

        proof

          for S1 be set st S1 in { (T . (N1,K1)) : K1 in M } holds S1 c= GT1

          proof

            let S1 be set;

            assume S1 in { (T . (N1,K1)) : K1 in M };

            then

            consider K1 such that

             A22: S1 = (T . (N1,K1)) and K1 in M;

            (T1 . (N1,K1)) c= GT1;

            hence thesis by A22;

          end;

          hence ( union { (T . (N1,K1)) : K1 in M }) c= GT1 by ZFMISC_1: 76;

          let K2 be object such that

           A23: K2 in GT1;

          reconsider K5 = K2 as Element of GT1 by A23;

          N1 in N;

          then N1 in ( dom (h . K5)) by A21;

          then ((h . K5) . N1) in ( rng (h . K5)) by FUNCT_1:def 3;

          then

           A24: g(N1,K5) in K5 by A21;

          K2 in ( nextcard N) by A23;

          then K2 in M by Def17;

          then

           A25: K5 c= M by ORDINAL1:def 2;

          then

           A26: (T . (N1, g(N1,K5))) in { (T . (N1,K1)) : K1 in M } by A24;

          K5 in { K3 where K3 be Element of GT1 : g(N1,K3) = g(N1,K5) };

          then K5 in (T . (N1, g(N1,K5))) by A10, A25, A24;

          hence thesis by A26, TARSKI:def 4;

        end;

        then ( union { (T . (N1,K1)) : K1 in M }) = (M \ N) by Def17;

        then (M \ ( union { (T . (N1,K1)) : K1 in M })) = (M /\ N) by XBOOLE_1: 48;

        hence thesis by CARD_1: 7, XBOOLE_1: 17;

      end;

      thus for K1 holds ( card (M \ ( union { (T . (N1,K1)) : N1 in N }))) c= N

      proof

        let K1;

        

         A27: N c= K1 implies ( card K1) = N

        proof

          assume N c= K1;

          then ( card N) c= ( card K1) by CARD_1: 11;

          then

           A28: N c= ( card K1);

          ( card K1) in M by CARD_1: 9;

          then ( card K1) in ( nextcard N) by Def17;

          then ( card K1) c= N by CARD_3: 91;

          hence thesis by A28;

        end;

        

         A29: ( card (M \ { K5 where K5 be Element of GT1 : K1 in K5 })) c= N

        proof

          per cases by ORDINAL1: 16;

            suppose

             A30: N c= K1;

            (M \ (K1 \/ {K1})) c= { K5 where K5 be Element of GT1 : K1 in K5 }

            proof

              let K6 be object such that

               A31: K6 in (M \ (K1 \/ {K1}));

              reconsider K7 = K6 as Element of M by A31;

              

               A32: not K6 in (K1 \/ {K1}) by A31, XBOOLE_0:def 5;

              then not K6 in {K1} by XBOOLE_0:def 3;

              then

               A33: not K6 = K1 by TARSKI:def 1;

              K7 in M;

              then

               A34: K7 in ( nextcard N) by Def17;

               not K6 in K1 by A32, XBOOLE_0:def 3;

              then

               A35: K1 in K7 by A33, ORDINAL1: 14;

              then N in K7 by A30, ORDINAL1: 12;

              then

              reconsider K8 = K7 as Element of GT1 by A34, XBOOLE_0:def 5;

              K8 in { K5 where K5 be Element of GT1 : K1 in K5 } by A35;

              hence thesis;

            end;

            then (M \ { K5 where K5 be Element of GT1 : K1 in K5 }) c= (M \ (M \ (K1 \/ {K1}))) by XBOOLE_1: 34;

            then

             A36: (M \ { K5 where K5 be Element of GT1 : K1 in K5 }) c= (M /\ (K1 \/ {K1})) by XBOOLE_1: 48;

             not K1 is finite by A30;

            then

             A37: ( card (K1 \/ {K1})) = ( card K1) by CARD_2: 78;

            (M /\ (K1 \/ {K1})) c= (K1 \/ {K1}) by XBOOLE_1: 17;

            then (M \ { K5 where K5 be Element of GT1 : K1 in K5 }) c= (K1 \/ {K1}) by A36;

            hence thesis by A27, A30, A37, CARD_1: 11;

          end;

            suppose

             A38: K1 in N;

            { K5 where K5 be Element of GT1 : K1 in K5 } = GT1

            proof

              defpred P[ set] means K1 in $1;

              { K5 where K5 be Element of GT1 : P[K5] } is Subset of GT1 from DOMAIN_1:sch 7;

              hence { K5 where K5 be Element of GT1 : K1 in K5 } c= GT1;

              let K6 be object such that

               A39: K6 in GT1;

              reconsider K7 = K6 as Element of ( nextcard N) by A39;

              reconsider K8 = K7 as Element of GT1 by A39;

               not K6 in N by A39, XBOOLE_0:def 5;

              then N c= K7 by ORDINAL1: 16;

              then K8 in { K5 where K5 be Element of GT1 : K1 in K5 } by A38;

              hence thesis;

            end;

            

            then (M \ { K5 where K5 be Element of GT1 : K1 in K5 }) = (M \ (M \ N)) by Def17

            .= (M /\ N) by XBOOLE_1: 48;

            hence thesis by CARD_1: 7, XBOOLE_1: 17;

          end;

        end;

        { K5 where K5 be Element of GT1 : K1 in K5 } c= ( union { (T . (N1,K1)) : N1 in N })

        proof

          let K4 be object;

          assume K4 in { K5 where K5 be Element of GT1 : K1 in K5 };

          then

          consider K5 be Element of GT1 such that

           A40: K4 = K5 and

           A41: K1 in K5;

          ( rng (h . K5)) = K5 by A21;

          then

          consider N2 be object such that

           A42: N2 in ( dom (h . K5)) and

           A43: ((h . K5) . N2) = K1 by A41, FUNCT_1:def 3;

          reconsider N3 = N2 as Element of N by A21, A42;

          K5 in { K3 where K3 be Element of GT1 : g(N3,K3) = K1 } by A43;

          then

           A44: K5 in (T . (N3,K1)) by A10;

          (T . (N3,K1)) in { (T . (N1,K1)) : N1 in N };

          hence thesis by A40, A44, TARSKI:def 4;

        end;

        then (M \ ( union { (T . (N1,K1)) : N1 in N })) c= (M \ { K5 where K5 be Element of GT1 : K1 in K5 }) by XBOOLE_1: 34;

        then ( card (M \ ( union { (T . (N1,K1)) : N1 in N }))) c= ( card (M \ { K5 where K5 be Element of GT1 : K1 in K5 })) by CARD_1: 11;

        hence thesis by A29;

      end;

    end;

    theorem :: CARD_FIL:35

    

     Th35: for M holds for I be Ideal of M st I is_complete_with M & ( Frechet_Ideal M) c= I holds ex S be Subset-Family of M st ( card S) = M & (for X1 be set st X1 in S holds not X1 in I) & for X1,X2 be set st X1 in S & X2 in S & X1 <> X2 holds X1 misses X2

    proof

      let M;

      set N = ( predecessor M);

      let I be Ideal of M such that

       A1: I is_complete_with M and

       A2: ( Frechet_Ideal M) c= I;

      consider T such that

       A3: T is_Ulam_Matrix_of M by Th34;

      defpred P[ set, set] means not (T . ($2,$1)) in I;

      

       A4: M = ( nextcard N) by Def17;

      

       A5: for K1 holds ( union { (T . (N1,K1)) : N1 in N }) in ( dual I)

      proof

        deffunc F( Element of ( predecessor M), Element of M) = (T . ($1,$2));

        defpred R[ set, set] means $1 in N;

        let K1;

        defpred P[ set, set] means $2 = K1 & $1 in N;

        

         A6: { F(N1,K2) : K2 = K1 & R[N1, K2] } = { F(N2,K1) : R[N2, K1] } from FRAENKEL:sch 20;

        { F(N1,K2) : P[N1, K2] } is Subset-Family of M from DOMAIN_1:sch 9;

        then

        reconsider C = { (T . (N1,K1)) : N1 in N } as Subset-Family of M by A6;

        assume not ( union { (T . (N1,K1)) : N1 in N }) in ( dual I);

        then not (( union C) ` ) in ( Frechet_Ideal M) by A2, SETFAM_1:def 7;

        then not ( card (M \ ( union { (T . (N1,K1)) : N1 in N }))) in ( card M) by Th19;

        then

         A7: not ( card (M \ ( union { (T . (N1,K1)) : N1 in N }))) in ( nextcard N) by A4;

        ( card (M \ ( union { (T . (N1,K1)) : N1 in N }))) c= N by A3;

        hence contradiction by A7, CARD_3: 91;

      end;

      

       A8: for K1 holds ex N2 st P[K1, N2]

      proof

        deffunc F( set) = (T . $1);

        let K1;

        

         A9: { (T . (N1,K1)) : N1 in N } is non empty

        proof

          set N2 = the Element of ( predecessor M);

          (T . (N2,K1)) in { (T . (N1,K1)) : N1 in N };

          hence thesis;

        end;

        

         A10: ( card { F(X) where X be Element of [:N, M:] : X in [:N, {K1}:] }) c= ( card [:N, {K1}:]) from TREES_2:sch 2;

        { (T . (N1,K1)) : N1 in N } c= { (T . X) where X be Element of [:N, M:] : X in [:N, {K1}:] }

        proof

          let Y be object;

          assume Y in { (T . (N1,K1)) : N1 in N };

          then

          consider N1 such that

           A11: Y = (T . (N1,K1)) and N1 in N;

           [N1, K1] is Element of [:N, M:] & [N1, K1] in [:N, {K1}:] by ZFMISC_1: 87, ZFMISC_1: 106;

          hence thesis by A11;

        end;

        then

         A12: ( card { (T . (N1,K1)) : N1 in N }) c= ( card { (T . X) where X be Element of [:N, M:] : X in [:N, {K1}:] }) by CARD_1: 11;

        assume

         A13: for N2 holds (T . (N2,K1)) in I;

        

         A14: { (T . (N1,K1)) : N1 in N } c= I

        proof

          let X be object;

          assume X in { (T . (N1,K1)) : N1 in N };

          then ex N2 st X = (T . (N2,K1)) & N2 in N;

          hence thesis by A13;

        end;

        ( card [:N, {K1}:]) = ( card N) by CARD_1: 69;

        then

         A15: ( card [:N, {K1}:]) = N;

        N in M by A4, CARD_1: 18;

        then ( card { (T . (N1,K1)) : N1 in N }) in M by A10, A12, A15, ORDINAL1: 12, XBOOLE_1: 1;

        then ( union { (T . (N1,K1)) : N1 in N }) in I by A1, A14, A9;

        hence contradiction by A5, Th10;

      end;

      consider h be Function of M, N such that

       A16: for K1 holds P[K1, (h . K1)] from FUNCT_2:sch 3( A8);

      ex N2 st ( card (h " {N2})) = M

      proof

        deffunc F( set) = ( sup (h " {$1}));

        assume

         A17: for N2 holds ( card (h " {N2})) <> M;

        

         A18: { ( sup (h " {N2})) : N2 in N } c= M

        proof

          let x be object;

          assume x in { ( sup (h " {N2})) : N2 in N };

          then

          consider N2 such that

           A19: x = ( sup (h " {N2})) and N2 in N;

          ( card (h " {N2})) c= M & ( card (h " {N2})) <> M by A17, CARD_1: 7;

          then ( card (h " {N2})) in M by CARD_1: 3;

          then ( card (h " {N2})) in ( cf M) by CARD_5:def 3;

          hence thesis by A19, CARD_5: 26;

        end;

        ( card { F(N2) : N2 in N }) c= ( card N) from TREES_2:sch 2;

        then ( card { ( sup (h " {N2})) : N2 in N }) c= N;

        then ( card { ( sup (h " {N2})) : N2 in N }) in M by A4, CARD_3: 91;

        then ( card { ( sup (h " {N2})) : N2 in N }) in ( cf M) by CARD_5:def 3;

        then

        reconsider K1 = ( sup { ( sup (h " {N3})) : N3 in N }) as Element of M by A18, CARD_5: 26;

        for N2 holds ( sup (h " {N2})) in ( sup { ( sup (h " {N3})) : N3 in N })

        proof

          let N2;

          ( sup (h " {N2})) in { ( sup (h " {N3})) : N3 in N };

          hence thesis by ORDINAL2: 19;

        end;

        then ( sup (h " {(h . K1)})) in K1;

        hence contradiction by ORDINAL2: 19, SETWISEO: 7;

      end;

      then

      consider N2 such that

       A20: ( card (h " {N2})) = M;

      { (T . (N2,K2)) : (h . K2) = N2 } c= ( bool M)

      proof

        let X be object;

        assume X in { (T . (N2,K2)) : (h . K2) = N2 };

        then ex K2 st X = (T . (N2,K2)) & (h . K2) = N2;

        hence thesis;

      end;

      then

      reconsider S = { (T . (N2,K2)) : (h . K2) = N2 } as Subset-Family of M;

      ( dom T) = [:N, M:] by FUNCT_2:def 1;

      then

      consider G be Function such that (( curry T) . N2) = G and

       A21: ( dom G) = M and ( rng G) c= ( rng T) and

       A22: for y be object st y in M holds (G . y) = (T . (N2,y)) by FUNCT_5: 29;

      ((h " {N2}),M) are_equipotent by A20, CARD_1:def 2;

      then

      consider f be Function such that

       A23: f is one-to-one and

       A24: ( dom f) = M and

       A25: ( rng f) = (h " {N2}) by WELLORD2:def 4;

      

       A26: ( dom (G * f)) = ( dom f) by A25, A21, RELAT_1: 27;

      

       A27: S c= ( rng (G * f))

      proof

        let X be object;

        assume X in S;

        then

        consider K2 such that

         A28: X = (T . (N2,K2)) and

         A29: (h . K2) = N2;

        K2 in M;

        then

         A30: K2 in ( dom h) by FUNCT_2:def 1;

        (h . K2) in {N2} by A29, TARSKI:def 1;

        then K2 in (h " {N2}) by A30, FUNCT_1:def 7;

        then

        consider K3 be object such that

         A31: K3 in ( dom f) and

         A32: (f . K3) = K2 by A25, FUNCT_1:def 3;

        X = (G . (f . K3)) by A22, A28, A32;

        then X = ((G * f) . K3) by A26, A31, FUNCT_1: 12;

        hence thesis by A26, A31, FUNCT_1:def 3;

      end;

      

       A33: for X be set st X in ( dom f) holds (h . (f . X)) = N2

      proof

        let X be set;

        assume X in ( dom f);

        then (f . X) in (h " {N2}) by A25, FUNCT_1:def 3;

        then (h . (f . X)) in {N2} by FUNCT_1:def 7;

        hence thesis by TARSKI:def 1;

      end;

      ( rng (G * f)) c= S

      proof

        let X be object;

        assume X in ( rng (G * f));

        then

        consider K1 be object such that

         A34: K1 in ( dom (G * f)) and

         A35: X = ((G * f) . K1) by FUNCT_1:def 3;

        (f . K1) in ( rng f) by A26, A34, FUNCT_1:def 3;

        then

        reconsider K3 = (f . K1) as Element of M by A25;

        X = (G . (f . K1)) by A34, A35, FUNCT_1: 12;

        then

         A36: X = (T . (N2,K3)) by A22;

        (h . K3) = N2 by A33, A26, A34;

        hence thesis by A36;

      end;

      then

       A37: ( rng (G * f)) = S by A27;

      

       A38: for K1, K2 st (h . K1) = N2 & K1 <> K2 holds (T . (N2,K1)) <> (T . (N2,K2))

      proof

        let K1, K2 such that

         A39: (h . K1) = N2 and

         A40: K1 <> K2;

        assume (T . (N2,K1)) = (T . (N2,K2));

        then ((T . (N2,K1)) /\ (T . (N2,K2))) <> {} by A16, A39, Th11;

        hence contradiction by A3, A40;

      end;

      

       A41: (G * f) is one-to-one

      proof

        let K1,K2 be object such that

         A42: K1 in ( dom (G * f)) and

         A43: K2 in ( dom (G * f)) and

         A44: ((G * f) . K1) = ((G * f) . K2);

        assume K1 <> K2;

        then

         A45: (f . K1) <> (f . K2) by A23, A26, A42, A43;

        

         A46: (f . K2) in ( rng f) by A26, A43, FUNCT_1:def 3;

        then

        reconsider K4 = (f . K2) as Element of M by A25;

        

         A47: ((G * f) . K2) = (G . (f . K2)) by A43, FUNCT_1: 12

        .= (T . (N2,(f . K2))) by A25, A22, A46;

        

         A48: (f . K1) in ( rng f) by A26, A42, FUNCT_1:def 3;

        then

        reconsider K3 = (f . K1) as Element of M by A25;

        (h . K3) = N2 by A33, A26, A42;

        then

         A49: (T . (N2,K3)) <> (T . (N2,K4)) by A38, A45;

        ((G * f) . K1) = (G . (f . K1)) by A42, FUNCT_1: 12

        .= (T . (N2,(f . K1))) by A25, A22, A48;

        hence contradiction by A44, A49, A47;

      end;

      take S;

      ( dom (G * f)) = M by A24, A25, A21, RELAT_1: 27;

      then (S,M) are_equipotent by A37, A41, WELLORD2:def 4;

      hence ( card S) = M by CARD_1:def 2;

      thus for X1 be set st X1 in S holds not X1 in I

      proof

        let X1 be set;

        assume X1 in S;

        then ex K1 st (T . (N2,K1)) = X1 & (h . K1) = N2;

        hence thesis by A16;

      end;

      thus for X1,X2 be set st X1 in S & X2 in S & X1 <> X2 holds X1 misses X2

      proof

        let X1,X2 be set such that

         A50: X1 in S and

         A51: X2 in S and

         A52: X1 <> X2;

        consider K2 such that

         A53: (T . (N2,K2)) = X2 and (h . K2) = N2 by A51;

        consider K1 such that

         A54: (T . (N2,K1)) = X1 and (h . K1) = N2 by A50;

        ((T . (N2,K1)) /\ (T . (N2,K2))) = {} by A3, A52, A54, A53;

        hence thesis by A54, A53;

      end;

    end;

    theorem :: CARD_FIL:36

    

     Th36: for X holds for N be Cardinal st N c= ( card X) holds ex Y be set st Y c= X & ( card Y) = N

    proof

      let X;

      (X,( card X)) are_equipotent by CARD_1:def 2;

      then

      consider f be Function such that

       A1: f is one-to-one and

       A2: ( dom f) = ( card X) and

       A3: ( rng f) = X by WELLORD2:def 4;

      let N be Cardinal;

      assume N c= ( card X);

      then

       A4: ( dom (f | N)) = N by A2, RELAT_1: 62;

      take (f .: N);

      thus (f .: N) c= X by A3, RELAT_1: 111;

      

       A5: ( rng (f | N)) = (f .: N) by RELAT_1: 115;

      (f | N) is one-to-one by A1, FUNCT_1: 52;

      then (N,(f .: N)) are_equipotent by A4, A5, WELLORD2:def 4;

      hence thesis by CARD_1:def 2;

    end;

    theorem :: CARD_FIL:37

    

     Th37: for M holds not ex F st F is uniform being_ultrafilter & F is_complete_with M

    proof

      let M;

      given F such that

       A1: F is uniform being_ultrafilter and

       A2: F is_complete_with M;

      ( Frechet_Ideal M) c= ( dual F)

      proof

        let X be object such that

         A3: X in ( Frechet_Ideal M);

        reconsider X1 = X as Subset of M by A3;

        assume not X in ( dual F);

        then X1 in F by A1, Th22;

        then

         A4: ( card X1) = ( card M) by A1;

        ( card X1) in ( card M) by A3, Th19;

        hence contradiction by A4;

      end;

      then

      consider S be Subset-Family of M such that

       A5: ( card S) = M and

       A6: for X1 be set st X1 in S holds not X1 in ( dual F) and

       A7: for X1,X2 be set st X1 in S & X2 in S & X1 <> X2 holds X1 misses X2 by A2, Th12, Th35;

      S is infinite by A5;

      then

      consider X1 be object such that

       A8: X1 in S by XBOOLE_0:def 1;

      (S \ {X1}) <> {}

      proof

        assume (S \ {X1}) = {} ;

        then S c= {X1} by XBOOLE_1: 37;

        hence contradiction by A5;

      end;

      then

      consider X2 be object such that

       A9: X2 in (S \ {X1}) by XBOOLE_0:def 1;

      

       A10: (S qua set \ {X1}) is Subset of S;

      reconsider X1, X2 as set by TARSKI: 1;

       not X2 in {X1} by A9, XBOOLE_0:def 5;

      then X2 <> X1 by TARSKI:def 1;

      then X1 misses X2 by A7, A8, A9, A10;

      then

       A11: (X1 /\ X2) = {} ;

      reconsider X1, X2 as Subset of M by A8, A9;

      

       A12: for X1 be set st X1 in S holds X1 in F by A1, A6, Th22;

      then

       A13: X1 in F by A8;

      X2 in F by A12, A9, A10;

      then {} in F by A11, A13, Def1;

      hence contradiction by Def1;

    end;

    reserve M for Aleph;

    theorem :: CARD_FIL:38

    

     Th38: M is measurable implies M is limit_cardinal

    proof

      assume M is measurable;

      then

      consider F be Filter of M such that

       A1: F is_complete_with M and

       A2: F is non principal being_ultrafilter;

      assume

       A3: not M is limit_cardinal;

      F is_complete_with ( card M) by A1;

      hence contradiction by A2, A3, Th23, Th37;

    end;

    theorem :: CARD_FIL:39

    M is measurable implies M is inaccessible by Th33, Th38;

    theorem :: CARD_FIL:40

    

     Th40: M is measurable implies M is strong_limit

    proof

      assume M is measurable;

      then

      consider F be Filter of M such that

       A1: F is_complete_with M and

       A2: F is non principal being_ultrafilter;

      assume not M is strong_limit;

      then

      consider N be Cardinal such that

       A3: N in M and

       A4: not ( exp (2,N)) in M;

      

       A5: M c= ( exp (2,N)) by A4, CARD_1: 4;

      then M c= ( card ( Funcs (N,2))) by CARD_2:def 3;

      then

      consider Y be set such that

       A6: Y c= ( Funcs (N,2)) and

       A7: ( card Y) = M by Th36;

      N is infinite

      proof

        M c= ( exp (2,( card N))) by A5;

        then

         A8: M c= ( card ( bool N)) by CARD_2: 31;

        assume N is finite;

        hence contradiction by A8;

      end;

      then

      reconsider N1 = N as Aleph;

      (Y,M) are_equipotent by A7, CARD_1:def 2;

      then

      consider f be Function such that

       A9: f is one-to-one and

       A10: ( dom f) = M and

       A11: ( rng f) = Y by WELLORD2:def 4;

      defpred P[ set, set] means (f " { h where h be Function of N1, { {} , 1} : h in Y & (h . $1) = $2 }) in F;

      

       A12: for A be Element of N1 holds ex i be Element of { {} , 1} st P[A, i]

      proof

        let A be Element of N1;

        set Y1 = { h where h be Function of N1, { {} , 1} : h in Y & (h . A) = 1 };

        reconsider Inv1 = (f " Y1) as Subset of M by A10, RELAT_1: 132;

        set Y0 = { h where h be Function of N1, { {} , 1} : h in Y & (h . A) = {} };

        reconsider Inv0 = (f " Y0) as Subset of M by A10, RELAT_1: 132;

        

         A13: for g1 be Function of N1, { {} , 1} st g1 in Y holds g1 in Y1 or g1 in Y0

        proof

          let g1 be Function of N1, { {} , 1} such that

           A14: g1 in Y;

          per cases ;

            suppose g1 in Y0;

            hence thesis;

          end;

            suppose not g1 in Y0;

            then not (g1 . A) = {} by A14;

            then (g1 . A) = 1 by TARSKI:def 2;

            hence thesis by A14;

          end;

        end;

        (Y \ Y0) = Y1

        proof

          thus (Y \ Y0) c= Y1

          proof

            let X be object such that

             A15: X in (Y \ Y0);

            X in Y by A15;

            then

            consider g1 be Function such that

             A16: g1 = X and

             A17: ( dom g1) = N1 & ( rng g1) c= { {} , 1} by A6, CARD_1: 50, FUNCT_2:def 2;

            reconsider g2 = g1 as Function of N1, { {} , 1} by A17, FUNCT_2:def 1, RELSET_1: 4;

             not X in Y0 by A15, XBOOLE_0:def 5;

            then g2 in Y1 by A13, A15, A16;

            hence thesis by A16;

          end;

          let X be object;

          assume X in Y1;

          then

          consider h be Function of N1, { {} , 1} such that

           A18: X = h & h in Y and

           A19: (h . A) = 1;

           not h in Y0

          proof

            assume h in Y0;

            then ex h1 be Function of N1, { {} , 1} st h1 = h & h1 in Y & (h1 . A) = {} ;

            hence contradiction by A19;

          end;

          hence thesis by A18, XBOOLE_0:def 5;

        end;

        

        then

         A20: Inv1 = ((f " ( rng f)) \ Inv0) by A11, FUNCT_1: 69

        .= (M \ Inv0) by A10, RELAT_1: 134;

        per cases by A2;

          suppose

           A21: Inv0 in F;

          reconsider Z = {} as Element of { {} , 1} by TARSKI:def 2;

          take Z;

          thus thesis by A21;

        end;

          suppose

           A22: (M \ Inv0) in F;

          reconsider O = 1 as Element of { {} , 1} by TARSKI:def 2;

          take O;

          thus thesis by A20, A22;

        end;

      end;

      consider g be Function of N1, { {} , 1} such that

       A23: for A be Element of N1 holds P[A, (g . A)] from FUNCT_2:sch 3( A12);

      deffunc T( Element of N1) = (f " { h where h be Function of N1, { {} , 1} : h in Y & (h . $1) = (g . $1) });

      reconsider f1 = f as Function of M, Y by A10, A11, FUNCT_2: 1;

      set MEET = ( meet { T(A) where A be Element of N1 : A in N1 });

      

       A24: ( rng (f | MEET)) = (f .: MEET) & (f | MEET) is one-to-one by A9, FUNCT_1: 52, RELAT_1: 115;

      ( card { T(A) where A be Element of N1 : A in N1 }) c= ( card N1) from TREES_2:sch 2;

      then ( card { T(A) where A be Element of N1 : A in N1 }) c= N1;

      then

       A25: ( card { T(A) where A be Element of N1 : A in N1 }) in M by A3, ORDINAL1: 12;

      set B = the Element of N1;

      

       A26: { T(A) where A be Element of N1 : A in N1 } c= F

      proof

        let X be object;

        assume X in { T(A) where A be Element of N1 : A in N1 };

        then ex A be Element of N1 st X = T(A) & A in N1;

        hence thesis by A23;

      end;

       T(B) in { T(A) where A be Element of N1 : A in N1 };

      then

       A27: ( meet { T(A) where A be Element of N1 : A in N1 }) in F by A1, A25, A26;

      

       A28: Y is infinite by A7;

      

       A29: for X be set holds X in ( meet { T(A) where A be Element of N1 : A in N1 }) implies (f . X) = g

      proof

        let X be set;

        assume

         A30: X in ( meet { T(A) where A be Element of N1 : A in N1 });

        then

        reconsider X1 = X as Element of M by A27;

        (f1 . X1) in Y by A28, FUNCT_2: 5;

        then

        consider h1 be Function such that

         A31: (f1 . X1) = h1 and

         A32: ( dom h1) = N and ( rng h1) c= 2 by A6, FUNCT_2:def 2;

        

         A33: for Z be object st Z in N1 holds (h1 . Z) = (g . Z)

        proof

          let Z be object;

          assume Z in N1;

          then

          reconsider Z1 = Z as Element of N1;

           T(Z1) in { T(A) where A be Element of N1 : A in N1 };

          then X1 in T(Z1) by A30, SETFAM_1:def 1;

          then (f1 . X1) in { h where h be Function of N1, { {} , 1} : h in Y & (h . Z1) = (g . Z1) } by FUNCT_1:def 7;

          then ex h be Function of N1, { {} , 1} st (f . X1) = h & h in Y & (h . Z1) = (g . Z1);

          hence thesis by A31;

        end;

        ( dom g) = N1 by FUNCT_2:def 1;

        hence thesis by A31, A32, A33, FUNCT_1: 2;

      end;

      

       A34: (f .: MEET) c= {g}

      proof

        let X be object;

        assume X in (f .: MEET);

        then ex x be object st x in ( dom f) & x in MEET & X = (f . x) by FUNCT_1:def 6;

        then X = g by A29;

        hence thesis by TARSKI:def 1;

      end;

      MEET = (( dom f) /\ MEET) by A10, A27, XBOOLE_1: 28;

      then ( dom (f | MEET)) = MEET by RELAT_1: 61;

      then

       A35: ( card MEET) c= ( card {g}) by A34, A24, CARD_1: 10;

      reconsider MEET as Subset of M by A27;

      F is_complete_with ( card M) by A1;

      then F is uniform by A2, Th23;

      then ( card MEET) = ( card M) by A27;

      hence contradiction by A35;

    end;

    theorem :: CARD_FIL:41

    M is measurable implies M is strongly_inaccessible by Th33, Th40;