fraenkel.miz



    begin

    reserve B for non empty set,

A,X,x for set;

    scheme :: FRAENKEL:sch1

    Fraenkel59 { A() -> set , F( object) -> object , P,Q[ object] } :

{ F(v) where v be Element of A() : P[v] } c= { F(u) where u be Element of A() : Q[u] }

      provided

       A1: for v be Element of A() holds P[v] implies Q[v];

      let x be object;

      assume x in { F(v9) where v9 be Element of A() : P[v9] };

      then

      consider v be Element of A() such that

       A2: x = F(v) and

       A3: P[v];

      Q[v] by A1, A3;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch2

    Fraenkel599 { A,B() -> set , F( object, object) -> object , P,Q[ object, object] } :

{ F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } c= { F(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] }

      provided

       A1: for u be Element of A(), v be Element of B() holds P[u, v] implies Q[u, v];

      let x be object;

      assume x in { F(u9,v9) where u9 be Element of A(), v9 be Element of B() : P[u9, v9] };

      then

      consider u be Element of A(), v be Element of B() such that

       A2: x = F(u,v) and

       A3: P[u, v];

      Q[u, v] by A1, A3;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch3

    Fraenkel69 { B() -> set , F( object) -> object , P,Q[ object] } :

{ F(v1) where v1 be Element of B() : P[v1] } = { F(v2) where v2 be Element of B() : Q[v2] }

      provided

       A1: for v be Element of B() holds P[v] iff Q[v];

      set A = { F(v1) where v1 be Element of B() : P[v1] }, B = { F(v2) where v2 be Element of B() : Q[v2] };

      

       A2: for v be Element of B() holds P[v] implies Q[v] by A1;

      thus A c= B from Fraenkel59( A2);

      

       A3: for v be Element of B() holds Q[v] implies P[v] by A1;

      thus B c= A from Fraenkel59( A3);

    end;

    scheme :: FRAENKEL:sch4

    Fraenkel699 { A,B() -> set , F( object, object) -> object , P,Q[ object, object] } :

{ F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } = { F(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] }

      provided

       A1: for u be Element of A(), v be Element of B() holds P[u, v] iff Q[u, v];

      set B = { F(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] };

      set A = { F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] };

      

       A2: for u be Element of A(), v be Element of B() holds P[u, v] implies Q[u, v] by A1;

      thus A c= B from Fraenkel599( A2);

      

       A3: for u be Element of A(), v be Element of B() holds Q[u, v] implies P[u, v] by A1;

      thus B c= A from Fraenkel599( A3);

    end;

    scheme :: FRAENKEL:sch5

    FraenkelF9 { B() -> set , F,G( object) -> object , P[ object] } :

{ F(v1) where v1 be Element of B() : P[v1] } = { G(v2) where v2 be Element of B() : P[v2] }

      provided

       A1: for v be Element of B() holds F(v) = G(v);

      set X = { F(v1) where v1 be Element of B() : P[v1] }, Y = { G(v2) where v2 be Element of B() : P[v2] };

      

       A2: Y c= X

      proof

        let x be object;

        assume x in Y;

        then

        consider v1 be Element of B() such that

         A3: x = G(v1) and

         A4: P[v1];

        x = F(v1) by A1, A3;

        hence thesis by A4;

      end;

      X c= Y

      proof

        let x be object;

        assume x in X;

        then

        consider v1 be Element of B() such that

         A5: x = F(v1) and

         A6: P[v1];

        x = G(v1) by A1, A5;

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch6

    FraenkelF9R { B() -> set , F,G( object) -> object , P[ object] } :

{ F(v1) where v1 be Element of B() : P[v1] } = { G(v2) where v2 be Element of B() : P[v2] }

      provided

       A1: for v be Element of B() st P[v] holds F(v) = G(v);

      set X = { F(v1) where v1 be Element of B() : P[v1] }, Y = { G(v2) where v2 be Element of B() : P[v2] };

      

       A2: Y c= X

      proof

        let x be object;

        assume x in Y;

        then

        consider v1 be Element of B() such that

         A3: x = G(v1) and

         A4: P[v1];

        x = F(v1) by A1, A3, A4;

        hence thesis by A4;

      end;

      X c= Y

      proof

        let x be object;

        assume x in X;

        then

        consider v1 be Element of B() such that

         A5: x = F(v1) and

         A6: P[v1];

        x = G(v1) by A1, A5, A6;

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch7

    FraenkelF99 { A,B() -> set , F,G( object, object) -> object , P[ object, object] } :

