zf_model.miz



    begin

    reserve F,H,H9 for ZF-formula,

x,y,z,t for Variable,

a,b,c,d,A,X for set;

    scheme :: ZF_MODEL:sch1

    ZFschex { F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set) -> set , F4( set, set) -> set , F5( Variable, set) -> set , H() -> ZF-formula } :

ex a, A st (for x, y holds [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A) & [H(), a] in A & for H, a st [H, a] in A holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A);

      defpred Graph[ set, ZF-formula, set] means (for x, y holds [(x '=' y), F1(x,y)] in $1 & [(x 'in' y), F2(x,y)] in $1) & [$2, $3] in $1 & for H, a st [H, a] in $1 holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in $1) & (H is conjunctive implies ex b, c st a = F4(b,c) & ( [( the_left_argument_of H), b] in $1 & [( the_right_argument_of H), c] in $1)) & (H is universal implies ex b st (a = F5(bound_in,b) & [( the_scope_of H), b] in $1));

      defpred Ind[ ZF-formula] means ex a, A st Graph[A, $1, a];

      

       A1: H is atomic implies Ind[H]

      proof

        assume

         A2: H is being_equality or H is being_membership;

        then

        consider a such that

         A3: H is being_equality & a = F1(Var1,Var2) or H is being_membership & a = F2(Var1,Var2);

        take a, X = ({ [(x '=' y), F1(x,y)] : x = x } \/ { [(z 'in' t), F2(z,t)] : z = z });

         A4:

        now

          assume H is being_membership;

          then (H . 1) = 1 & H = (( Var1 H) 'in' ( Var2 H)) by ZF_LANG: 19, ZF_LANG: 37;

          then [H, a] in { [(x 'in' y), F2(x,y)] : x = x } by A3, ZF_LANG: 18;

          hence [H, a] in X by XBOOLE_0:def 3;

        end;

        thus for x, y holds [(x '=' y), F1(x,y)] in X & [(x 'in' y), F2(x,y)] in X

        proof

          let x, y;

           [(x '=' y), F1(x,y)] in { [(z '=' t), F1(z,t)] : z = z };

          hence [(x '=' y), F1(x,y)] in X by XBOOLE_0:def 3;

           [(x 'in' y), F2(x,y)] in { [(z 'in' t), F2(z,t)] : z = z };

          hence thesis by XBOOLE_0:def 3;

        end;

        now

          assume H is being_equality;

          then (H . 1) = 0 & H = (( Var1 H) '=' ( Var2 H)) by ZF_LANG: 18, ZF_LANG: 36;

          then [H, a] in { [(x '=' y), F1(x,y)] : x = x } by A3, ZF_LANG: 19;

          hence [H, a] in X by XBOOLE_0:def 3;

        end;

        hence [H, a] in X by A2, A4;

        let H, a;

         A5:

        now

          assume [H, a] in { [(z 'in' t), F2(z,t)] : z = z };

          then

          consider x, y such that

           A6: [H, a] = [(x 'in' y), F2(x,y)] and x = x;

          H = (x 'in' y) by A6, XTUPLE_0: 1;

          hence (H . 1) = 1 by ZF_LANG: 15;

        end;

        assume

         A7: [H, a] in X;

        then

         A8: [H, a] in { [(x '=' y), F1(x,y)] : x = x } or [H, a] in { [(z 'in' t), F2(z,t)] : z = z } by XBOOLE_0:def 3;

        thus H is being_equality implies a = F1(Var1,Var2)

        proof

          assume

           A9: H is being_equality;

          then

           A10: H = (( Var1 H) '=' ( Var2 H)) by ZF_LANG: 36;

          

           A11: (H . 1) = 0 by A9, ZF_LANG: 18;

           [H, a] <> [(x 'in' y), F2(x,y)]

          proof

            H <> (x 'in' y) by A11, ZF_LANG: 15;

            hence thesis by XTUPLE_0: 1;

          end;

          then not ex x, y st [H, a] = [(x 'in' y), F2(x,y)] & x = x;

          then

          consider x, y such that

           A12: [H, a] = [(x '=' y), F1(x,y)] and x = x by A8;

          H = (x '=' y) by A12, XTUPLE_0: 1;

          then ( Var1 H) = x & ( Var2 H) = y by A10, ZF_LANG: 1;

          hence thesis by A12, XTUPLE_0: 1;

        end;

        thus H is being_membership implies a = F2(Var1,Var2)

        proof

          assume

           A13: H is being_membership;

          then

           A14: H = (( Var1 H) 'in' ( Var2 H)) by ZF_LANG: 37;

          

           A15: (H . 1) = 1 by A13, ZF_LANG: 19;

           [H, a] <> [(x '=' y), F1(x,y)]

          proof

            H <> (x '=' y) by A15, ZF_LANG: 15;

            hence thesis by XTUPLE_0: 1;

          end;

          then not ex x, y st [H, a] = [(x '=' y), F1(x,y)] & x = x;

          then

          consider x, y such that

           A16: [H, a] = [(x 'in' y), F2(x,y)] and x = x by A8;

          H = (x 'in' y) by A16, XTUPLE_0: 1;

          then ( Var1 H) = x & ( Var2 H) = y by A14, ZF_LANG: 2;

          hence thesis by A16, XTUPLE_0: 1;

        end;

        now

          assume [H, a] in { [(x '=' y), F1(x,y)] : x = x };

          then

          consider x, y such that

           A17: [H, a] = [(x '=' y), F1(x,y)] and x = x;

          H = (x '=' y) by A17, XTUPLE_0: 1;

          hence (H . 1) = 0 by ZF_LANG: 15;

        end;

        hence thesis by A7, A5, XBOOLE_0:def 3, ZF_LANG: 20, ZF_LANG: 21, ZF_LANG: 22;

      end;

      

       A18: for H st H is conjunctive & Ind[( the_left_argument_of H)] & Ind[( the_right_argument_of H)] holds Ind[H]

      proof

        let H;

        assume H is conjunctive;

        then

         A19: (H . 1) = 3 by ZF_LANG: 21;

        given a1 be set, A1 be set such that

         A20: Graph[A1, ( the_left_argument_of H), a1];

        given a2 be set, A2 be set such that

         A21: Graph[A2, ( the_right_argument_of H), a2];

        take a = F4(a1,a2), X = ((A1 \/ A2) \/ { [H, a]});

        thus for x, y holds [(x '=' y), F1(x,y)] in X & [(x 'in' y), F2(x,y)] in X

        proof

          let x, y;

           [(x 'in' y), F2(x,y)] in A1 by A20;

          then

           A22: [(x 'in' y), F2(x,y)] in (A1 \/ A2) by XBOOLE_0:def 3;

           [(x '=' y), F1(x,y)] in A1 by A20;

          then [(x '=' y), F1(x,y)] in (A1 \/ A2) by XBOOLE_0:def 3;

          hence thesis by A22, XBOOLE_0:def 3;

        end;

         [H, a] in { [H, a]} by TARSKI:def 1;

        hence [H, a] in X by XBOOLE_0:def 3;

        let F, c;

        

         A23: [F, c] = [H, a] implies F = H & c = a by XTUPLE_0: 1;

        assume [F, c] in X;

        then

         A24: [F, c] in (A1 \/ A2) or [F, c] in { [H, a]} by XBOOLE_0:def 3;

        then

         A25: [F, c] in A1 or [F, c] in A2 or [F, c] = [H, a] by TARSKI:def 1, XBOOLE_0:def 3;

        hence F is being_equality implies c = F1(Var1,Var2) by A20, A21, A23, A19, ZF_LANG: 18;

         not H is being_membership by A19, ZF_LANG: 19;

        hence F is being_membership implies c = F2(Var1,Var2) by A20, A21, A25, XTUPLE_0: 1;

        thus F is negative implies ex b st c = F3(b) & [( the_argument_of F), b] in X

        proof

          assume

           A26: F is negative;

           A27:

          now

            assume [F, c] in A2;

            then

            consider b such that

             A28: c = F3(b) and

             A29: [( the_argument_of F), b] in A2 by A21, A26;

             [( the_argument_of F), b] in (A1 \/ A2) by A29, XBOOLE_0:def 3;

            then [( the_argument_of F), b] in X by XBOOLE_0:def 3;

            hence thesis by A28;

          end;

          now

            assume [F, c] in A1;

            then

            consider b such that

             A30: c = F3(b) and

             A31: [( the_argument_of F), b] in A1 by A20, A26;

             [( the_argument_of F), b] in (A1 \/ A2) by A31, XBOOLE_0:def 3;

            then [( the_argument_of F), b] in X by XBOOLE_0:def 3;

            hence thesis by A30;

          end;

          hence thesis by A24, A23, A19, A26, A27, TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG: 20;

        end;

        thus F is conjunctive implies ex b, d st c = F4(b,d) & [( the_left_argument_of F), b] in X & [( the_right_argument_of F), d] in X

        proof

          assume

           A32: F is conjunctive;

           A33:

          now

            assume [F, c] in A1;

            then

            consider b, d such that

             A34: c = F4(b,d) and

             A35: [( the_left_argument_of F), b] in A1 and

             A36: [( the_right_argument_of F), d] in A1 by A20, A32;

             [( the_right_argument_of F), d] in (A1 \/ A2) by A36, XBOOLE_0:def 3;

            then

             A37: [( the_right_argument_of F), d] in X by XBOOLE_0:def 3;

             [( the_left_argument_of F), b] in (A1 \/ A2) by A35, XBOOLE_0:def 3;

            then [( the_left_argument_of F), b] in X by XBOOLE_0:def 3;

            hence thesis by A34, A37;

          end;

           A38:

          now

            assume [F, c] in A2;

            then

            consider b, d such that

             A39: c = F4(b,d) and

             A40: [( the_left_argument_of F), b] in A2 and

             A41: [( the_right_argument_of F), d] in A2 by A21, A32;

             [( the_right_argument_of F), d] in (A1 \/ A2) by A41, XBOOLE_0:def 3;

            then

             A42: [( the_right_argument_of F), d] in X by XBOOLE_0:def 3;

             [( the_left_argument_of F), b] in (A1 \/ A2) by A40, XBOOLE_0:def 3;

            then [( the_left_argument_of F), b] in X by XBOOLE_0:def 3;

            hence thesis by A39, A42;

          end;

          now

            assume

             A43: [F, c] = [H, a];

            then [( the_right_argument_of F), a2] in (A1 \/ A2) by A21, A23, XBOOLE_0:def 3;

            then

             A44: [( the_right_argument_of F), a2] in X by XBOOLE_0:def 3;

             [( the_left_argument_of F), a1] in (A1 \/ A2) by A20, A23, A43, XBOOLE_0:def 3;

            then [( the_left_argument_of F), a1] in X by XBOOLE_0:def 3;

            hence thesis by A23, A43, A44;

          end;

          hence thesis by A24, A33, A38, TARSKI:def 1, XBOOLE_0:def 3;

        end;

        thus F is universal implies ex b st c = F5(bound_in,b) & [( the_scope_of F), b] in X

        proof

          assume

           A45: F is universal;

           A46:

          now

            assume [F, c] in A2;

            then

            consider b such that

             A47: c = F5(bound_in,b) and

             A48: [( the_scope_of F), b] in A2 by A21, A45;

             [( the_scope_of F), b] in (A1 \/ A2) by A48, XBOOLE_0:def 3;

            then [( the_scope_of F), b] in X by XBOOLE_0:def 3;

            hence thesis by A47;

          end;

          now

            assume [F, c] in A1;

            then

            consider b such that

             A49: c = F5(bound_in,b) and

             A50: [( the_scope_of F), b] in A1 by A20, A45;

             [( the_scope_of F), b] in (A1 \/ A2) by A50, XBOOLE_0:def 3;

            then [( the_scope_of F), b] in X by XBOOLE_0:def 3;

            hence thesis by A49;

          end;

          hence thesis by A24, A23, A19, A45, A46, TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG: 22;

        end;

      end;

      

       A51: for H st H is universal & Ind[( the_scope_of H)] holds Ind[H]

      proof

        let H;

        assume H is universal;

        then

         A52: (H . 1) = 4 by ZF_LANG: 22;

        given a, A such that

         A53: Graph[A, ( the_scope_of H), a];

        take b = F5(bound_in,a), X = (A \/ { [H, b]});

        thus for x, y holds [(x '=' y), F1(x,y)] in X & [(x 'in' y), F2(x,y)] in X

        proof

          let x, y;

           [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A by A53;

          hence thesis by XBOOLE_0:def 3;

        end;

         [H, b] in { [H, b]} by TARSKI:def 1;

        hence [H, b] in X by XBOOLE_0:def 3;

        let F, c;

        

         A54: [F, c] = [H, b] implies F = H & c = b by XTUPLE_0: 1;

        assume [F, c] in X;

        then

         A55: [F, c] in A or [F, c] in { [H, b]} by XBOOLE_0:def 3;

        hence F is being_equality implies c = F1(Var1,Var2) by A53, A54, A52, TARSKI:def 1, ZF_LANG: 18;

        thus F is being_membership implies c = F2(Var1,Var2) by A53, A55, A54, A52, TARSKI:def 1, ZF_LANG: 19;

        thus F is negative implies ex b st c = F3(b) & [( the_argument_of F), b] in X

        proof

          assume F is negative;

          then

          consider b such that

           A56: c = F3(b) and

           A57: [( the_argument_of F), b] in A by A53, A55, A54, A52, TARSKI:def 1, ZF_LANG: 20;

           [( the_argument_of F), b] in X by A57, XBOOLE_0:def 3;

          hence thesis by A56;

        end;

        thus F is conjunctive implies ex b, d st c = F4(b,d) & [( the_left_argument_of F), b] in X & [( the_right_argument_of F), d] in X

        proof

          assume F is conjunctive;

          then

          consider b, d such that

           A58: c = F4(b,d) & [( the_left_argument_of F), b] in A & [( the_right_argument_of F), d] in A by A53, A55, A54, A52, TARSKI:def 1, ZF_LANG: 21;

          take b, d;

          thus thesis by A58, XBOOLE_0:def 3;

        end;

        thus F is universal implies ex b st c = F5(bound_in,b) & [( the_scope_of F), b] in X

        proof

          assume

           A59: F is universal;

           A60:

          now

            assume [F, c] in A;

            then

            consider b such that

             A61: c = F5(bound_in,b) and

             A62: [( the_scope_of F), b] in A by A53, A59;

             [( the_scope_of F), b] in X by A62, XBOOLE_0:def 3;

            hence thesis by A61;

          end;

          now

            assume

             A63: [F, c] = [H, b];

            then [( the_scope_of F), a] in X by A53, A54, XBOOLE_0:def 3;

            hence thesis by A54, A63;

          end;

          hence thesis by A55, A60, TARSKI:def 1;

        end;

      end;

      

       A64: for H st H is negative & Ind[( the_argument_of H)] holds Ind[H]

      proof

        let H;

        assume H is negative;

        then

         A65: (H . 1) = 2 by ZF_LANG: 20;

        given a, A such that

         A66: Graph[A, ( the_argument_of H), a];

        take b = F3(a), X = (A \/ { [H, b]});

        thus for x, y holds [(x '=' y), F1(x,y)] in X & [(x 'in' y), F2(x,y)] in X

        proof

          let x, y;

           [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A by A66;

          hence thesis by XBOOLE_0:def 3;

        end;

         [H, b] in { [H, b]} by TARSKI:def 1;

        hence [H, b] in X by XBOOLE_0:def 3;

        let F, c;

        

         A67: [F, c] = [H, b] implies F = H & c = b by XTUPLE_0: 1;

        assume [F, c] in X;

        then

         A68: [F, c] in A or [F, c] in { [H, b]} by XBOOLE_0:def 3;

        hence F is being_equality implies c = F1(Var1,Var2) by A66, A67, A65, TARSKI:def 1, ZF_LANG: 18;

        thus F is being_membership implies c = F2(Var1,Var2) by A66, A68, A67, A65, TARSKI:def 1, ZF_LANG: 19;

        thus F is negative implies ex b st c = F3(b) & [( the_argument_of F), b] in X

        proof

          assume

           A69: F is negative;

           A70:

          now

            assume [F, c] in A;

            then

            consider d such that

             A71: c = F3(d) and

             A72: [( the_argument_of F), d] in A by A66, A69;

             [( the_argument_of F), d] in X by A72, XBOOLE_0:def 3;

            hence thesis by A71;

          end;

          now

            assume

             A73: [F, c] = [H, b];

            then [( the_argument_of F), a] in X by A66, A67, XBOOLE_0:def 3;

            hence thesis by A67, A73;

          end;

          hence thesis by A68, A70, TARSKI:def 1;

        end;

        thus F is conjunctive implies ex b, d st c = F4(b,d) & [( the_left_argument_of F), b] in X & [( the_right_argument_of F), d] in X

        proof

          assume F is conjunctive;

          then

          consider b, d such that

           A74: c = F4(b,d) & [( the_left_argument_of F), b] in A & [( the_right_argument_of F), d] in A by A66, A68, A67, A65, TARSKI:def 1, ZF_LANG: 21;

          take b, d;

          thus thesis by A74, XBOOLE_0:def 3;

        end;

        thus F is universal implies ex b st c = F5(bound_in,b) & [( the_scope_of F), b] in X

        proof

          assume F is universal;

          then

          consider b such that

           A75: c = F5(bound_in,b) & [( the_scope_of F), b] in A by A66, A68, A67, A65, TARSKI:def 1, ZF_LANG: 22;

          take b;

          thus thesis by A75, XBOOLE_0:def 3;

        end;

      end;

      for H holds Ind[H] from ZF_LANG:sch 1( A1, A64, A18, A51);

      hence thesis;

    end;

    scheme :: ZF_MODEL:sch2

    ZFschuniq { F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set) -> set , F4( set, set) -> set , F5( Variable, set) -> set , H() -> ZF-formula , a() -> set , b() -> set } :

a() = b()

      provided

       A1: ex A st (for x, y holds [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A) & [H(), a()] in A & for H, a st [H, a] in A holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A)

       and

       A2: ex A st (for x, y holds [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A) & [H(), b()] in A & for H, a st [H, a] in A holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A);

      consider A1 be set such that for x, y holds [(x '=' y), F1(x,y)] in A1 & [(x 'in' y), F2(x,y)] in A1 and

       A3: [H(), a()] in A1 and

       A4: for H, a st [H, a] in A1 holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A1) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A1 & [( the_right_argument_of H), c] in A1) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A1) by A1;

      consider A2 be set such that for x, y holds [(x '=' y), F1(x,y)] in A2 & [(x 'in' y), F2(x,y)] in A2 and

       A5: [H(), b()] in A2 and

       A6: for H, a st [H, a] in A2 holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A2) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A2 & [( the_right_argument_of H), c] in A2) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A2) by A2;

      defpred P[ ZF-formula] means for a, b st [$1, a] in A1 & [$1, b] in A2 holds a = b;

      

       A7: for H st H is universal & P[( the_scope_of H)] holds P[H]

      proof

        let H such that

         A8: H is universal and

         A9: for a, b st [( the_scope_of H), a] in A1 & [( the_scope_of H), b] in A2 holds a = b;

        let a, b;

        assume [H, a] in A1 & [H, b] in A2;

        then (ex a1 be set st a = F5(bound_in,a1) & [( the_scope_of H), a1] in A1) & ex b1 be set st b = F5(bound_in,b1) & [( the_scope_of H), b1] in A2 by A4, A6, A8;

        hence thesis by A9;

      end;

      

       A10: for H st H is atomic holds P[H]

      proof

        let H such that

         A11: H is being_equality or H is being_membership;

        let a, b such that

         A12: [H, a] in A1 and

         A13: [H, b] in A2;

         A14:

        now

          assume

           A15: H is being_membership;

          then a = F2(Var1,Var2) by A4, A12;

          hence thesis by A6, A13, A15;

        end;

        now

          assume

           A16: H is being_equality;

          then a = F1(Var1,Var2) by A4, A12;

          hence thesis by A6, A13, A16;

        end;

        hence thesis by A11, A14;

      end;

      

       A17: for H st H is conjunctive & P[( the_left_argument_of H)] & P[( the_right_argument_of H)] holds P[H]

      proof

        let H such that

         A18: H is conjunctive and

         A19: for a, b st [( the_left_argument_of H), a] in A1 & [( the_left_argument_of H), b] in A2 holds a = b and

         A20: for a, b st [( the_right_argument_of H), a] in A1 & [( the_right_argument_of H), b] in A2 holds a = b;

        let a, b;

        assume that

         A21: [H, a] in A1 and

         A22: [H, b] in A2;

        consider a1,a2 be set such that

         A23: a = F4(a1,a2) and

         A24: [( the_left_argument_of H), a1] in A1 and

         A25: [( the_right_argument_of H), a2] in A1 by A4, A18, A21;

        consider b1,b2 be set such that

         A26: b = F4(b1,b2) and

         A27: [( the_left_argument_of H), b1] in A2 and

         A28: [( the_right_argument_of H), b2] in A2 by A6, A18, A22;

        a1 = b1 by A19, A24, A27;

        hence thesis by A20, A23, A25, A26, A28;

      end;

      

       A29: for H st H is negative & P[( the_argument_of H)] holds P[H]

      proof

        let H such that

         A30: H is negative and

         A31: for a, b st [( the_argument_of H), a] in A1 & [( the_argument_of H), b] in A2 holds a = b;

        let a, b;

        assume [H, a] in A1 & [H, b] in A2;

        then (ex a1 be set st a = F3(a1) & [( the_argument_of H), a1] in A1) & ex b1 be set st b = F3(b1) & [( the_argument_of H), b1] in A2 by A4, A6, A30;

        hence thesis by A31;

      end;

      for H holds P[H] from ZF_LANG:sch 1( A10, A29, A17, A7);

      hence thesis by A3, A5;

    end;

    scheme :: ZF_MODEL:sch3

    ZFschresult { F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set) -> set , F4( set, set) -> set , F5( Variable, set) -> set , H() -> ZF-formula , f( ZF-formula) -> set } :

(H() is being_equality implies f(H) = F1(Var1,Var2)) & (H() is being_membership implies f(H) = F2(Var1,Var2)) & (H() is negative implies f(H) = F3(f)) & (H() is conjunctive implies for a, b st a = f(the_left_argument_of) & b = f(the_right_argument_of) holds f(H) = F4(a,b)) & (H() is universal implies f(H) = F5(bound_in,f))

      provided

       A1: for H9, a holds a = f(H9) iff ex A st (for x, y holds [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A) & [H9, a] in A & for H, a st [H, a] in A holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A);

      consider A such that

       A2: for x, y holds [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A and

       A3: [H(), f(H)] in A and

       A4: for H, a st [H, a] in A holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A) by A1;

      thus H() is being_equality implies f(H) = F1(Var1,Var2) by A3, A4;

      thus H() is being_membership implies f(H) = F2(Var1,Var2) by A3, A4;

      thus H() is negative implies f(H) = F3(f)

      proof

        assume H() is negative;

        then ex b st f(H) = F3(b) & [( the_argument_of H()), b] in A by A3, A4;

        hence thesis by A1, A2, A4;

      end;

      thus H() is conjunctive implies for a, b st a = f(the_left_argument_of) & b = f(the_right_argument_of) holds f(H) = F4(a,b)

      proof

        assume H() is conjunctive;

        then

        consider b, c such that

         A5: f(H) = F4(b,c) and

         A6: [( the_left_argument_of H()), b] in A and

         A7: [( the_right_argument_of H()), c] in A by A3, A4;

        

         A8: f(the_left_argument_of) = b by A1, A2, A4, A6;

        let a1,a2 be set;

        assume a1 = f(the_left_argument_of) & a2 = f(the_right_argument_of);

        hence thesis by A1, A2, A4, A5, A7, A8;

      end;

      thus H() is universal implies f(H) = F5(bound_in,f)

      proof

        assume H() is universal;

        then ex b st f(H) = F5(bound_in,b) & [( the_scope_of H()), b] in A by A3, A4;

        hence thesis by A1, A2, A4;

      end;

    end;

    scheme :: ZF_MODEL:sch4

    ZFschproperty { F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set) -> set , F4( set, set) -> set , F5( Variable, set) -> set , f( ZF-formula) -> set , H() -> ZF-formula , P[ set] } :