{ F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } = { G(u2,v2) where u2 be Element of A(), v2 be Element of B() : P[u2, v2] }

      provided

       A1: for u be Element of A(), v be Element of B() holds F(u,v) = G(u,v);

      set Y = { G(u2,v2) where u2 be Element of A(), v2 be Element of B() : P[u2, v2] };

      set X = { F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] };

      

       A2: Y c= X

      proof

        let x be object;

        assume x in Y;

        then

        consider u1 be Element of A(), v1 be Element of B() such that

         A3: x = G(u1,v1) and

         A4: P[u1, v1];

        x = F(u1,v1) by A1, A3;

        hence thesis by A4;

      end;

      X c= Y

      proof

        let x be object;

        assume x in X;

        then

        consider u1 be Element of A(), v1 be Element of B() such that

         A5: x = F(u1,v1) and

         A6: P[u1, v1];

        x = G(u1,v1) by A1, A5;

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch8

    FraenkelF699 { A,B() -> set , F( object, object) -> object , P,Q[ object, object] } :

{ F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } = { F(v2,u2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] }

      provided

       A1: for u be Element of A(), v be Element of B() holds P[u, v] iff Q[u, v]

       and

       A2: for u be Element of A(), v be Element of B() holds F(u,v) = F(v,u);

      

       A3: for u be Element of A(), v be Element of B() holds Q[u, v] implies P[u, v] by A1;

      

       A4: { F(u1,v1) where u1 be Element of A(), v1 be Element of B() : Q[u1, v1] } c= { F(u2,v2) where u2 be Element of A(), v2 be Element of B() : P[u2, v2] } from Fraenkel599( A3);

      deffunc H( set, set) = F($2,$1);

      

       A5: for u be Element of A(), v be Element of B() holds P[u, v] implies Q[u, v] by A1;

      

       A6: { F(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } c= { F(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] } from Fraenkel599( A5);

      

       A7: for u be Element of A(), v be Element of B() holds F(u,v) = H(u,v) by A2;

      { F(u1,v1) where u1 be Element of A(), v1 be Element of B() : Q[u1, v1] } = { H(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] } from FraenkelF99( A7);

      hence thesis by A6, A4;

    end;

    theorem :: FRAENKEL:1

    

     Th1: for A,B be set, F,G be Function of A, B holds for X be set st (F | X) = (G | X) holds for x be Element of A st x in X holds (F . x) = (G . x)

    proof

      let A,B be set, F,G be Function of A, B;

      let X be set such that

       A1: (F | X) = (G | X);

      let x be Element of A;

      assume

       A2: x in X;

      

      hence (F . x) = ((G | X) . x) by A1, FUNCT_1: 49

      .= (G . x) by A2, FUNCT_1: 49;

    end;

    theorem :: FRAENKEL:2

    

     Th2: for A,B be set holds ( Funcs (A,B)) c= ( bool [:A, B:])

    proof

      let A,B be set, x be object;

      assume x in ( Funcs (A,B));

      then

      consider f be Function such that

       A1: x = f and

       A2: ( dom f) = A and

       A3: ( rng f) c= B by FUNCT_2:def 2;

      

       A4: f c= [:( dom f), ( rng f):] by RELAT_1: 7;

       [:( dom f), ( rng f):] c= [:A, B:] by A2, A3, ZFMISC_1: 95;

      then f c= [:A, B:] by A4;

      hence thesis by A1;

    end;

    theorem :: FRAENKEL:3

    

     Th3: for X,Y be set st ( Funcs (X,Y)) <> {} & X c= A & Y c= B holds for f be Element of ( Funcs (X,Y)) holds f is PartFunc of A, B

    proof

      let X,Y be set such that

       A1: ( Funcs (X,Y)) <> {} and

       A2: X c= A and

       A3: Y c= B;

      let f be Element of ( Funcs (X,Y));

      consider g be Function such that

       A4: f = g and

       A5: ( dom g) = X and

       A6: ( rng g) c= Y by A1, FUNCT_2:def 2;

      ( rng g) c= B by A3, A6;

      hence thesis by A2, A4, A5, RELSET_1: 4;

    end;

    scheme :: FRAENKEL:sch9

    RelevantArgs { A,B,X() -> set , f,g() -> Function of A(), B() , P,Q[ object] } :

{ (f() . u9) where u9 be Element of A() : P[u9] & u9 in X() } = { (g() . v9) where v9 be Element of A() : Q[v9] & v9 in X() }

      provided

       A1: (f() | X()) = (g() | X())

       and

       A2: for u be Element of A() st u in X() holds P[u] iff Q[u];

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

      deffunc G( set) = (g() . $1);

      defpred PP[ set] means P[$1] & $1 in X();

      defpred QQ[ set] means Q[$1] & $1 in X();

      set C = { G(v9) where v9 be Element of A() : PP[v9] };

      

       A3: for v be Element of A() holds PP[v] iff QQ[v] by A2;

      

       A4: C = { G(v9) where v9 be Element of A() : QQ[v9] } from Fraenkel69( A3);

      

       A5: for v be Element of A() st PP[v] holds F(v) = G(v) by A1, Th1;

      { F(u9) where u9 be Element of A() : PP[u9] } = C from FraenkelF9R( A5);

      hence thesis by A4;

    end;

    scheme :: FRAENKEL:sch10

    FrSet0 { A() -> non empty set , P[ object] } :

{ x where x be Element of A() : P[x] } c= A();

      { x where x be Element of A() : P[x] } is Subset of A() from DOMAIN_1:sch 7;

      hence thesis;

    end;

    scheme :: FRAENKEL:sch11

    Gen199 { A,B() -> set , F( object, object) -> object , P[ object, object], Q[ object] } :

for s be Element of A(), t be Element of B() st P[s, t] holds Q[F(s,t)]

      provided

       A1: for st1 be set st st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } holds Q[st1];

      let s be Element of A(), t be Element of B();

      assume P[s, t];

      then F(s,t) in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] };

      hence thesis by A1;

    end;

    scheme :: FRAENKEL:sch12

    Gen199A { A,B() -> set , F( object, object) -> object , P[ object, object], Q[ object] } :

for st1 be set st st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } holds Q[st1]

      provided

       A1: for s be Element of A(), t be Element of B() st P[s, t] holds Q[F(s,t)];

      let st1 be set;

      assume st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] };

      then ex s1 be Element of A(), t1 be Element of B() st st1 = F(s1,t1) & P[s1, t1];

      hence thesis by A1;

    end;

    scheme :: FRAENKEL:sch13

    Gen299 { A,B,C() -> set , F( object, object) -> Element of C() , P[ object, object], Q[ object] } :

{ st1 where st1 be Element of C() : st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } & Q[st1] } = { F(s2,t2) where s2 be Element of A(), t2 be Element of B() : P[s2, t2] & Q[F(s2,t2)] };

      thus { st1 where st1 be Element of C() : st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } & Q[st1] } c= { F(s2,t2) where s2 be Element of A(), t2 be Element of B() : P[s2, t2] & Q[F(s2,t2)] }

      proof

        let x be object;

        assume x in { st1 where st1 be Element of C() : st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } & Q[st1] };

        then

        consider st1 be Element of C() such that

         A1: x = st1 and

         A2: st1 in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } and

         A3: Q[st1];

        ex s1 be Element of A(), t1 be Element of B() st st1 = F(s1,t1) & P[s1, t1] by A2;

        hence thesis by A1, A3;

      end;

      let x be object;

      assume x in { F(s2,t2) where s2 be Element of A(), t2 be Element of B() : P[s2, t2] & Q[F(s2,t2)] };

      then

      consider s2 be Element of A(), t2 be Element of B() such that

       A4: x = F(s2,t2) and

       A5: P[s2, t2] and

       A6: Q[F(s2,t2)];

      F(s2,t2) in { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : P[s1, t1] } by A5;

      hence thesis by A4, A6;

    end;

    scheme :: FRAENKEL:sch14

    Gen39 { A() -> set , F( object) -> object , P,Q[ object] } :

{ F(s) where s be Element of A() : s in { s1 where s1 be Element of A() : Q[s1] } & P[s] } = { F(s2) where s2 be Element of A() : Q[s2] & P[s2] };

      defpred QQ[ set] means Q[$1] & P[$1];

      defpred PP[ set] means $1 in { s1 where s1 be Element of A() : Q[s1] } & P[$1];

      

       A1: for s be Element of A() holds PP[s] iff QQ[s]

      proof

        let s be Element of A();

        now

          assume s in { s1 where s1 be Element of A() : Q[s1] };

          then ex s1 be Element of A() st s = s1 & Q[s1];

          hence Q[s];

        end;

        hence thesis;

      end;

      thus { F(s) where s be Element of A() : PP[s] } = { F(s2) where s2 be Element of A() : QQ[s2] } from Fraenkel69( A1);

    end;

    scheme :: FRAENKEL:sch15

    Gen399 { A,B() -> set , F( object, object) -> object , P[ object, object], Q[ object] } :

{ F(s,t) where s be Element of A(), t be Element of B() : s in { s1 where s1 be Element of A() : Q[s1] } & P[s, t] } = { F(s2,t2) where s2 be Element of A(), t2 be Element of B() : Q[s2] & P[s2, t2] };

      defpred QQ[ set, set] means Q[$1] & P[$1, $2];

      defpred PP[ set, set] means $1 in { s1 where s1 be Element of A() : Q[s1] } & P[$1, $2];

      

       A1: for s be Element of A(), t be Element of B() holds PP[s, t] iff QQ[s, t]

      proof

        let s be Element of A(), t be Element of B();

        now

          assume s in { s1 where s1 be Element of A() : Q[s1] };

          then ex s1 be Element of A() st s = s1 & Q[s1];

          hence Q[s];

        end;

        hence thesis;

      end;

      thus { F(s,t) where s be Element of A(), t be Element of B() : PP[s, t] } = { F(s2,t2) where s2 be Element of A(), t2 be Element of B() : QQ[s2, t2] } from Fraenkel699( A1);

    end;

    scheme :: FRAENKEL:sch16

    Gen499 { A,B() -> set , F( object, object) -> object , P,Q[ object, object] } :