P[f(H)]

      provided

       A1: for H9, a holds a = f(H9) iff ex A st (for x, y holds [(x '=' y), F1(x,y)] in A & [(x 'in' y), F2(x,y)] in A) & [H9, a] in A & for H, a st [H, a] in A holds (H is being_equality implies a = F1(Var1,Var2)) & (H is being_membership implies a = F2(Var1,Var2)) & (H is negative implies ex b st a = F3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = F4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = F5(bound_in,b) & [( the_scope_of H), b] in A)

       and

       A2: for x, y holds P[F1(x,y)] & P[F2(x,y)]

       and

       A3: for a st P[a] holds P[F3(a)]

       and

       A4: for a, b st P[a] & P[b] holds P[F4(a,b)]

       and

       A5: for a, x st P[a] holds P[F5(x,a)];

      defpred Pf[ ZF-formula] means P[f($1)];

      deffunc g( ZF-formula) = f($1);

      deffunc f5( Variable, set) = F5($1,$2);

      deffunc f4( set, set) = F4($1,$2);

      deffunc f3( set) = F3($1);

      deffunc f2( Variable, Variable) = F2($1,$2);

      deffunc f1( Variable, Variable) = F1($1,$2);

      

       A6: for H9, a holds a = g(H9) iff ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H9, a] in A & for H, a st [H, a] in A holds (H is being_equality implies a = f1(Var1,Var2)) & (H is being_membership implies a = f2(Var1,Var2)) & (H is negative implies ex b st a = f3(b) & [( the_argument_of H), b] in A) & (H is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H), b] in A & [( the_right_argument_of H), c] in A) & (H is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H), b] in A) by A1;

       A7:

      now

        let H;

        thus (H is being_equality implies g(H) = f1(Var1,Var2)) & (H is being_membership implies g(H) = f2(Var1,Var2)) & (H is negative implies g(H) = f3(g)) & (H is conjunctive implies for a, b st a = g(the_left_argument_of) & b = g(the_right_argument_of) holds g(H) = f4(a,b)) & (H is universal implies g(H) = f5(bound_in,g)) from ZFschresult( A6);

      end;

      

       A8: for H st H is negative & Pf[( the_argument_of H)] holds Pf[H]

      proof

        let H;

        assume H is negative;

        then f(H) = F3(f) by A7;

        hence thesis by A3;

      end;

      

       A9: for H st H is universal & Pf[( the_scope_of H)] holds Pf[H]

      proof

        let H;

        assume H is universal;

        then f(H) = F5(bound_in,f) by A7;

        hence thesis by A5;

      end;

      

       A10: for H st H is conjunctive & Pf[( the_left_argument_of H)] & Pf[( the_right_argument_of H)] holds Pf[H]

      proof

        let H;

        assume H is conjunctive;

        then f(H) = F4(f,f) by A7;

        hence thesis by A4;

      end;

      

       A11: for H st H is atomic holds Pf[H]

      proof

        let H;

        assume H is being_equality or H is being_membership;

        then f(H) = F1(Var1,Var2) or f(H) = F2(Var1,Var2) by A7;

        hence thesis by A2;

      end;

      for H holds Pf[H] from ZF_LANG:sch 1( A11, A8, A10, A9);

      hence thesis;

    end;

    deffunc f1( Variable, Variable) = {$1, $2};

    deffunc f2( Variable, Variable) = {$1, $2};

    deffunc f3( set) = $1;

    deffunc f4( set, set) = ( union {$1, $2});

    deffunc f5( Variable, set) = ($2 \ {$1});

    definition

      let H;

      :: ZF_MODEL:def1

      func Free H -> set means

      : Def1: ex A st (for x, y holds [(x '=' y), {x, y}] in A & [(x 'in' y), {x, y}] in A) & [H, it ] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = {( Var1 H9), ( Var2 H9)}) & (H9 is being_membership implies a = {( Var1 H9), ( Var2 H9)}) & (H9 is negative implies ex b st a = b & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = ( union {b, c}) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = (b \ {( bound_in H9)}) & [( the_scope_of H9), b] in A);

      existence

      proof

        thus ex a, A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) from ZFschex;

      end;

      uniqueness

      proof

        let a1,a2 be set such that

         A1: ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a1] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) and

         A2: ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a2] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A);

        thus a1 = a2 from ZFschuniq( A1, A2);

      end;

    end

    deffunc f( ZF-formula) = ( Free $1);

    

     Lm1: for H holds for a1 be set holds a1 = f(H) iff ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a1] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) by Def1;

     Lm2:

    now

      let H;

      thus (H is being_equality implies f(H) = f1(Var1,Var2)) & (H is being_membership implies f(H) = f2(Var1,Var2)) & (H is negative implies f(H) = f3(f)) & (H is conjunctive implies for a, b st a = f(the_left_argument_of) & b = f(the_right_argument_of) holds f(H) = f4(a,b)) & (H is universal implies f(H) = f5(bound_in,f)) from ZFschresult( Lm1);

    end;

    definition

      let H;

      :: original: Free

      redefine

      func Free H -> Subset of VAR ;

      coherence

      proof

        defpred P[ set] means $1 is Subset of VAR ;

        

         A1: P[ f1(x,y)] & P[ f2(x,y)]

        proof

           {x, y} c= VAR

          proof

            let a be object;

            assume a in {x, y};

            then a = x or a = y by TARSKI:def 2;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A2: P[a] & P[b] implies P[ f4(a,b)]

        proof

          assume

           A3: a is Subset of VAR & b is Subset of VAR ;

          ( union {a, b}) c= VAR

          proof

            let c be object;

            assume c in ( union {a, b});

            then

            consider X such that

             A4: c in X and

             A5: X in {a, b} by TARSKI:def 4;

            X is Subset of VAR by A3, A5, TARSKI:def 2;

            hence thesis by A4;

          end;

          hence thesis;

        end;

        

         A6: for a, x st P[a] holds P[ f5(x,a)] by XBOOLE_1: 1;

        

         A7: P[a] implies P[ f3(a)];

        thus P[ f(H)] from ZFschproperty( Lm1, A1, A7, A2, A6);

      end;

    end

    theorem :: ZF_MODEL:1

    for H holds (H is being_equality implies ( Free H) = {( Var1 H), ( Var2 H)}) & (H is being_membership implies ( Free H) = {( Var1 H), ( Var2 H)}) & (H is negative implies ( Free H) = ( Free ( the_argument_of H))) & (H is conjunctive implies ( Free H) = (( Free ( the_left_argument_of H)) \/ ( Free ( the_right_argument_of H)))) & (H is universal implies ( Free H) = (( Free ( the_scope_of H)) \ {( bound_in H)}))

    proof

      let H;

      thus (H is being_equality implies ( Free H) = {( Var1 H), ( Var2 H)}) & (H is being_membership implies ( Free H) = {( Var1 H), ( Var2 H)}) & (H is negative implies ( Free H) = ( Free ( the_argument_of H))) by Lm2;

      thus H is conjunctive implies ( Free H) = (( Free ( the_left_argument_of H)) \/ ( Free ( the_right_argument_of H)))

      proof

        assume H is conjunctive;

        

        hence ( Free H) = ( union {( Free ( the_left_argument_of H)), ( Free ( the_right_argument_of H))}) by Lm2

        .= (( Free ( the_left_argument_of H)) \/ ( Free ( the_right_argument_of H))) by ZFMISC_1: 75;

      end;

      assume H is universal;

      hence thesis by Lm2;

    end;

    definition

      let D be non empty set;

      :: ZF_MODEL:def2

      func VAL D -> set equals ( Funcs ( VAR ,D));

      coherence ;

    end

    registration

      let D be non empty set;

      cluster ( VAL D) -> non empty;

      coherence ;

    end

    reserve E for non empty set,