{ F(s,t) where s be Element of A(), t be Element of B() : P[s, t] } c= { F(s1,t1) where s1 be Element of A(), t1 be Element of B() : Q[s1, t1] }

      provided

       A1: for s be Element of A(), t be Element of B() st P[s, t] holds ex s9 be Element of A() st Q[s9, t] & F(s,t) = F(s9,t);

      let x be object;

      assume x in { F(s,t) where s be Element of A(), t be Element of B() : P[s, t] };

      then

      consider s be Element of A(), t be Element of B() such that

       A2: x = F(s,t) and

       A3: P[s, t];

      ex s9 be Element of A() st Q[s9, t] & F(s,t) = F(s9,t) by A1, A3;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch17

    FrSet1 { D,A() -> set , P[ object], F( object) -> object } :

{ F(y) where y be Element of D() : F(y) in A() & P[y] } c= A();

      let x be object;

      assume x in { F(y) where y be Element of D() : F(y) in A() & P[y] };

      then ex y be Element of D() st x = F(y) & F(y) in A() & P[y];

      hence thesis;

    end;

    scheme :: FRAENKEL:sch18

    FrSet2 { D,A() -> set , Q[ object], F( object) -> object } :

{ F(y) where y be Element of D() : Q[y] & not F(y) in A() } misses A();

      assume { F(y) where y be Element of D() : Q[y] & not F(y) in A() } meets A();

      then

      consider x be object such that

       A1: x in { F(y) where y be Element of D() : Q[y] & not F(y) in A() } and

       A2: x in A() by XBOOLE_0: 3;

      ex y be Element of D() st x = F(y) & Q[y] & not F(y) in A() by A1;

      hence thesis by A2;

    end;

    scheme :: FRAENKEL:sch19

    FrEqua1 { A,B() -> set , F( object, object) -> object , x() -> Element of B() , P,Q[ object, object] } :

{ F(s,t) where s be Element of A(), t be Element of B() : Q[s, t] } = { F(s9,x) where s9 be Element of A() : P[s9, x()] }

      provided

       A1: for s be Element of A() holds for t be Element of B() holds Q[s, t] iff t = x() & P[s, t];

      thus { F(s,t) where s be Element of A(), t be Element of B() : Q[s, t] } c= { F(s9,x) where s9 be Element of A() : P[s9, x()] }

      proof

        let x be object;

        assume x in { F(s,t) where s be Element of A(), t be Element of B() : Q[s, t] };

        then

        consider s be Element of A(), t be Element of B() such that

         A2: x = F(s,t) and

         A3: Q[s, t];

        

         A4: P[s, t] by A1, A3;

        t = x() by A1, A3;

        hence thesis by A2, A4;

      end;

      let x be object;

      assume x in { F(s9,x) where s9 be Element of A() : P[s9, x()] };

      then

      consider s9 be Element of A() such that

       A5: x = F(s9,x) and

       A6: P[s9, x()];

      Q[s9, x()] by A1, A6;

      hence thesis by A5;

    end;

    scheme :: FRAENKEL:sch20

    FrEqua2 { A,B() -> set , F( object, object) -> object , x() -> Element of B() , P[ object, object] } :

{ F(s,t) where s be Element of A(), t be Element of B() : t = x() & P[s, t] } = { F(s9,x) where s9 be Element of A() : P[s9, x()] };

      defpred Q[ set, set] means $2 = x() & P[$1, $2];

      

       A1: for s be Element of A() holds for t be Element of B() holds Q[s, t] iff t = x() & P[s, t];

      thus { F(s,t) where s be Element of A(), t be Element of B() : Q[s, t] } = { F(s9,x) where s9 be Element of A() : P[s9, x()] } from FrEqua1( A1);

    end;

    reserve phi for Element of ( Funcs (A,B));

    theorem :: FRAENKEL:4

    

     Th4: for X,Y be set st ( Funcs (X,Y)) <> {} & X c= A & Y c= B holds for f be Element of ( Funcs (X,Y)) holds ex phi be Element of ( Funcs (A,B)) st (phi | X) = f

    proof

      let X,Y be set such that

       A1: ( Funcs (X,Y)) <> {} and

       A2: X c= A and

       A3: Y c= B;

      let f be Element of ( Funcs (X,Y));

      reconsider f9 = f as PartFunc of A, B by A1, A2, A3, Th3;

      consider phi be Function of A, B such that

       A4: for x be object st x in ( dom f9) holds (phi . x) = (f9 . x) by FUNCT_2: 71;

      reconsider phi as Element of ( Funcs (A,B)) by FUNCT_2: 8;

      take phi;

      ex g be Function st f = g & ( dom g) = X & ( rng g) c= Y by A1, FUNCT_2:def 2;

      

      then ( dom f9) = (A /\ X) by XBOOLE_1: 28

      .= (( dom phi) /\ X) by FUNCT_2:def 1;

      hence thesis by A4, FUNCT_1: 46;

    end;

    theorem :: FRAENKEL:5

    

     Th5: (phi | X) = (phi | (A /\ X))

    proof

      ( dom phi) = A by FUNCT_2:def 1;

      

      then

       A1: ( dom (phi | X)) = ((( dom phi) /\ A) /\ X) by RELAT_1: 61

      .= (( dom phi) /\ (A /\ X)) by XBOOLE_1: 16;

      for x be object st x in ( dom (phi | X)) holds ((phi | X) . x) = (phi . x) by FUNCT_1: 47;

      hence thesis by A1, FUNCT_1: 46;

    end;

    scheme :: FRAENKEL:sch21

    FraenkelFin { A,X() -> set , F( object) -> object } :

{ F(w) where w be Element of A() : w in X() } is finite

      provided

       A1: X() is finite;

      set M = { F(w) where w be Element of A() : w in X() };

      per cases ;

        suppose

         A2: A() is empty;

        M c= {F({})}

        proof

          let x be object;

          assume x in M;

          then

          consider w be Element of A() such that

           A3: x = F(w) & w in X();

          w = {} by A2, SUBSET_1:def 1;

          hence thesis by A3, TARSKI:def 1;

        end;

        hence thesis;

      end;

        suppose

         A4: A() is non empty;

        consider f be Function such that

         A5: ( dom f) = (X() /\ A()) and

         A6: for y be object st y in (X() /\ A()) holds (f . y) = F(y) from FUNCT_1:sch 3;

        M = (f .: X())

        proof

          thus M c= (f .: X())

          proof

            let x be object;

            assume x in M;

            then

            consider u be Element of A() such that

             A7: x = F(u) and

             A8: u in X();

            

             A9: u in ( dom f) by A4, A5, A8, XBOOLE_0:def 4;

            then (f . u) = F(u) by A5, A6;

            hence thesis by A7, A8, A9, FUNCT_1:def 6;

          end;

          let x be object;

          assume x in (f .: X());

          then

          consider y be object such that

           A10: y in ( dom f) and

           A11: y in X() and

           A12: x = (f . y) by FUNCT_1:def 6;

          reconsider y as Element of A() by A5, A10, XBOOLE_0:def 4;

          x = F(y) by A5, A6, A10, A12;

          hence thesis by A11;

        end;

        hence thesis by A1;

      end;

    end;

    scheme :: FRAENKEL:sch22

    CartFin { A,B() -> non empty set , X,Y() -> set , F( object, object) -> object } :

{ F(u,v) where u be Element of A(), v be Element of B() : u in X() & v in Y() } is finite

      provided

       A1: X() is finite

       and

       A2: Y() is finite;

      deffunc G( object) = F(`1,`2);

      set M = { F(u9,v9) where u9 be Element of A(), v9 be Element of B() : u9 in X() & v9 in Y() };

      consider f be Function such that

       A3: ( dom f) = [:(X() /\ A()), (Y() /\ B()):] and

       A4: for y be object st y in [:(X() /\ A()), (Y() /\ B()):] holds (f . y) = G(y) from FUNCT_1:sch 3;

      

       A5: ( dom f) = ( [:X(), Y():] /\ [:A(), B():]) by A3, ZFMISC_1: 100;

      M = (f .: [:X(), Y():])

      proof

        thus M c= (f .: [:X(), Y():])

        proof

          let x be object;

          assume x in M;

          then

          consider u be Element of A(), v be Element of B() such that

           A6: x = F(u,v) and

           A7: u in X() and

           A8: v in Y();

          

           A9: [u, v] in [:X(), Y():] by A7, A8, ZFMISC_1: 87;

          then

           A10: [u, v] in ( dom f) by A5, XBOOLE_0:def 4;

          

           A11: ( [u, v] `2 ) = v;

          ( [u, v] `1 ) = u;

          then (f . (u,v)) = F(u,v) by A3, A4, A10, A11;

          hence thesis by A6, A9, A10, FUNCT_1:def 6;

        end;

        let x be object;

        assume x in (f .: [:X(), Y():]);

        then

        consider y be object such that

         A12: y in ( dom f) and

         A13: y in [:X(), Y():] and

         A14: x = (f . y) by FUNCT_1:def 6;

        reconsider y as Element of [:A(), B():] by A5, A12, XBOOLE_0:def 4;

        

         A15: y = [(y `1 ), (y `2 )] by MCART_1: 21;

        then

         A16: (y `1 ) in X() by A13, ZFMISC_1: 87;

        

         A17: (y `2 ) in Y() by A13, A15, ZFMISC_1: 87;

        x = F(`1,`2) by A3, A4, A12, A14;

        hence thesis by A16, A17;

      end;

      hence thesis by A1, A2;

    end;

    scheme :: FRAENKEL:sch23

    Finiteness { A() -> non empty set , B() -> Element of ( Fin A()) , P[ Element of A(), Element of A()] } :