f,g,h for Function of VAR , E,

v1,v2,v3,v4,v5,u5 for Element of ( VAL E);

    definition

      deffunc f4( set, set) = ($1 /\ $2);

      let H, E;

      deffunc f1( Variable, Variable) = { v3 : for f st f = v3 holds (f . $1) = (f . $2) };

      deffunc f2( Variable, Variable) = { v3 : for f st f = v3 holds (f . $1) in (f . $2) };

      deffunc f3( set) = (( VAL E) \ $1);

      deffunc f5( Variable, set) = { v5 : for X, f st X = $2 & f = v5 holds f in X & for g st for y st (g . y) <> (f . y) holds $1 = y holds g in X };

      :: ZF_MODEL:def3

      func St (H,E) -> set means

      : Def3: ex A st (for x, y holds [(x '=' y), { v1 : for f st f = v1 holds (f . x) = (f . y) }] in A & [(x 'in' y), { v2 : for f st f = v2 holds (f . x) in (f . y) }] in A) & [H, it ] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = { v3 : for f st f = v3 holds (f . ( Var1 H9)) = (f . ( Var2 H9)) }) & (H9 is being_membership implies a = { v4 : for f st f = v4 holds (f . ( Var1 H9)) in (f . ( Var2 H9)) }) & (H9 is negative implies ex b st a = (( VAL E) \ b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = (b /\ c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = { v5 : for X, f st X = b & f = v5 holds f in X & for g st for y st (g . y) <> (f . y) holds ( bound_in H9) = y holds g in X } & [( the_scope_of H9), b] in A);

      existence

      proof

        thus ex a, A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) from ZFschex;

      end;

      uniqueness

      proof

        let a1,a2 be set such that

         A1: ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a1] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) and

         A2: ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a2] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A);

        thus a1 = a2 from ZFschuniq( A1, A2);

      end;

    end

     Lm3:

    now

      deffunc f4( set, set) = ($1 /\ $2);

      let H, E;

      deffunc f1( Variable, Variable) = { v3 : for f st f = v3 holds (f . $1) = (f . $2) };

      deffunc f2( Variable, Variable) = { v3 : for f st f = v3 holds (f . $1) in (f . $2) };

      deffunc f3( set) = (( VAL E) \ $1);

      deffunc f5( Variable, set) = { v5 : for X, f st X = $2 & f = v5 holds f in X & for g st for y st (g . y) <> (f . y) holds $1 = y holds g in X };

      deffunc f( ZF-formula) = ( St ($1,E));

      

       A1: for H, a holds a = f(H) iff ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) by Def3;

      thus (H is being_equality implies f(H) = f1(Var1,Var2)) & (H is being_membership implies f(H) = f2(Var1,Var2)) & (H is negative implies f(H) = f3(f)) & (H is conjunctive implies for a, b st a = f(the_left_argument_of) & b = f(the_right_argument_of) holds f(H) = f4(a,b)) & (H is universal implies f(H) = f5(bound_in,f)) from ZFschresult( A1);

    end;

    definition

      let H, E;

      :: original: St

      redefine

      func St (H,E) -> Subset of ( VAL E) ;

      coherence

      proof

        defpred P[ set] means $1 is Subset of ( VAL E);

        deffunc f( ZF-formula) = ( St ($1,E));

        deffunc f5( Variable, set) = { v5 : for X, f st X = $2 & f = v5 holds f in X & for g st for y st (g . y) <> (f . y) holds $1 = y holds g in X };

        deffunc f4( set, set) = ($1 /\ $2);

        deffunc f3( set) = (( VAL E) \ $1);

        deffunc f2( Variable, Variable) = { v3 : for f st f = v3 holds (f . $1) in (f . $2) };

        deffunc f1( Variable, Variable) = { v3 : for f st f = v3 holds (f . $1) = (f . $2) };

        

         A1: for b st P[b] holds P[ f3(b)];

        

         A2: for X,Y be set st P[X] & P[Y] holds P[ f4(X,Y)]

        proof

          let X,Y be set;

          assume that

           A3: X is Subset of ( VAL E) and Y is Subset of ( VAL E);

          reconsider X as Subset of ( VAL E) by A3;

          (X /\ Y) c= ( VAL E);

          hence thesis;

        end;

        now

          let x, y;

          set X1 = { v1 : for f st f = v1 holds (f . x) = (f . y) };

          set X2 = { v1 : for f st f = v1 holds (f . x) in (f . y) };

          X1 c= ( VAL E)

          proof

            let a be object;

            assume a in X1;

            then ex v1 st a = v1 & for f st f = v1 holds (f . x) = (f . y);

            hence thesis;

          end;

          hence { v1 : for f st f = v1 holds (f . x) = (f . y) } is Subset of ( VAL E);

          X2 c= ( VAL E)

          proof

            let a be object;

            assume a in X2;

            then ex v1 st a = v1 & for f st f = v1 holds (f . x) in (f . y);

            hence thesis;

          end;

          hence { v1 : for f st f = v1 holds (f . x) in (f . y) } is Subset of ( VAL E);

        end;

        then

         A4: P[ f1(x,y)] & P[ f2(x,y)];

        

         A5: for a, x st P[a] holds P[ f5(x,a)]

        proof

          let a, x such that a is Subset of ( VAL E);

          set Y = { u5 : for X, f st X = a & f = u5 holds f in X & for g st for y st (g . y) <> (f . y) holds x = y holds g in X };

          Y c= ( VAL E)

          proof

            let b be object;

            assume b in Y;

            then ex v1 st b = v1 & for X, f st X = a & f = v1 holds f in X & for g st for y st (g . y) <> (f . y) holds x = y holds g in X;

            hence thesis;

          end;

          hence thesis;

        end;

        

         A6: for H, a holds a = f(H) iff ex A st (for x, y holds [(x '=' y), f1(x,y)] in A & [(x 'in' y), f2(x,y)] in A) & [H, a] in A & for H9, a st [H9, a] in A holds (H9 is being_equality implies a = f1(Var1,Var2)) & (H9 is being_membership implies a = f2(Var1,Var2)) & (H9 is negative implies ex b st a = f3(b) & [( the_argument_of H9), b] in A) & (H9 is conjunctive implies ex b, c st a = f4(b,c) & [( the_left_argument_of H9), b] in A & [( the_right_argument_of H9), c] in A) & (H9 is universal implies ex b st a = f5(bound_in,b) & [( the_scope_of H9), b] in A) by Def3;

        thus P[ f(H)] from ZFschproperty( A6, A4, A1, A2, A5);

      end;

    end

    theorem :: ZF_MODEL:2

    

     Th2: for x, y, f holds (f . x) = (f . y) iff f in ( St ((x '=' y),E))

    proof

      let x, y, f;

      

       A1: (x '=' y) is being_equality;

      then

       A2: (x '=' y) = (( Var1 (x '=' y)) '=' ( Var2 (x '=' y))) by ZF_LANG: 36;

      then

       A3: x = ( Var1 (x '=' y)) by ZF_LANG: 1;

      

       A4: y = ( Var2 (x '=' y)) by A2, ZF_LANG: 1;

      

       A5: ( St ((x '=' y),E)) = { v1 : for f st f = v1 holds (f . ( Var1 (x '=' y))) = (f . ( Var2 (x '=' y))) } by A1, Lm3;

      thus (f . x) = (f . y) implies f in ( St ((x '=' y),E))

      proof

        reconsider v = f as Element of ( VAL E) by FUNCT_2: 8;

        assume (f . x) = (f . y);

        then for f st f = v holds (f . ( Var1 (x '=' y))) = (f . ( Var2 (x '=' y))) by A2, A3, ZF_LANG: 1;

        hence thesis by A5;

      end;

      assume f in ( St ((x '=' y),E));

      then ex v1 st f = v1 & for f st f = v1 holds (f . ( Var1 (x '=' y))) = (f . ( Var2 (x '=' y))) by A5;

      hence thesis by A3, A4;

    end;

    theorem :: ZF_MODEL:3

    

     Th3: for x, y, f holds (f . x) in (f . y) iff f in ( St ((x 'in' y),E))

    proof

      let x, y, f;

      

       A1: (x 'in' y) is being_membership;

      then

       A2: (x 'in' y) = (( Var1 (x 'in' y)) 'in' ( Var2 (x 'in' y))) by ZF_LANG: 37;

      then

       A3: x = ( Var1 (x 'in' y)) by ZF_LANG: 2;

      

       A4: y = ( Var2 (x 'in' y)) by A2, ZF_LANG: 2;

      

       A5: ( St ((x 'in' y),E)) = { v1 : for f st f = v1 holds (f . ( Var1 (x 'in' y))) in (f . ( Var2 (x 'in' y))) } by A1, Lm3;

      thus (f . x) in (f . y) implies f in ( St ((x 'in' y),E))

      proof

        reconsider v = f as Element of ( VAL E) by FUNCT_2: 8;

        assume (f . x) in (f . y);

        then for f st f = v holds (f . ( Var1 (x 'in' y))) in (f . ( Var2 (x 'in' y))) by A2, A3, ZF_LANG: 2;

        hence thesis by A5;

      end;

      assume f in ( St ((x 'in' y),E));

      then ex v1 st f = v1 & for f st f = v1 holds (f . ( Var1 (x 'in' y))) in (f . ( Var2 (x 'in' y))) by A5;

      hence thesis by A3, A4;

    end;

    theorem :: ZF_MODEL:4

    

     Th4: for H, f holds not f in ( St (H,E)) iff f in ( St (( 'not' H),E))

    proof

      let H, f;

      

       A1: ( 'not' H) is negative;

      then H = ( the_argument_of ( 'not' H)) by ZF_LANG:def 30;

      then

       A2: ( St (( 'not' H),E)) = (( VAL E) \ ( St (H,E))) by A1, Lm3;

      f in ( VAL E) by FUNCT_2: 8;

      hence not f in ( St (H,E)) implies f in ( St (( 'not' H),E)) by A2, XBOOLE_0:def 5;

      assume f in ( St (( 'not' H),E));

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    theorem :: ZF_MODEL:5

    

     Th5: for H, H9, f holds f in ( St (H,E)) & f in ( St (H9,E)) iff f in ( St ((H '&' H9),E))

    proof

      let H, H9, f;

      

       A1: (H '&' H9) is conjunctive;

      then

       A2: ( St ((H '&' H9),E)) = (( St (( the_left_argument_of (H '&' H9)),E)) /\ ( St (( the_right_argument_of (H '&' H9)),E))) by Lm3;

      (H '&' H9) = (( the_left_argument_of (H '&' H9)) '&' ( the_right_argument_of (H '&' H9))) by A1, ZF_LANG: 40;

      then

       A3: H = ( the_left_argument_of (H '&' H9)) & H9 = ( the_right_argument_of (H '&' H9)) by ZF_LANG: 30;

      hence f in ( St (H,E)) & f in ( St (H9,E)) implies f in ( St ((H '&' H9),E)) by A2, XBOOLE_0:def 4;

      assume f in ( St ((H '&' H9),E));

      hence thesis by A2, A3, XBOOLE_0:def 4;

    end;

    theorem :: ZF_MODEL:6

    

     Th6: for x, H, f holds (f in ( St (H,E)) & for g st for y st (g . y) <> (f . y) holds x = y holds g in ( St (H,E))) iff f in ( St (( All (x,H)),E))

    proof

      let x, H, f;

      

       A1: ( All (x,H)) is universal;

      then

       A2: ( St (( All (x,H)),E)) = { v5 : for X, f st X = ( St (( the_scope_of ( All (x,H))),E)) & f = v5 holds f in X & for g st for y st (g . y) <> (f . y) holds ( bound_in ( All (x,H))) = y holds g in X } by Lm3;

      

       A3: ( All (x,H)) = ( All (( bound_in ( All (x,H))),( the_scope_of ( All (x,H))))) by A1, ZF_LANG: 44;

      then

       A4: x = ( bound_in ( All (x,H))) by ZF_LANG: 3;

      

       A5: H = ( the_scope_of ( All (x,H))) by A3, ZF_LANG: 3;

      thus (f in ( St (H,E)) & for g st for y st (g . y) <> (f . y) holds x = y holds g in ( St (H,E))) implies f in ( St (( All (x,H)),E))

      proof

        reconsider v = f as Element of ( VAL E) by FUNCT_2: 8;

        assume f in ( St (H,E)) & for g st for y st (g . y) <> (f . y) holds x = y holds g in ( St (H,E));

        then for X, h holds X = ( St (( the_scope_of ( All (x,H))),E)) & h = v implies h in X & for g holds (for y st (g . y) <> (h . y) holds ( bound_in ( All (x,H))) = y) implies g in X by A4, A5;

        hence thesis by A2;

      end;

      assume f in ( St (( All (x,H)),E));

      then

       A6: ex v5 st f = v5 & for X, f st X = ( St (( the_scope_of ( All (x,H))),E)) & f = v5 holds f in X & for g st for y st (g . y) <> (f . y) holds ( bound_in ( All (x,H))) = y holds g in X by A2;

      hence f in ( St (H,E)) by A5;

      let g;

      assume for y st (g . y) <> (f . y) holds x = y;

      hence thesis by A4, A5, A6;

    end;

    theorem :: ZF_MODEL:7

    H is being_equality implies for f holds (f . ( Var1 H)) = (f . ( Var2 H)) iff f in ( St (H,E))

    proof

      assume H is being_equality;

      then H = (( Var1 H) '=' ( Var2 H)) by ZF_LANG: 36;

      hence thesis by Th2;

    end;

    theorem :: ZF_MODEL:8

    H is being_membership implies for f holds (f . ( Var1 H)) in (f . ( Var2 H)) iff f in ( St (H,E))

    proof

      assume H is being_membership;

      then H = (( Var1 H) 'in' ( Var2 H)) by ZF_LANG: 37;

      hence thesis by Th3;

    end;

    theorem :: ZF_MODEL:9

    H is negative implies for f holds not f in ( St (( the_argument_of H),E)) iff f in ( St (H,E))

    proof

      assume H is negative;

      then H = ( 'not' ( the_argument_of H)) by ZF_LANG:def 30;

      hence thesis by Th4;

    end;

    theorem :: ZF_MODEL:10

    H is conjunctive implies for f holds f in ( St (( the_left_argument_of H),E)) & f in ( St (( the_right_argument_of H),E)) iff f in ( St (H,E))

    proof

      assume H is conjunctive;

      then H = (( the_left_argument_of H) '&' ( the_right_argument_of H)) by ZF_LANG: 40;

      hence thesis by Th5;

    end;

    theorem :: ZF_MODEL:11

    H is universal implies for f holds (f in ( St (( the_scope_of H),E)) & for g st for y st (g . y) <> (f . y) holds ( bound_in H) = y holds g in ( St (( the_scope_of H),E))) iff f in ( St (H,E))

    proof

      assume H is universal;

      then H = ( All (( bound_in H),( the_scope_of H))) by ZF_LANG: 44;

      hence thesis by Th6;

    end;

    definition

      let D be non empty set;

      let f be Function of VAR , D;

      let H;

      :: ZF_MODEL:def4

      pred D,f |= H means

      : Def4: f in ( St (H,D));

    end

    theorem :: ZF_MODEL:12

    for E, f, x, y holds (E,f) |= (x '=' y) iff (f . x) = (f . y) by Th2;

    theorem :: ZF_MODEL:13

    for E, f, x, y holds (E,f) |= (x 'in' y) iff (f . x) in (f . y) by Th3;

    theorem :: ZF_MODEL:14

    

     Th14: for E, f, H holds (E,f) |= H iff not (E,f) |= ( 'not' H) by Th4;

    theorem :: ZF_MODEL:15

    

     Th15: for E, f, H, H9 holds (E,f) |= (H '&' H9) iff (E,f) |= H & (E,f) |= H9 by Th5;

    theorem :: ZF_MODEL:16

    

     Th16: for E, f, H, x holds (E,f) |= ( All (x,H)) iff for g st for y st (g . y) <> (f . y) holds x = y holds (E,g) |= H

    proof

      let E, f, H, x;

      

       A1: (for g st for y st (g . y) <> (f . y) holds x = y holds (E,g) |= H) implies (E,f) |= H

      proof

        

         A2: for y st (f . y) <> (f . y) holds x = y;

        assume for g st for y st (g . y) <> (f . y) holds x = y holds (E,g) |= H;

        hence thesis by A2;

      end;

      

       A3: (for g st for y st (g . y) <> (f . y) holds x = y holds (E,g) |= H) implies for g st for y st (g . y) <> (f . y) holds x = y holds g in ( St (H,E)) by Def4;

      thus thesis by A3, A1, Th6;

    end;

    theorem :: ZF_MODEL:17

    for E, f, H, H9 holds (E,f) |= (H 'or' H9) iff (E,f) |= H or (E,f) |= H9

    proof

      let E, f, H, H9;

      (E,f) |= (( 'not' H) '&' ( 'not' H9)) iff (E,f) |= ( 'not' H) & (E,f) |= ( 'not' H9) by Th15;

      hence thesis by Th14;

    end;

    theorem :: ZF_MODEL:18

    

     Th18: for E, f, H, H9 holds (E,f) |= (H => H9) iff ((E,f) |= H implies (E,f) |= H9)

    proof

      let E, f, H, H9;

      (E,f) |= (H '&' ( 'not' H9)) iff (E,f) |= H & (E,f) |= ( 'not' H9) by Th15;

      hence thesis by Th14;

    end;

    theorem :: ZF_MODEL:19

    for E, f, H, H9 holds (E,f) |= (H <=> H9) iff ((E,f) |= H iff (E,f) |= H9)

    proof

      let E, f, H, H9;

      (E,f) |= ((H => H9) '&' (H9 => H)) iff (E,f) |= (H => H9) & (E,f) |= (H9 => H) by Th15;

      hence thesis by Th18;

    end;

    theorem :: ZF_MODEL:20

    

     Th20: for E, f, H, x holds (E,f) |= ( Ex (x,H)) iff ex g st (for y st (g . y) <> (f . y) holds x = y) & (E,g) |= H

    proof

      let E, f, H, x;

      thus (E,f) |= ( Ex (x,H)) implies ex g st (for y st (g . y) <> (f . y) holds x = y) & (E,g) |= H

      proof

        assume (E,f) |= ( Ex (x,H));

        then

        consider g such that

         A1: for y st (g . y) <> (f . y) holds x = y and

         A2: not (E,g) |= ( 'not' H) by Th14, Th16;

        thus thesis by A1, A2, Th14;

      end;

      given g such that

       A3: for y st (g . y) <> (f . y) holds x = y and

       A4: (E,g) |= H;

       not (E,g) |= ( 'not' H) by A4, Th14;

      hence thesis by Th14, A3, Th16;

    end;

    theorem :: ZF_MODEL:21

    (E,f) |= ( All (x,y,H)) iff for g st for z st (g . z) <> (f . z) holds x = z or y = z holds (E,g) |= H

    proof

      thus (E,f) |= ( All (x,y,H)) implies for g st for z st (g . z) <> (f . z) holds x = z or y = z holds (E,g) |= H

      proof

        assume

         A1: (E,f) |= ( All (x,y,H));

        

         A2: for g st for z st (g . z) <> (f . z) holds x = z holds for h st for z st (h . z) <> (g . z) holds y = z holds (E,h) |= H

        proof

          let g;

          assume for z st (g . z) <> (f . z) holds x = z;

          then (E,g) |= ( All (y,H)) by A1, Th16;

          hence thesis by Th16;

        end;

        let g such that

         A3: for z st (g . z) <> (f . z) holds x = z or y = z;

        set h = (g +* (y,(f . y)));

        for z st (h . z) <> (f . z) holds x = z

        proof

          let z such that

           A4: (h . z) <> (f . z) and

           A5: x <> z;

          

           A6: y <> z by A4, FUNCT_7: 128;

          then (g . z) = (f . z) by A3, A5;

          hence contradiction by A4, A6, FUNCT_7: 32;

        end;

        then (for z st (g . z) <> (h . z) holds y = z) implies (E,g) |= H by A2;

        hence thesis by FUNCT_7: 32;

      end;

      assume

       A7: for g st for z st (g . z) <> (f . z) holds x = z or y = z holds (E,g) |= H;

      now

        let g such that

         A8: for z st (g . z) <> (f . z) holds x = z;

        now

          let h such that

           A9: for z st (h . z) <> (g . z) holds y = z;

          now

            let z;

            assume that

             A10: (h . z) <> (f . z) & x <> z and

             A11: y <> z;

            (h . z) = (g . z) by A9, A11;

            hence contradiction by A8, A10;

          end;

          hence (E,h) |= H by A7;

        end;

        hence (E,g) |= ( All (y,H)) by Th16;

      end;

      hence thesis by Th16;

    end;

    theorem :: ZF_MODEL:22

    (E,f) |= ( Ex (x,y,H)) iff ex g st (for z st (g . z) <> (f . z) holds x = z or y = z) & (E,g) |= H

    proof

      thus (E,f) |= ( Ex (x,y,H)) implies ex g st (for z st (g . z) <> (f . z) holds x = z or y = z) & (E,g) |= H

      proof

        assume (E,f) |= ( Ex (x,y,H));

        then

        consider g such that

         A1: for z st (g . z) <> (f . z) holds x = z and

         A2: (E,g) |= ( Ex (y,H)) by Th20;

        consider h such that

         A3: for z st (h . z) <> (g . z) holds y = z and

         A4: (E,h) |= H by A2, Th20;

        take h;

        thus for z st (h . z) <> (f . z) holds x = z or y = z

        proof

          let z such that

           A5: (h . z) <> (f . z) and

           A6: x <> z and

           A7: y <> z;

          (g . z) = (f . z) by A1, A6;

          hence contradiction by A3, A5, A7;

        end;

        thus thesis by A4;

      end;

      given g such that

       A8: for z st (g . z) <> (f . z) holds x = z or y = z and

       A9: (E,g) |= H;

      set h = (f +* (x,(g . x)));

      now

        let z;

        assume that

         A10: (g . z) <> (h . z) and

         A11: y <> z;

        

         A12: x <> z by A10, FUNCT_7: 128;

        then (g . z) = (f . z) by A8, A11;

        hence contradiction by A10, A12, FUNCT_7: 32;

      end;

      then

       A13: (E,h) |= ( Ex (y,H)) by A9, Th20;

      for z st (h . z) <> (f . z) holds x = z by FUNCT_7: 32;

      hence thesis by A13, Th20;

    end;

    definition

      let E, H;

      :: ZF_MODEL:def5

      pred E |= H means for f holds (E,f) |= H;

    end

    theorem :: ZF_MODEL:23

    E |= ( All (x,H)) iff E |= H

    proof

      thus E |= ( All (x,H)) implies E |= H

      proof

        assume

         A1: for f holds (E,f) |= ( All (x,H));

        let f;

        for y st (f . y) <> (f . y) holds x = y;

        hence thesis by A1, Th16;

      end;

      assume

       A2: E |= H;

      let f;

      for g st for y st (g . y) <> (f . y) holds x = y holds (E,g) |= H by A2;

      hence thesis by Th16;

    end;

    definition

      :: ZF_MODEL:def6

      func the_axiom_of_extensionality -> ZF-formula equals ( All (( x. 0 ),( x. 1),(( All (( x. 2),((( x. 2) 'in' ( x. 0 )) <=> (( x. 2) 'in' ( x. 1))))) => (( x. 0 ) '=' ( x. 1)))));

      correctness ;

      :: ZF_MODEL:def7

      func the_axiom_of_pairs -> ZF-formula equals ( All (( x. 0 ),( x. 1),( Ex (( x. 2),( All (( x. 3),((( x. 3) 'in' ( x. 2)) <=> ((( x. 3) '=' ( x. 0 )) 'or' (( x. 3) '=' ( x. 1))))))))));

      correctness ;

      :: ZF_MODEL:def8

      func the_axiom_of_unions -> ZF-formula equals ( All (( x. 0 ),( Ex (( x. 1),( All (( x. 2),((( x. 2) 'in' ( x. 1)) <=> ( Ex (( x. 3),((( x. 2) 'in' ( x. 3)) '&' (( x. 3) 'in' ( x. 0 ))))))))))));

      correctness ;

      :: ZF_MODEL:def9

      func the_axiom_of_infinity -> ZF-formula equals ( Ex (( x. 0 ),( x. 1),((( x. 1) 'in' ( x. 0 )) '&' ( All (( x. 2),((( x. 2) 'in' ( x. 0 )) => ( Ex (( x. 3),(((( x. 3) 'in' ( x. 0 )) '&' ( 'not' (( x. 3) '=' ( x. 2)))) '&' ( All (( x. 4),((( x. 4) 'in' ( x. 2)) => (( x. 4) 'in' ( x. 3))))))))))))));

      correctness ;

      :: ZF_MODEL:def10

      func the_axiom_of_power_sets -> ZF-formula equals ( All (( x. 0 ),( Ex (( x. 1),( All (( x. 2),((( x. 2) 'in' ( x. 1)) <=> ( All (( x. 3),((( x. 3) 'in' ( x. 2)) => (( x. 3) 'in' ( x. 0 ))))))))))));

      correctness ;

    end

    definition

      let H be ZF-formula;

      :: ZF_MODEL:def11

      func the_axiom_of_substitution_for H -> ZF-formula equals (( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) => ( All (( x. 1),( Ex (( x. 2),( All (( x. 4),((( x. 4) 'in' ( x. 2)) <=> ( Ex (( x. 3),((( x. 3) 'in' ( x. 1)) '&' H)))))))))));

      correctness ;

    end

    definition

      let E;

      :: ZF_MODEL:def12

      attr E is being_a_model_of_ZF means E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & for H st {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) holds E |= ( the_axiom_of_substitution_for H);

    end