for x be Element of A() st x in B() holds ex y be Element of A() st y in B() & P[y, x] & for z be Element of A() st z in B() & P[z, y] holds P[y, z]

      provided

       A1: for x be Element of A() holds P[x, x]

       and

       A2: for x,y,z be Element of A() st P[x, y] & P[y, z] holds P[x, z];

      defpred R[ Element of A(), Element of ( Fin A())] means ex y be Element of A() st y in $2 & P[y, $1] & for z be Element of A() st z in $2 & P[z, y] holds P[y, z];

      defpred Q[ Element of ( Fin A())] means for x be Element of A() st x in $1 holds R[x, $1];

       A3:

      now

        let B be Element of ( Fin A()), x be Element of A();

        assume

         A4: Q[B];

        thus Q[(B \/ {.x.})]

        proof

          let z be Element of A() such that

           A5: z in (B \/ {x});

          now

            per cases by A5, ZFMISC_1: 136;

              suppose z in B;

              then

              consider y be Element of A() such that

               A6: y in B and

               A7: P[y, z] and

               A8: for x be Element of A() st x in B & P[x, y] holds P[y, x] by A4;

              now

                per cases ;

                  case

                   A9: P[x, y];

                  thus x in (B \/ {x}) by ZFMISC_1: 136;

                  thus P[x, z] by A2, A7, A9;

                  let v be Element of A() such that

                   A10: v in (B \/ {x}) and

                   A11: P[v, x];

                   A12:

                  now

                    assume

                     A13: v in B;

                    P[v, y] by A2, A9, A11;

                    then P[y, v] by A8, A13;

                    hence P[x, v] by A2, A9;

                  end;

                  v in B or v = x by A10, ZFMISC_1: 136;

                  hence P[x, v] by A1, A12;

                end;

                  case

                   A14: not P[x, y];

                  thus y in (B \/ {x}) by A6, XBOOLE_0:def 3;

                  thus P[y, z] by A7;

                  let v be Element of A() such that

                   A15: v in (B \/ {x}) and

                   A16: P[v, y];

                  v in B or v = x by A15, ZFMISC_1: 136;

                  hence P[y, v] by A8, A14, A16;

                end;

              end;

              hence thesis;

            end;

              suppose

               A17: z = x;

              now

                per cases ;

                  case ex w be Element of A() st w in B & P[w, x];

                  then

                  consider w be Element of A() such that

                   A18: w in B and

                   A19: P[w, z] by A17;

                  consider y be Element of A() such that

                   A20: y in B and

                   A21: P[y, w] and

                   A22: for x be Element of A() st x in B & P[x, y] holds P[y, x] by A4, A18;

                  take u = y;

                  thus u in (B \/ {x}) by A20, XBOOLE_0:def 3;

                  thus P[u, z] by A2, A19, A21;

                  let v be Element of A() such that

                   A23: v in (B \/ {x}) and

                   A24: P[v, u];

                  v in B or v = x by A23, ZFMISC_1: 136;

                  hence P[u, v] by A2, A17, A19, A21, A22, A24;

                end;

                  case

                   A25: for w be Element of A() st w in B holds not P[w, x];

                  thus x in (B \/ {x}) by ZFMISC_1: 136;

                  thus

                   A26: P[x, x] by A1;

                  let v be Element of A() such that

                   A27: v in (B \/ {x}) and

                   A28: P[v, x];

                   not v in B by A25, A28;

                  hence P[x, v] by A26, A27, ZFMISC_1: 136;

                end;

              end;

              hence thesis by A17;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A29: Q[( {}. A())];

      for B be Element of ( Fin A()) holds Q[B] from SETWISEO:sch 4( A29, A3);

      hence thesis;

    end;

    scheme :: FRAENKEL:sch24

    FinIm { A,B() -> non empty set , x() -> Element of ( Fin B()) , F( object) -> Element of A() , P[ object, object] } :

ex c1 be Element of ( Fin A()) st for t be Element of A() holds t in c1 iff ex t9 be Element of B() st t9 in x() & t = F(t9) & P[t, t9];

      defpred R[ set] means ex t9 be Element of B() st t9 in x() & $1 = F(t9) & P[$1, t9];

      set c = { F(t9) where t9 be Element of B() : t9 in x() }, c1 = { tt where tt be Element of A() : R[tt] };

      

       A1: c1 c= c

      proof

        let x be object;

        assume x in c1;

        then ex tt be Element of A() st x = tt & ex t9 be Element of B() st t9 in x() & tt = F(t9) & P[tt, t9];

        hence thesis;

      end;

      

       A2: c1 c= A() from FrSet0;

      

       A3: x() is finite;

      c is finite from FraenkelFin( A3);

      then

      reconsider c1 as Element of ( Fin A()) by A1, A2, FINSUB_1:def 5;

      take c1;

      let t be Element of A();

      t in c1 implies ex tt be Element of A() st t = tt & ex t9 be Element of B() st t9 in x() & tt = F(t9) & P[tt, t9];

      hence thesis;

    end;

    registration

      let A,B be finite set;

      cluster ( Funcs (A,B)) -> finite;

      coherence

      proof

        ( bool [:A, B:]) is finite;

        hence thesis by Th2, FINSET_1: 1;

      end;

    end

    theorem :: FRAENKEL:6

    for A,B be set st A is finite & B is finite holds ( Funcs (A,B)) is finite;

    scheme :: FRAENKEL:sch25

    ImFin { A() -> set , B() -> non empty set , X,Y() -> set , F( object) -> object } :

{ F(phi9) where phi9 be Element of ( Funcs (A(),B())) : (phi9 .: X()) c= Y() } is finite

      provided

       A1: X() is finite

       and

       A2: Y() is finite

       and

       A3: for phi,psi be Element of ( Funcs (A(),B())) holds (phi | X()) = (psi | X()) implies F(phi) = F(psi);

      defpred P[ set, set] means for phi be Element of ( Funcs (A(),B())) st (phi | X()) = $1 holds $2 = F(phi);

      set Z = { F(phi9) where phi9 be Element of ( Funcs (A(),B())) : (phi9 .: X()) c= Y() };

      set x = the Element of Z;

      

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

      assume

       A5: not thesis;

      then Z <> {} ;

      then x in Z;

      then

      consider phi be Element of ( Funcs (A(),B())) such that x = F(phi) and

       A6: (phi .: X()) c= Y();

      now

        assume (B() /\ Y()) = {} ;

        then

         A7: (phi .: X()) = {} by A6, XBOOLE_1: 3, XBOOLE_1: 19;

        A() = ( dom phi) by FUNCT_2:def 1;

        then A() misses X() by A7, RELAT_1: 118;

        hence (A() /\ X()) = {} ;

      end;

      then

      reconsider FF = ( Funcs ((A() /\ X()),(B() /\ Y()))), Z as non empty set by A5, FUNCT_2: 8;

      

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

      

       A9: (A() /\ X()) c= A() by XBOOLE_1: 17;

       A10:

      now

        let f be Element of FF;

        consider phi be Element of ( Funcs (A(),B())) such that

         A11: (phi | (A() /\ X())) = f by A9, A4, Th4;

        

         A12: (phi | X()) = f by A11, Th5;

        ex g be Function st f = g & ( dom g) = (A() /\ X()) & ( rng g) c= (B() /\ Y()) by FUNCT_2:def 2;

        then ( rng (phi | X())) c= Y() by A8, A12;

        then (phi .: X()) c= Y() by RELAT_1: 115;

        then F(phi) in Z;

        then

        reconsider g9 = F(phi) as Element of Z;

        take g = g9;

        thus P[f, g] by A3, A12;

      end;

      consider F be Function of FF, Z such that

       A13: for f be Element of FF holds P[f, (F . f)] from FUNCT_2:sch 3( A10);

      Z c= (F .: ( Funcs ((A() /\ X()),(B() /\ Y()))))

      proof

        let y be object;

        assume y in Z;

        then

        consider phi be Element of ( Funcs (A(),B())) such that

         A14: y = F(phi) and

         A15: (phi .: X()) c= Y();

        ( rng (phi | X())) c= Y() by A15, RELAT_1: 115;

        then

         A16: ( rng (phi | X())) c= (B() /\ Y()) by XBOOLE_1: 19;

        

         A17: ( dom (phi | X())) = (( dom phi) /\ X()) by RELAT_1: 61

        .= (A() /\ X()) by FUNCT_2:def 1;

        then

        reconsider x = (phi | X()) as Element of ( Funcs ((A() /\ X()),(B() /\ Y()))) by A16, FUNCT_2:def 2;

        (phi | X()) in ( Funcs ((A() /\ X()),(B() /\ Y()))) by A17, A16, FUNCT_2:def 2;

        then

         A18: x in ( dom F) by FUNCT_2:def 1;

        y = (F . x) by A13, A14;

        hence thesis by A18, FUNCT_1:def 6;

      end;

      hence contradiction by A1, A2, A5;

    end;

    scheme :: FRAENKEL:sch26

    FunctChoice { A() -> non empty set , B() -> non empty set , P[ Element of A(), Element of B()], x() -> Element of ( Fin A()) } :

ex ff be Function of A(), B() st for t be Element of A() st t in x() holds P[t, (ff . t)]

      provided

       A1: for t be Element of A() st t in x() holds ex ff be Element of B() st P[t, ff];

      set b = the Element of B();

      set M = { { ff where ff be Element of B() : P[tt, ff] } where tt be Element of A() : tt in x() };

      set f = the Function of A(), B();

      assume

       A2: not thesis;

      then

      consider t be Element of A() such that

       A3: t in x() and not P[t, (f . t)];

      { ff where ff be Element of B() : P[t, ff] } in M by A3;

      then

      reconsider M as non empty set;

      now

        let X;

        assume X in M;

        then

        consider t be Element of A() such that

         A4: X = { ff where ff be Element of B() : P[t, ff] } and

         A5: t in x();

        consider ff be Element of B() such that

         A6: P[t, ff] by A1, A5;

        ff in X by A4, A6;

        hence X <> {} ;

      end;

      then

      consider Choice be Function such that ( dom Choice) = M and

       A7: X in M implies (Choice . X) in X by FUNCT_1: 111;

      defpred Q[ Element of A(), set] means ($1 in x() implies $2 = (Choice . { ff where ff be Element of B() : P[$1, ff] })) & ($1 in x() or $2 = b);

       A8:

      now

        let t be Element of A();

         A9:

        now

          set s = { ff where ff be Element of B() : P[t, ff] };

          assume t in x();

          then s in M;

          then (Choice . s) in s by A7;

          then ex ff be Element of B() st (Choice . s) = ff & P[t, ff];

          hence (Choice . s) is Element of B();

        end;

        t in x() implies t in x();

        hence ex y be Element of B() st Q[t, y] by A9;

      end;

      consider f be Function of A(), B() such that

       A10: for x be Element of A() holds Q[x, (f . x)] from FUNCT_2:sch 3( A8);

      now

        let t be Element of A();

        assume

         A11: t in x();

        then

         A12: { ff where ff be Element of B() : P[t, ff] } in M;

        (f . t) = (Choice . { ff where ff be Element of B() : P[t, ff] }) by A10, A11;

        then (f . t) in { ff where ff be Element of B() : P[t, ff] } by A7, A12;

        then ex ff be Element of B() st (f . t) = ff & P[t, ff];

        hence P[t, (f . t)];

      end;

      hence contradiction by A2;

    end;

    scheme :: FRAENKEL:sch27

    FuncsChoice { A() -> non empty set , B() -> non empty set , P[ Element of A(), Element of B()], x() -> Element of ( Fin A()) } :

ex ff be Element of ( Funcs (A(),B())) st for t be Element of A() st t in x() holds P[t, (ff . t)]

      provided

       A1: for t be Element of A() st t in x() holds ex ff be Element of B() st P[t, ff];

      

       A2: for t be Element of A() st t in x() holds ex ff be Element of B() st P[t, ff] by A1;

      consider ff be Function of A(), B() such that

       A3: for t be Element of A() st t in x() holds P[t, (ff . t)] from FunctChoice( A2);

      reconsider ff as Element of ( Funcs (A(),B())) by FUNCT_2: 8;

      take ff;

      thus thesis by A3;

    end;

    scheme :: FRAENKEL:sch28

    FraenkelFin9 { A,B() -> non empty set , X() -> set , P[ object, object] } :

{ x where x be Element of B() : ex w be Element of A() st P[w, x] & w in X() } is finite

      provided

       A1: X() is finite

       and

       A2: for w be Element of A(), x,y be Element of B() st P[w, x] & P[w, y] holds x = y;

      set M = { x where x be Element of B() : ex w be Element of A() st P[w, x] & w in X() };

      defpred Q[ object, object] means P[$1, $2] & $1 in X() & $2 in B();

      

       A3: for x,y be object st x in A() & Q[x, y] holds y in B();

      

       A4: for x,y1,y2 be object st x in A() & Q[x, y1] & Q[x, y2] holds y1 = y2 by A2;

      consider f be PartFunc of A(), B() such that

       A5: for x be object holds x in ( dom f) iff x in A() & ex y be object st Q[x, y] and

       A6: for x be object st x in ( dom f) holds Q[x, (f . x)] from PARTFUN1:sch 2( A3, A4);

      M = (f .: X())

      proof

        thus M c= (f .: X())

        proof

          let x be object;

          assume x in M;

          then

          consider u be Element of B() such that

           A7: x = u and

           A8: ex w be Element of A() st P[w, u] & w in X();

          consider w be Element of A() such that

           A9: P[w, u] and

           A10: w in X() by A8;

          

           A11: w in ( dom f) by A5, A9, A10;

          then Q[w, (f . w)] by A6;

          then (f . w) = x by A2, A7, A9;

          hence thesis by A10, A11, FUNCT_1:def 6;

        end;

        let x be object;

        assume x in (f .: X());

        then

        consider y be object such that

         A12: y in ( dom f) and

         A13: y in X() and

         A14: x = (f . y) by FUNCT_1:def 6;

        reconsider x as Element of B() by A6, A12, A14;

        P[y, x] by A6, A12, A14;

        hence thesis by A12, A13;

      end;

      hence thesis by A1;

    end;