:: ZF_MODEL semantic presentation begin scheme :: ZF_MODEL:sch 1 ZFschex{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula } : ex a, A being set st ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) proof defpred S1[ set , ZF-formula, set ] means ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in \$1 & [(x 'in' y),F2(x,y)] in \$1 ) ) & [\$2,\$3] in \$1 & ( for H being ZF-formula for a being set st [H,a] in \$1 holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in \$1 ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in \$1 ) ) ) ) ); defpred S2[ ZF-formula] means ex a, A being set st S1[A,\$1,a]; A1: for H being ZF-formula st H is atomic holds S2[H] proof let H be ZF-formula; ::_thesis: ( H is atomic implies S2[H] ) assume A2: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: S2[H] then consider a being set such that A3: ( ( H is being_equality & a = F1((Var1 H),(Var2 H)) ) or ( H is being_membership & a = F2((Var1 H),(Var2 H)) ) ) ; take a ; ::_thesis: ex A being set st S1[A,H,a] take X = { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } \/ { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } ; ::_thesis: S1[X,H,a] A4: now__::_thesis:_(_H_is_being_membership_implies_[H,a]_in_X_) assume H is being_membership ; ::_thesis: [H,a] in X 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)] where x, y is Variable : x = x } by A3, ZF_LANG:18; hence [H,a] in X by XBOOLE_0:def_3; ::_thesis: verum end; thus for x, y being Variable holds ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) ::_thesis: ( [H,a] in X & ( for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) ) proof let x, y be Variable; ::_thesis: ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) [(x '=' y),F1(x,y)] in { [(z '=' t),F1(z,t)] where z, t is Variable : z = z } ; hence [(x '=' y),F1(x,y)] in X by XBOOLE_0:def_3; ::_thesis: [(x 'in' y),F2(x,y)] in X [(x 'in' y),F2(x,y)] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } ; hence [(x 'in' y),F2(x,y)] in X by XBOOLE_0:def_3; ::_thesis: verum end; now__::_thesis:_(_H_is_being_equality_implies_[H,a]_in_X_) assume H is being_equality ; ::_thesis: [H,a] in X 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)] where x, y is Variable : x = x } by A3, ZF_LANG:19; hence [H,a] in X by XBOOLE_0:def_3; ::_thesis: verum end; hence [H,a] in X by A2, A4; ::_thesis: for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) let H be ZF-formula; ::_thesis: for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) let a be set ; ::_thesis: ( [H,a] in X implies ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) A5: now__::_thesis:_(_[H,a]_in__{__[(z_'in'_t),F2(z,t)]_where_z,_t_is_Variable_:_z_=_z__}__implies_H_._1_=_1_) assume [H,a] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } ; ::_thesis: H . 1 = 1 then consider x, y being Variable 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; ::_thesis: verum end; assume A7: [H,a] in X ; ::_thesis: ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) then A8: ( [H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } or [H,a] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } ) by XBOOLE_0:def_3; thus ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) ::_thesis: ( ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) proof assume A9: H is being_equality ; ::_thesis: a = F1((Var1 H),(Var2 H)) then A10: H = (Var1 H) '=' (Var2 H) by ZF_LANG:36; A11: H . 1 = 0 by A9, ZF_LANG:18; for x, y being Variable holds [H,a] <> [(x 'in' y),F2(x,y)] proof let x, y be Variable; ::_thesis: [H,a] <> [(x 'in' y),F2(x,y)] H <> x 'in' y by A11, ZF_LANG:15; hence [H,a] <> [(x 'in' y),F2(x,y)] by XTUPLE_0:1; ::_thesis: verum end; then for x, y being Variable holds ( not [H,a] = [(x 'in' y),F2(x,y)] or not x = x ) ; then consider x, y being Variable 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 a = F1((Var1 H),(Var2 H)) by A12, XTUPLE_0:1; ::_thesis: verum end; thus ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) ::_thesis: ( ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) proof assume A13: H is being_membership ; ::_thesis: a = F2((Var1 H),(Var2 H)) then A14: H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37; A15: H . 1 = 1 by A13, ZF_LANG:19; for x, y being Variable holds [H,a] <> [(x '=' y),F1(x,y)] proof let x, y be Variable; ::_thesis: [H,a] <> [(x '=' y),F1(x,y)] H <> x '=' y by A15, ZF_LANG:15; hence [H,a] <> [(x '=' y),F1(x,y)] by XTUPLE_0:1; ::_thesis: verum end; then for x, y being Variable holds ( not [H,a] = [(x '=' y),F1(x,y)] or not x = x ) ; then consider x, y being Variable 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 a = F2((Var1 H),(Var2 H)) by A16, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_(_[H,a]_in__{__[(x_'='_y),F1(x,y)]_where_x,_y_is_Variable_:_x_=_x__}__implies_H_._1_=_0_) assume [H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } ; ::_thesis: H . 1 = 0 then consider x, y being Variable 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; ::_thesis: verum end; hence ( ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) by A7, A5, XBOOLE_0:def_3, ZF_LANG:20, ZF_LANG:21, ZF_LANG:22; ::_thesis: verum end; A18: for H being ZF-formula st H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] holds S2[H] proof let H be ZF-formula; ::_thesis: ( H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] implies S2[H] ) assume H is conjunctive ; ::_thesis: ( not S2[ the_left_argument_of H] or not S2[ the_right_argument_of H] or S2[H] ) then A19: H . 1 = 3 by ZF_LANG:21; given a1, A1 being set such that A20: S1[A1, the_left_argument_of H,a1] ; ::_thesis: ( not S2[ the_right_argument_of H] or S2[H] ) given a2, A2 being set such that A21: S1[A2, the_right_argument_of H,a2] ; ::_thesis: S2[H] take a = F4(a1,a2); ::_thesis: ex A being set st S1[A,H,a] take X = (A1 \/ A2) \/ {[H,a]}; ::_thesis: S1[X,H,a] thus for x, y being Variable holds ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) ::_thesis: ( [H,a] in X & ( for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) ) proof let x, y be Variable; ::_thesis: ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) [(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 ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) by A22, XBOOLE_0:def_3; ::_thesis: verum end; [H,a] in {[H,a]} by TARSKI:def_1; hence [H,a] in X by XBOOLE_0:def_3; ::_thesis: for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) let F be ZF-formula; ::_thesis: for a being set st [F,a] in X holds ( ( F is being_equality implies a = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies a = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( a = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( a = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) let c be set ; ::_thesis: ( [F,c] in X implies ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) ) A23: ( [F,c] = [H,a] implies ( F = H & c = a ) ) by XTUPLE_0:1; assume [F,c] in X ; ::_thesis: ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] 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 F),(Var2 F)) ) by A20, A21, A23, A19, ZF_LANG:18; ::_thesis: ( ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) not H is being_membership by A19, ZF_LANG:19; hence ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) by A20, A21, A25, XTUPLE_0:1; ::_thesis: ( ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) thus ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) ::_thesis: ( ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) proof assume A26: F is negative ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) A27: now__::_thesis:_(_[F,c]_in_A2_implies_ex_b_being_set_st_ (_c_=_F3(b)_&_[(the_argument_of_F),b]_in_X_)_) assume [F,c] in A2 ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) then consider b being set 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 ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A28; ::_thesis: verum end; now__::_thesis:_(_[F,c]_in_A1_implies_ex_b_being_set_st_ (_c_=_F3(b)_&_[(the_argument_of_F),b]_in_X_)_) assume [F,c] in A1 ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) then consider b being set 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 ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A30; ::_thesis: verum end; hence ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A24, A23, A19, A26, A27, TARSKI:def_1, XBOOLE_0:def_3, ZF_LANG:20; ::_thesis: verum end; thus ( F is conjunctive implies ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) ) ::_thesis: ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) proof assume A32: F is conjunctive ; ::_thesis: ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) A33: now__::_thesis:_(_[F,c]_in_A1_implies_ex_b,_d_being_set_st_ (_c_=_F4(b,d)_&_[(the_left_argument_of_F),b]_in_X_&_[(the_right_argument_of_F),d]_in_X_)_) assume [F,c] in A1 ; ::_thesis: ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) then consider b, d being set 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 ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) by A34, A37; ::_thesis: verum end; A38: now__::_thesis:_(_[F,c]_in_A2_implies_ex_b,_d_being_set_st_ (_c_=_F4(b,d)_&_[(the_left_argument_of_F),b]_in_X_&_[(the_right_argument_of_F),d]_in_X_)_) assume [F,c] in A2 ; ::_thesis: ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) then consider b, d being set 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 ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) by A39, A42; ::_thesis: verum end; now__::_thesis:_(_[F,c]_=_[H,a]_implies_ex_b,_d_being_set_st_ (_c_=_F4(b,d)_&_[(the_left_argument_of_F),b]_in_X_&_[(the_right_argument_of_F),d]_in_X_)_) assume A43: [F,c] = [H,a] ; ::_thesis: ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) 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 ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) by A23, A43, A44; ::_thesis: verum end; hence ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) by A24, A33, A38, TARSKI:def_1, XBOOLE_0:def_3; ::_thesis: verum end; thus ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ::_thesis: verum proof assume A45: F is universal ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) A46: now__::_thesis:_(_[F,c]_in_A2_implies_ex_b_being_set_st_ (_c_=_F5((bound_in_F),b)_&_[(the_scope_of_F),b]_in_X_)_) assume [F,c] in A2 ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) then consider b being set such that A47: c = F5((bound_in F),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 ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A47; ::_thesis: verum end; now__::_thesis:_(_[F,c]_in_A1_implies_ex_b_being_set_st_ (_c_=_F5((bound_in_F),b)_&_[(the_scope_of_F),b]_in_X_)_) assume [F,c] in A1 ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) then consider b being set such that A49: c = F5((bound_in F),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 ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A49; ::_thesis: verum end; hence ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A24, A23, A19, A45, A46, TARSKI:def_1, XBOOLE_0:def_3, ZF_LANG:22; ::_thesis: verum end; end; A51: for H being ZF-formula st H is universal & S2[ the_scope_of H] holds S2[H] proof let H be ZF-formula; ::_thesis: ( H is universal & S2[ the_scope_of H] implies S2[H] ) assume H is universal ; ::_thesis: ( not S2[ the_scope_of H] or S2[H] ) then A52: H . 1 = 4 by ZF_LANG:22; given a, A being set such that A53: S1[A, the_scope_of H,a] ; ::_thesis: S2[H] take b = F5((bound_in H),a); ::_thesis: ex A being set st S1[A,H,b] take X = A \/ {[H,b]}; ::_thesis: S1[X,H,b] thus for x, y being Variable holds ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) ::_thesis: ( [H,b] in X & ( for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) ) proof let x, y be Variable; ::_thesis: ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) by A53; hence ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) by XBOOLE_0:def_3; ::_thesis: verum end; [H,b] in {[H,b]} by TARSKI:def_1; hence [H,b] in X by XBOOLE_0:def_3; ::_thesis: for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) let F be ZF-formula; ::_thesis: for a being set st [F,a] in X holds ( ( F is being_equality implies a = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies a = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( a = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( a = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) let c be set ; ::_thesis: ( [F,c] in X implies ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) ) A54: ( [F,c] = [H,b] implies ( F = H & c = b ) ) by XTUPLE_0:1; assume [F,c] in X ; ::_thesis: ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] 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 F),(Var2 F)) ) by A53, A54, A52, TARSKI:def_1, ZF_LANG:18; ::_thesis: ( ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) thus ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) by A53, A55, A54, A52, TARSKI:def_1, ZF_LANG:19; ::_thesis: ( ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) thus ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) ::_thesis: ( ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) proof assume F is negative ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) then consider b being set 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 ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A56; ::_thesis: verum end; thus ( F is conjunctive implies ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) ) ::_thesis: ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) proof assume F is conjunctive ; ::_thesis: ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) then consider b, d being set 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 ; ::_thesis: ex d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) take d ; ::_thesis: ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) thus ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) by A58, XBOOLE_0:def_3; ::_thesis: verum end; thus ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ::_thesis: verum proof assume A59: F is universal ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) A60: now__::_thesis:_(_[F,c]_in_A_implies_ex_b_being_set_st_ (_c_=_F5((bound_in_F),b)_&_[(the_scope_of_F),b]_in_X_)_) assume [F,c] in A ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) then consider b being set such that A61: c = F5((bound_in F),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 ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A61; ::_thesis: verum end; now__::_thesis:_(_[F,c]_=_[H,b]_implies_ex_b_being_set_st_ (_c_=_F5((bound_in_F),b)_&_[(the_scope_of_F),b]_in_X_)_) assume A63: [F,c] = [H,b] ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) then [(the_scope_of F),a] in X by A53, A54, XBOOLE_0:def_3; hence ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A54, A63; ::_thesis: verum end; hence ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A55, A60, TARSKI:def_1; ::_thesis: verum end; end; A64: for H being ZF-formula st H is negative & S2[ the_argument_of H] holds S2[H] proof let H be ZF-formula; ::_thesis: ( H is negative & S2[ the_argument_of H] implies S2[H] ) assume H is negative ; ::_thesis: ( not S2[ the_argument_of H] or S2[H] ) then A65: H . 1 = 2 by ZF_LANG:20; given a, A being set such that A66: S1[A, the_argument_of H,a] ; ::_thesis: S2[H] take b = F3(a); ::_thesis: ex A being set st S1[A,H,b] take X = A \/ {[H,b]}; ::_thesis: S1[X,H,b] thus for x, y being Variable holds ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) ::_thesis: ( [H,b] in X & ( for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) ) proof let x, y be Variable; ::_thesis: ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) by A66; hence ( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) by XBOOLE_0:def_3; ::_thesis: verum end; [H,b] in {[H,b]} by TARSKI:def_1; hence [H,b] in X by XBOOLE_0:def_3; ::_thesis: for H being ZF-formula for a being set st [H,a] in X holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in X ) ) & ( H is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) let F be ZF-formula; ::_thesis: for a being set st [F,a] in X holds ( ( F is being_equality implies a = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies a = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( a = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( a = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( a = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) let c be set ; ::_thesis: ( [F,c] in X implies ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) ) A67: ( [F,c] = [H,b] implies ( F = H & c = b ) ) by XTUPLE_0:1; assume [F,c] in X ; ::_thesis: ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] 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 F),(Var2 F)) ) by A66, A67, A65, TARSKI:def_1, ZF_LANG:18; ::_thesis: ( ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) thus ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) by A66, A68, A67, A65, TARSKI:def_1, ZF_LANG:19; ::_thesis: ( ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) thus ( F is negative implies ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) ) ::_thesis: ( ( F is conjunctive implies ex b, c being set st ( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) proof assume A69: F is negative ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) A70: now__::_thesis:_(_[F,c]_in_A_implies_ex_b_being_set_st_ (_c_=_F3(b)_&_[(the_argument_of_F),b]_in_X_)_) assume [F,c] in A ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) then consider d being set 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 ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A71; ::_thesis: verum end; now__::_thesis:_(_[F,c]_=_[H,b]_implies_ex_b_being_set_st_ (_c_=_F3(b)_&_[(the_argument_of_F),b]_in_X_)_) assume A73: [F,c] = [H,b] ; ::_thesis: ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) then [(the_argument_of F),a] in X by A66, A67, XBOOLE_0:def_3; hence ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A67, A73; ::_thesis: verum end; hence ex b being set st ( c = F3(b) & [(the_argument_of F),b] in X ) by A68, A70, TARSKI:def_1; ::_thesis: verum end; thus ( F is conjunctive implies ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) ) ::_thesis: ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) proof assume F is conjunctive ; ::_thesis: ex b, d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) then consider b, d being set 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 ; ::_thesis: ex d being set st ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) take d ; ::_thesis: ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) thus ( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) by A74, XBOOLE_0:def_3; ::_thesis: verum end; thus ( F is universal implies ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ::_thesis: verum proof assume F is universal ; ::_thesis: ex b being set st ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) then consider b being set such that A75: ( c = F5((bound_in F),b) & [(the_scope_of F),b] in A ) by A66, A68, A67, A65, TARSKI:def_1, ZF_LANG:22; take b ; ::_thesis: ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) thus ( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A75, XBOOLE_0:def_3; ::_thesis: verum end; end; for H being ZF-formula holds S2[H] from ZF_LANG:sch_1(A1, A64, A18, A51); hence ex a, A being set st ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) ; ::_thesis: verum end; scheme :: ZF_MODEL:sch 2 ZFschuniq{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula, F7() -> set , F8() -> set } : F7() = F8() provided A1: ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),F7()] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) and A2: ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),F8()] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) proof consider A1 being set such that for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A1 & [(x 'in' y),F2(x,y)] in A1 ) and A3: [F6(),F7()] in A1 and A4: for H being ZF-formula for a being set st [H,a] in A1 holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A1 ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A1 ) ) ) by A1; consider A2 being set such that for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A2 & [(x 'in' y),F2(x,y)] in A2 ) and A5: [F6(),F8()] in A2 and A6: for H being ZF-formula for a being set st [H,a] in A2 holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A2 ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A2 ) ) ) by A2; defpred S1[ ZF-formula] means for a, b being set st [\$1,a] in A1 & [\$1,b] in A2 holds a = b; A7: for H being ZF-formula st H is universal & S1[ the_scope_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is universal & S1[ the_scope_of H] implies S1[H] ) assume that A8: H is universal and A9: for a, b being set st [(the_scope_of H),a] in A1 & [(the_scope_of H),b] in A2 holds a = b ; ::_thesis: S1[H] let a, b be set ; ::_thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b ) assume ( [H,a] in A1 & [H,b] in A2 ) ; ::_thesis: a = b then ( ex a1 being set st ( a = F5((bound_in H),a1) & [(the_scope_of H),a1] in A1 ) & ex b1 being set st ( b = F5((bound_in H),b1) & [(the_scope_of H),b1] in A2 ) ) by A4, A6, A8; hence a = b by A9; ::_thesis: verum end; A10: for H being ZF-formula st H is atomic holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is atomic implies S1[H] ) assume A11: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: S1[H] let a, b be set ; ::_thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b ) assume that A12: [H,a] in A1 and A13: [H,b] in A2 ; ::_thesis: a = b A14: now__::_thesis:_(_H_is_being_membership_implies_a_=_b_) assume A15: H is being_membership ; ::_thesis: a = b then a = F2((Var1 H),(Var2 H)) by A4, A12; hence a = b by A6, A13, A15; ::_thesis: verum end; now__::_thesis:_(_H_is_being_equality_implies_a_=_b_) assume A16: H is being_equality ; ::_thesis: a = b then a = F1((Var1 H),(Var2 H)) by A4, A12; hence a = b by A6, A13, A16; ::_thesis: verum end; hence a = b by A11, A14; ::_thesis: verum end; A17: for H being ZF-formula st H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] ) assume that A18: H is conjunctive and A19: for a, b being set 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 being set st [(the_right_argument_of H),a] in A1 & [(the_right_argument_of H),b] in A2 holds a = b ; ::_thesis: S1[H] let a, b be set ; ::_thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b ) assume that A21: [H,a] in A1 and A22: [H,b] in A2 ; ::_thesis: a = b consider a1, a2 being 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 being 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 a = b by A20, A23, A25, A26, A28; ::_thesis: verum end; A29: for H being ZF-formula st H is negative & S1[ the_argument_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is negative & S1[ the_argument_of H] implies S1[H] ) assume that A30: H is negative and A31: for a, b being set st [(the_argument_of H),a] in A1 & [(the_argument_of H),b] in A2 holds a = b ; ::_thesis: S1[H] let a, b be set ; ::_thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b ) assume ( [H,a] in A1 & [H,b] in A2 ) ; ::_thesis: a = b then ( ex a1 being set st ( a = F3(a1) & [(the_argument_of H),a1] in A1 ) & ex b1 being set st ( b = F3(b1) & [(the_argument_of H),b1] in A2 ) ) by A4, A6, A30; hence a = b by A31; ::_thesis: verum end; for H being ZF-formula holds S1[H] from ZF_LANG:sch_1(A10, A29, A17, A7); hence F7() = F8() by A3, A5; ::_thesis: verum end; scheme :: ZF_MODEL:sch 3 ZFschresult{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula, F7( ZF-formula) -> set } : ( ( F6() is being_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) ) & ( F6() is being_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) & ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) ) provided A1: for H9 being ZF-formula for a being set holds ( a = F7(H9) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) ) proof consider A being set such that A2: for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) and A3: [F6(),F7(F6())] in A and A4: for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) by A1; thus ( F6() is being_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) ) by A3, A4; ::_thesis: ( ( F6() is being_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) & ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) ) thus ( F6() is being_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) by A3, A4; ::_thesis: ( ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) ) thus ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) ::_thesis: ( ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) ) proof assume F6() is negative ; ::_thesis: F7(F6()) = F3(F7((the_argument_of F6()))) then ex b being set st ( F7(F6()) = F3(b) & [(the_argument_of F6()),b] in A ) by A3, A4; hence F7(F6()) = F3(F7((the_argument_of F6()))) by A1, A2, A4; ::_thesis: verum end; thus ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds F7(F6()) = F4(a,b) ) ::_thesis: ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) proof assume F6() is conjunctive ; ::_thesis: for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds F7(F6()) = F4(a,b) then consider b, c being set such that A5: F7(F6()) = F4(b,c) and A6: [(the_left_argument_of F6()),b] in A and A7: [(the_right_argument_of F6()),c] in A by A3, A4; A8: F7((the_left_argument_of F6())) = b by A1, A2, A4, A6; let a1, a2 be set ; ::_thesis: ( a1 = F7((the_left_argument_of F6())) & a2 = F7((the_right_argument_of F6())) implies F7(F6()) = F4(a1,a2) ) assume ( a1 = F7((the_left_argument_of F6())) & a2 = F7((the_right_argument_of F6())) ) ; ::_thesis: F7(F6()) = F4(a1,a2) hence F7(F6()) = F4(a1,a2) by A1, A2, A4, A5, A7, A8; ::_thesis: verum end; thus ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) ::_thesis: verum proof assume F6() is universal ; ::_thesis: F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) then ex b being set st ( F7(F6()) = F5((bound_in F6()),b) & [(the_scope_of F6()),b] in A ) by A3, A4; hence F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) by A1, A2, A4; ::_thesis: verum end; end; scheme :: ZF_MODEL:sch 4 ZFschproperty{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6( ZF-formula) -> set , F7() -> ZF-formula, P1[ set ] } : P1[F6(F7())] provided A1: for H9 being ZF-formula for a being set holds ( a = F6(H9) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st ( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set 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 being set st ( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) ) and A2: for x, y being Variable holds ( P1[F1(x,y)] & P1[F2(x,y)] ) and A3: for a being set st P1[a] holds P1[F3(a)] and A4: for a, b being set st P1[a] & P1[b] holds P1[F4(a,b)] and A5: for a being set for x being Variable st P1[a] holds P1[F5(x,a)] proof defpred S1[ ZF-formula] means P1[F6(\$1)]; deffunc H1( ZF-formula) -> set = F6(\$1); deffunc H2( Variable, set ) -> set = F5(\$1,\$2); deffunc H3( set , set ) -> set = F4(\$1,\$2); deffunc H4( set ) -> set = F3(\$1); deffunc H5( Variable, Variable) -> set = F2(\$1,\$2); deffunc H6( Variable, Variable) -> set = F1(\$1,\$2); A6: for H9 being ZF-formula for a being set holds ( a = H1(H9) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H6(x,y)] in A & [(x 'in' y),H5(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = H6( Var1 H, Var2 H) ) & ( H is being_membership implies a = H5( Var1 H, Var2 H) ) & ( H is negative implies ex b being set st ( a = H4(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st ( a = H3(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st ( a = H2( bound_in H,b) & [(the_scope_of H),b] in A ) ) ) ) ) ) by A1; A7: now__::_thesis:_for_H_being_ZF-formula_holds_ (_(_H_is_being_equality_implies_H1(H)_=_H6(_Var1_H,_Var2_H)_)_&_(_H_is_being_membership_implies_H1(H)_=_H5(_Var1_H,_Var2_H)_)_&_(_H_is_negative_implies_H1(H)_=_H4(H1(_the_argument_of_H))_)_&_(_H_is_conjunctive_implies_for_a,_b_being_set_st_a_=_H1(_the_left_argument_of_H)_&_b_=_H1(_the_right_argument_of_H)_holds_ H1(H)_=_H3(a,b)_)_&_(_H_is_universal_implies_H1(H)_=_H2(_bound_in_H,H1(_the_scope_of_H))_)_) let H be ZF-formula; ::_thesis: ( ( H is being_equality implies H1(H) = H6( Var1 H, Var2 H) ) & ( H is being_membership implies H1(H) = H5( Var1 H, Var2 H) ) & ( H is negative implies H1(H) = H4(H1( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H1( the_left_argument_of H) & b = H1( the_right_argument_of H) holds H1(H) = H3(a,b) ) & ( H is universal implies H1(H) = H2( bound_in H,H1( the_scope_of H)) ) ) thus ( ( H is being_equality implies H1(H) = H6( Var1 H, Var2 H) ) & ( H is being_membership implies H1(H) = H5( Var1 H, Var2 H) ) & ( H is negative implies H1(H) = H4(H1( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H1( the_left_argument_of H) & b = H1( the_right_argument_of H) holds H1(H) = H3(a,b) ) & ( H is universal implies H1(H) = H2( bound_in H,H1( the_scope_of H)) ) ) from ZF_MODEL:sch_3(A6); ::_thesis: verum end; A8: for H being ZF-formula st H is negative & S1[ the_argument_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is negative & S1[ the_argument_of H] implies S1[H] ) assume H is negative ; ::_thesis: ( not S1[ the_argument_of H] or S1[H] ) then F6(H) = F3(F6((the_argument_of H))) by A7; hence ( not S1[ the_argument_of H] or S1[H] ) by A3; ::_thesis: verum end; A9: for H being ZF-formula st H is universal & S1[ the_scope_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is universal & S1[ the_scope_of H] implies S1[H] ) assume H is universal ; ::_thesis: ( not S1[ the_scope_of H] or S1[H] ) then F6(H) = F5((bound_in H),F6((the_scope_of H))) by A7; hence ( not S1[ the_scope_of H] or S1[H] ) by A5; ::_thesis: verum end; A10: for H being ZF-formula st H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[H] ) assume H is conjunctive ; ::_thesis: ( not S1[ the_left_argument_of H] or not S1[ the_right_argument_of H] or S1[H] ) then F6(H) = F4(F6((the_left_argument_of H)),F6((the_right_argument_of H))) by A7; hence ( not S1[ the_left_argument_of H] or not S1[ the_right_argument_of H] or S1[H] ) by A4; ::_thesis: verum end; A11: for H being ZF-formula st H is atomic holds S1[H] proof let H be ZF-formula; ::_thesis: ( H is atomic implies S1[H] ) assume ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: S1[H] then ( F6(H) = F1((Var1 H),(Var2 H)) or F6(H) = F2((Var1 H),(Var2 H)) ) by A7; hence S1[H] by A2; ::_thesis: verum end; for H being ZF-formula holds S1[H] from ZF_LANG:sch_1(A11, A8, A10, A9); hence P1[F6(F7())] ; ::_thesis: verum end; deffunc H1( Variable, Variable) -> set = {\$1,\$2}; deffunc H2( Variable, Variable) -> set = {\$1,\$2}; deffunc H3( set ) -> set = \$1; deffunc H4( set , set ) -> set = union {\$1,\$2}; deffunc H5( Variable, set ) -> Element of K27((union {\$2})) = (union {\$2}) \ {\$1}; definition let H be ZF-formula; func Free H -> set means :Def1: :: ZF_MODEL:def 1 ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,it] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ); existence ex b1, A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b1] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) proof thus ex a, A being set st ( ( for x, y being Variable holds ( [(x '=' y),H1(x,y)] in A & [(x 'in' y),H2(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H1( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H2( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H3(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H4(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H5( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) from ZF_MODEL:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b1] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b2] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) holds b1 = b2 proof let a1, a2 be set ; ::_thesis: ( ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,a1] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,a2] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) implies a1 = a2 ) assume that A1: ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H1(x,y)] in A & [(x 'in' y),H2(x,y)] in A ) ) & [H,a1] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H1( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H2( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H3(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H4(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H5( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) and A2: ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H1(x,y)] in A & [(x 'in' y),H2(x,y)] in A ) ) & [H,a2] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H1( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H2( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H3(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H4(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H5( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ; ::_thesis: a1 = a2 thus a1 = a2 from ZF_MODEL:sch_2(A1, A2); ::_thesis: verum end; end; :: deftheorem Def1 defines Free ZF_MODEL:def_1_:_ for H being ZF-formula for b2 being set holds ( b2 = Free H iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b2] in A & ( for H9 being ZF-formula for a being set 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 being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set 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 being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) ); deffunc H6( ZF-formula) -> set = Free \$1; Lm1: for H being ZF-formula for a1 being set holds ( a1 = H6(H) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H1(x,y)] in A & [(x 'in' y),H2(x,y)] in A ) ) & [H,a1] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H1( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H2( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H3(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H4(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H5( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def1; Lm2: now__::_thesis:_for_H_being_ZF-formula_holds_ (_(_H_is_being_equality_implies_H6(H)_=_H1(_Var1_H,_Var2_H)_)_&_(_H_is_being_membership_implies_H6(H)_=_H2(_Var1_H,_Var2_H)_)_&_(_H_is_negative_implies_H6(H)_=_H3(H6(_the_argument_of_H))_)_&_(_H_is_conjunctive_implies_for_a,_b_being_set_st_a_=_H6(_the_left_argument_of_H)_&_b_=_H6(_the_right_argument_of_H)_holds_ H6(H)_=_H4(a,b)_)_&_(_H_is_universal_implies_H6(H)_=_H5(_bound_in_H,H6(_the_scope_of_H))_)_) let H be ZF-formula; ::_thesis: ( ( H is being_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is being_membership implies H6(H) = H2( Var1 H, Var2 H) ) & ( H is negative implies H6(H) = H3(H6( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H6( the_left_argument_of H) & b = H6( the_right_argument_of H) holds H6(H) = H4(a,b) ) & ( H is universal implies H6(H) = H5( bound_in H,H6( the_scope_of H)) ) ) thus ( ( H is being_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is being_membership implies H6(H) = H2( Var1 H, Var2 H) ) & ( H is negative implies H6(H) = H3(H6( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H6( the_left_argument_of H) & b = H6( the_right_argument_of H) holds H6(H) = H4(a,b) ) & ( H is universal implies H6(H) = H5( bound_in H,H6( the_scope_of H)) ) ) from ZF_MODEL:sch_3(Lm1); ::_thesis: verum end; definition let H be ZF-formula; :: original: Free redefine func Free H -> Subset of VAR; coherence Free H is Subset of VAR proof defpred S1[ set ] means \$1 is Subset of VAR; A1: for x, y being Variable holds ( S1[H1(x,y)] & S1[H2(x,y)] ) proof let x, y be Variable; ::_thesis: ( S1[H1(x,y)] & S1[H2(x,y)] ) {x,y} c= VAR proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in VAR ) assume a in {x,y} ; ::_thesis: a in VAR then ( a = x or a = y ) by TARSKI:def_2; hence a in VAR ; ::_thesis: verum end; hence ( S1[H1(x,y)] & S1[H2(x,y)] ) ; ::_thesis: verum end; A2: for a, b being set st S1[a] & S1[b] holds S1[H4(a,b)] proof let a, b be set ; ::_thesis: ( S1[a] & S1[b] implies S1[H4(a,b)] ) assume A3: ( a is Subset of VAR & b is Subset of VAR ) ; ::_thesis: S1[H4(a,b)] union {a,b} c= VAR proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in union {a,b} or c in VAR ) assume c in union {a,b} ; ::_thesis: c in VAR then consider X being set 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 c in VAR by A4; ::_thesis: verum end; hence S1[H4(a,b)] ; ::_thesis: verum end; A6: for a being set for x being Variable st S1[a] holds S1[H5(x,a)] proof let a be set ; ::_thesis: for x being Variable st S1[a] holds S1[H5(x,a)] let x be Variable; ::_thesis: ( S1[a] implies S1[H5(x,a)] ) assume A7: a is Subset of VAR ; ::_thesis: S1[H5(x,a)] (union {a}) \ {x} c= VAR proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (union {a}) \ {x} or b in VAR ) assume b in (union {a}) \ {x} ; ::_thesis: b in VAR then consider X being set such that A8: b in X and A9: X in {a} by TARSKI:def_4; X = a by A9, TARSKI:def_1; hence b in VAR by A7, A8; ::_thesis: verum end; hence S1[H5(x,a)] ; ::_thesis: verum end; A10: for a being set st S1[a] holds S1[H3(a)] ; thus S1[H6(H)] from ZF_MODEL:sch_4(Lm1, A1, A10, A2, A6); ::_thesis: verum end; end; theorem :: ZF_MODEL:1 for H being ZF-formula 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 be ZF-formula; ::_thesis: ( ( 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)} ) ) 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; ::_thesis: ( ( 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)} ) ) thus ( H is conjunctive implies Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) ) ::_thesis: ( H is universal implies Free H = (Free (the_scope_of H)) \ {(bound_in H)} ) proof assume H is conjunctive ; ::_thesis: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) 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 ; ::_thesis: verum end; assume H is universal ; ::_thesis: Free H = (Free (the_scope_of H)) \ {(bound_in H)} then Free H = (union {(Free (the_scope_of H))}) \ {(bound_in H)} by Lm2; hence Free H = (Free (the_scope_of H)) \ {(bound_in H)} by ZFMISC_1:25; ::_thesis: verum end; definition let D be non empty set ; func VAL D -> set equals :: ZF_MODEL:def 2 Funcs (VAR,D); coherence Funcs (VAR,D) is set ; end; :: deftheorem defines VAL ZF_MODEL:def_2_:_ for D being non empty set holds VAL D = Funcs (VAR,D); registration let D be non empty set ; cluster VAL D -> non empty ; coherence not VAL D is empty ; end; definition deffunc H7( set , set ) -> set = (union {\$1}) /\ (union {\$2}); let H be ZF-formula; let E be non empty set ; deffunc H8( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . \$1 = f . \$2 } ; deffunc H9( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . \$1 in f . \$2 } ; deffunc H10( set ) -> Element of K27((VAL E)) = (VAL E) \ (union {\$1}); deffunc H11( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = \$2 & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds \$1 = y ) holds g in X ) ) } ; func St (H,E) -> set means :Def3: :: ZF_MODEL:def 3 ex A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,it] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ); existence ex b1, A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,b1] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) proof thus ex a, A being set st ( ( for x, y being Variable holds ( [(x '=' y),H8(x,y)] in A & [(x 'in' y),H9(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H8( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H9( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H10(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H7(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H11( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) from ZF_MODEL:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ex A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,b1] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,b2] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) holds b1 = b2 proof let a1, a2 be set ; ::_thesis: ( ex A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,a1] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,a2] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) implies a1 = a2 ) assume that A1: ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H8(x,y)] in A & [(x 'in' y),H9(x,y)] in A ) ) & [H,a1] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H8( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H9( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H10(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H7(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H11( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) and A2: ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H8(x,y)] in A & [(x 'in' y),H9(x,y)] in A ) ) & [H,a2] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H8( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H9( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H10(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H7(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H11( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ; ::_thesis: a1 = a2 thus a1 = a2 from ZF_MODEL:sch_2(A1, A2); ::_thesis: verum end; end; :: deftheorem Def3 defines St ZF_MODEL:def_3_:_ for H being ZF-formula for E being non empty set for b3 being set holds ( b3 = St (H,E) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds f . x in f . y } ] in A ) ) & [H,b3] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = b & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds bound_in H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) ); Lm3: now__::_thesis:_for_H_being_ZF-formula for_E_being_non_empty_set_holds_ (_(_H_is_being_equality_implies_H12(H)_=_H8(_Var1_H,_Var2_H)_)_&_(_H_is_being_membership_implies_H12(H)_=_H9(_Var1_H,_Var2_H)_)_&_(_H_is_negative_implies_H12(H)_=_H10(H12(_the_argument_of_H))_)_&_(_H_is_conjunctive_implies_for_a,_b_being_set_st_a_=_H12(_the_left_argument_of_H)_&_b_=_H12(_the_right_argument_of_H)_holds_ H12(H)_=_H7(a,b)_)_&_(_H_is_universal_implies_H12(H)_=_H11(_bound_in_H,H12(_the_scope_of_H))_)_) deffunc H7( set , set ) -> set = (union {\$1}) /\ (union {\$2}); let H be ZF-formula; ::_thesis: for E being non empty set holds ( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds H12(H) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) ) let E be non empty set ; ::_thesis: ( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds H12(H) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) ) deffunc H8( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . \$1 = f . \$2 } ; deffunc H9( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . \$1 in f . \$2 } ; deffunc H10( set ) -> Element of K27((VAL E)) = (VAL E) \ (union {\$1}); deffunc H11( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = \$2 & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds \$1 = y ) holds g in X ) ) } ; deffunc H12( ZF-formula) -> set = St (\$1,E); A1: for H being ZF-formula for a being set holds ( a = H12(H) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H8(x,y)] in A & [(x 'in' y),H9(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H8( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H9( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H10(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H7(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H11( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def3; thus ( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds H12(H) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) ) from ZF_MODEL:sch_3(A1); ::_thesis: verum end; definition let H be ZF-formula; let E be non empty set ; :: original: St redefine func St (H,E) -> Subset of (VAL E); coherence St (H,E) is Subset of (VAL E) proof defpred S1[ set ] means \$1 is Subset of (VAL E); deffunc H7( ZF-formula) -> set = St (\$1,E); deffunc H8( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = \$2 & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds \$1 = y ) holds g in X ) ) } ; deffunc H9( set , set ) -> set = (union {\$1}) /\ (union {\$2}); deffunc H10( set ) -> Element of K27((VAL E)) = (VAL E) \ (union {\$1}); deffunc H11( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . \$1 in f . \$2 } ; deffunc H12( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . \$1 = f . \$2 } ; A1: for b being set st S1[b] holds S1[H10(b)] ; A2: for X, Y being set st S1[X] & S1[Y] holds S1[H9(X,Y)] proof let X, Y be set ; ::_thesis: ( S1[X] & S1[Y] implies S1[H9(X,Y)] ) assume that A3: X is Subset of (VAL E) and Y is Subset of (VAL E) ; ::_thesis: S1[H9(X,Y)] reconsider X = X as Subset of (VAL E) by A3; A4: union {X} = X by ZFMISC_1:25; (union {X}) /\ (union {Y}) c= VAL E proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union {X}) /\ (union {Y}) or a in VAL E ) assume a in (union {X}) /\ (union {Y}) ; ::_thesis: a in VAL E then a in X by A4, XBOOLE_0:def_4; hence a in VAL E ; ::_thesis: verum end; hence S1[H9(X,Y)] ; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Variable_holds_ (__{__v1_where_v1_is_Element_of_VAL_E_:_for_f_being_Function_of_VAR,E_st_f_=_v1_holds_ f_._x_=_f_._y__}__is_Subset_of_(VAL_E)_&__{__v1_where_v1_is_Element_of_VAL_E_:_for_f_being_Function_of_VAR,E_st_f_=_v1_holds_ f_._x_in_f_._y__}__is_Subset_of_(VAL_E)_) let x, y be Variable; ::_thesis: ( { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } is Subset of (VAL E) & { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } is Subset of (VAL E) ) set X1 = { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ; set X2 = { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } ; { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } c= VAL E proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } or a in VAL E ) assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } ; ::_thesis: a in VAL E then ex v1 being Element of VAL E st ( a = v1 & ( for f being Function of VAR,E st f = v1 holds f . x = f . y ) ) ; hence a in VAL E ; ::_thesis: verum end; hence { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x = f . y } is Subset of (VAL E) ; ::_thesis: { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } is Subset of (VAL E) { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } c= VAL E proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } or a in VAL E ) assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } ; ::_thesis: a in VAL E then ex v1 being Element of VAL E st ( a = v1 & ( for f being Function of VAR,E st f = v1 holds f . x in f . y ) ) ; hence a in VAL E ; ::_thesis: verum end; hence { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds f . x in f . y } is Subset of (VAL E) ; ::_thesis: verum end; then A5: for x, y being Variable holds ( S1[H12(x,y)] & S1[H11(x,y)] ) ; A6: for a being set for x being Variable st S1[a] holds S1[H8(x,a)] proof let a be set ; ::_thesis: for x being Variable st S1[a] holds S1[H8(x,a)] let x be Variable; ::_thesis: ( S1[a] implies S1[H8(x,a)] ) assume a is Subset of (VAL E) ; ::_thesis: S1[H8(x,a)] set Y = { u5 where u5 is Element of VAL E : for X being set for f being Function of VAR,E st X = a & f = u5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in X ) ) } ; { u5 where u5 is Element of VAL E : for X being set for f being Function of VAR,E st X = a & f = u5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in X ) ) } c= VAL E proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { u5 where u5 is Element of VAL E : for X being set for f being Function of VAR,E st X = a & f = u5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in X ) ) } or b in VAL E ) assume b in { u5 where u5 is Element of VAL E : for X being set for f being Function of VAR,E st X = a & f = u5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in X ) ) } ; ::_thesis: b in VAL E then ex v1 being Element of VAL E st ( b = v1 & ( for X being set for f being Function of VAR,E st X = a & f = v1 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in X ) ) ) ) ; hence b in VAL E ; ::_thesis: verum end; hence S1[H8(x,a)] ; ::_thesis: verum end; A7: for H being ZF-formula for a being set holds ( a = H7(H) iff ex A being set st ( ( for x, y being Variable holds ( [(x '=' y),H12(x,y)] in A & [(x 'in' y),H11(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H12( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H11( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H10(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H9(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H8( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def3; thus S1[H7(H)] from ZF_MODEL:sch_4(A7, A5, A1, A2, A6); ::_thesis: verum end; end; theorem Th2: :: ZF_MODEL:2 for E being non empty set for x, y being Variable for f being Function of VAR,E holds ( f . x = f . y iff f in St ((x '=' y),E) ) proof let E be non empty set ; ::_thesis: for x, y being Variable for f being Function of VAR,E holds ( f . x = f . y iff f in St ((x '=' y),E) ) let x, y be Variable; ::_thesis: for f being Function of VAR,E holds ( f . x = f . y iff f in St ((x '=' y),E) ) let f be Function of VAR,E; ::_thesis: ( f . x = f . y iff f in St ((x '=' y),E) ) A1: x '=' y is being_equality by ZF_LANG:5; 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 where v1 is Element of VAL E : for f being Function of VAR,E 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) ) ::_thesis: ( f in St ((x '=' y),E) implies f . x = f . y ) proof reconsider v = f as Element of VAL E by FUNCT_2:8; assume f . x = f . y ; ::_thesis: f in St ((x '=' y),E) then for f being Function of VAR,E st f = v holds f . (Var1 (x '=' y)) = f . (Var2 (x '=' y)) by A2, A3, ZF_LANG:1; hence f in St ((x '=' y),E) by A5; ::_thesis: verum end; assume f in St ((x '=' y),E) ; ::_thesis: f . x = f . y then ex v1 being Element of VAL E st ( f = v1 & ( for f being Function of VAR,E st f = v1 holds f . (Var1 (x '=' y)) = f . (Var2 (x '=' y)) ) ) by A5; hence f . x = f . y by A3, A4; ::_thesis: verum end; theorem Th3: :: ZF_MODEL:3 for E being non empty set for x, y being Variable for f being Function of VAR,E holds ( f . x in f . y iff f in St ((x 'in' y),E) ) proof let E be non empty set ; ::_thesis: for x, y being Variable for f being Function of VAR,E holds ( f . x in f . y iff f in St ((x 'in' y),E) ) let x, y be Variable; ::_thesis: for f being Function of VAR,E holds ( f . x in f . y iff f in St ((x 'in' y),E) ) let f be Function of VAR,E; ::_thesis: ( f . x in f . y iff f in St ((x 'in' y),E) ) A1: x 'in' y is being_membership by ZF_LANG:5; 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 where v1 is Element of VAL E : for f being Function of VAR,E 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) ) ::_thesis: ( f in St ((x 'in' y),E) implies f . x in f . y ) proof reconsider v = f as Element of VAL E by FUNCT_2:8; assume f . x in f . y ; ::_thesis: f in St ((x 'in' y),E) then for f being Function of VAR,E st f = v holds f . (Var1 (x 'in' y)) in f . (Var2 (x 'in' y)) by A2, A3, ZF_LANG:2; hence f in St ((x 'in' y),E) by A5; ::_thesis: verum end; assume f in St ((x 'in' y),E) ; ::_thesis: f . x in f . y then ex v1 being Element of VAL E st ( f = v1 & ( for f being Function of VAR,E st f = v1 holds f . (Var1 (x 'in' y)) in f . (Var2 (x 'in' y)) ) ) by A5; hence f . x in f . y by A3, A4; ::_thesis: verum end; theorem Th4: :: ZF_MODEL:4 for E being non empty set for H being ZF-formula for f being Function of VAR,E holds ( not f in St (H,E) iff f in St (('not' H),E) ) proof let E be non empty set ; ::_thesis: for H being ZF-formula for f being Function of VAR,E holds ( not f in St (H,E) iff f in St (('not' H),E) ) let H be ZF-formula; ::_thesis: for f being Function of VAR,E holds ( not f in St (H,E) iff f in St (('not' H),E) ) let f be Function of VAR,E; ::_thesis: ( not f in St (H,E) iff f in St (('not' H),E) ) A1: union {(St (H,E))} = St (H,E) by ZFMISC_1:25; A2: 'not' H is negative by ZF_LANG:5; then H = the_argument_of ('not' H) by ZF_LANG:def_30; then A3: St (('not' H),E) = (VAL E) \ (St (H,E)) by A2, 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 A3, XBOOLE_0:def_5; ::_thesis: ( f in St (('not' H),E) implies not f in St (H,E) ) assume f in St (('not' H),E) ; ::_thesis: not f in St (H,E) hence not f in St (H,E) by A3, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th5: :: ZF_MODEL:5 for E being non empty set for H, H9 being ZF-formula for f being Function of VAR,E holds ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) ) proof let E be non empty set ; ::_thesis: for H, H9 being ZF-formula for f being Function of VAR,E holds ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) ) let H, H9 be ZF-formula; ::_thesis: for f being Function of VAR,E holds ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) ) let f be Function of VAR,E; ::_thesis: ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) ) A1: ( union {(St (H,E))} = St (H,E) & union {(St (H9,E))} = St (H9,E) ) by ZFMISC_1:25; A2: H '&' H9 is conjunctive by ZF_LANG:5; then A3: St ((H '&' H9),E) = (union {(St ((the_left_argument_of (H '&' H9)),E))}) /\ (union {(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 A2, ZF_LANG:40; then A4: ( 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 A3, A1, XBOOLE_0:def_4; ::_thesis: ( f in St ((H '&' H9),E) implies ( f in St (H,E) & f in St (H9,E) ) ) assume f in St ((H '&' H9),E) ; ::_thesis: ( f in St (H,E) & f in St (H9,E) ) hence ( f in St (H,E) & f in St (H9,E) ) by A3, A4, A1, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th6: :: ZF_MODEL:6 for E being non empty set for x being Variable for H being ZF-formula for f being Function of VAR,E holds ( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) iff f in St ((All (x,H)),E) ) proof let E be non empty set ; ::_thesis: for x being Variable for H being ZF-formula for f being Function of VAR,E holds ( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) iff f in St ((All (x,H)),E) ) let x be Variable; ::_thesis: for H being ZF-formula for f being Function of VAR,E holds ( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) iff f in St ((All (x,H)),E) ) let H be ZF-formula; ::_thesis: for f being Function of VAR,E holds ( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) iff f in St ((All (x,H)),E) ) let f be Function of VAR,E; ::_thesis: ( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) iff f in St ((All (x,H)),E) ) A1: All (x,H) is universal by ZF_LANG:5; then A2: St ((All (x,H)),E) = { v5 where v5 is Element of VAL E : for X being set for f being Function of VAR,E st X = St ((the_scope_of (All (x,H))),E) & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable 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 being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) implies f in St ((All (x,H)),E) ) ::_thesis: ( f in St ((All (x,H)),E) implies ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) ) proof reconsider v = f as Element of VAL E by FUNCT_2:8; assume ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) ; ::_thesis: f in St ((All (x,H)),E) then for X being set for h being Function of VAR,E st X = St ((the_scope_of (All (x,H))),E) & h = v holds ( h in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> h . y holds bound_in (All (x,H)) = y ) holds g in X ) ) by A4, A5; hence f in St ((All (x,H)),E) by A2; ::_thesis: verum end; assume f in St ((All (x,H)),E) ; ::_thesis: ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) ) then A6: ex v5 being Element of VAL E st ( f = v5 & ( for X being set for f being Function of VAR,E st X = St ((the_scope_of (All (x,H))),E) & f = v5 holds ( f in X & ( for g being Function of VAR,E st ( for y being Variable 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; ::_thesis: for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) let g be Function of VAR,E; ::_thesis: ( ( for y being Variable st g . y <> f . y holds x = y ) implies g in St (H,E) ) assume for y being Variable st g . y <> f . y holds x = y ; ::_thesis: g in St (H,E) hence g in St (H,E) by A4, A5, A6; ::_thesis: verum end; theorem :: ZF_MODEL:7 for H being ZF-formula for E being non empty set st H is being_equality holds for f being Function of VAR,E holds ( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) proof let H be ZF-formula; ::_thesis: for E being non empty set st H is being_equality holds for f being Function of VAR,E holds ( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) let E be non empty set ; ::_thesis: ( H is being_equality implies for f being Function of VAR,E holds ( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) ) assume H is being_equality ; ::_thesis: for f being Function of VAR,E holds ( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) then H = (Var1 H) '=' (Var2 H) by ZF_LANG:36; hence for f being Function of VAR,E holds ( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) by Th2; ::_thesis: verum end; theorem :: ZF_MODEL:8 for H being ZF-formula for E being non empty set st H is being_membership holds for f being Function of VAR,E holds ( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) proof let H be ZF-formula; ::_thesis: for E being non empty set st H is being_membership holds for f being Function of VAR,E holds ( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) let E be non empty set ; ::_thesis: ( H is being_membership implies for f being Function of VAR,E holds ( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) ) assume H is being_membership ; ::_thesis: for f being Function of VAR,E holds ( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) then H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37; hence for f being Function of VAR,E holds ( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) by Th3; ::_thesis: verum end; theorem :: ZF_MODEL:9 for H being ZF-formula for E being non empty set st H is negative holds for f being Function of VAR,E holds ( not f in St ((the_argument_of H),E) iff f in St (H,E) ) proof let H be ZF-formula; ::_thesis: for E being non empty set st H is negative holds for f being Function of VAR,E holds ( not f in St ((the_argument_of H),E) iff f in St (H,E) ) let E be non empty set ; ::_thesis: ( H is negative implies for f being Function of VAR,E holds ( not f in St ((the_argument_of H),E) iff f in St (H,E) ) ) assume H is negative ; ::_thesis: for f being Function of VAR,E holds ( not f in St ((the_argument_of H),E) iff f in St (H,E) ) then H = 'not' (the_argument_of H) by ZF_LANG:def_30; hence for f being Function of VAR,E holds ( not f in St ((the_argument_of H),E) iff f in St (H,E) ) by Th4; ::_thesis: verum end; theorem :: ZF_MODEL:10 for H being ZF-formula for E being non empty set st H is conjunctive holds for f being Function of VAR,E 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 let H be ZF-formula; ::_thesis: for E being non empty set st H is conjunctive holds for f being Function of VAR,E 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) ) let E be non empty set ; ::_thesis: ( H is conjunctive implies for f being Function of VAR,E 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) ) ) assume H is conjunctive ; ::_thesis: for f being Function of VAR,E 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) ) then H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40; hence for f being Function of VAR,E 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) ) by Th5; ::_thesis: verum end; theorem :: ZF_MODEL:11 for H being ZF-formula for E being non empty set st H is universal holds for f being Function of VAR,E holds ( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable 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 let H be ZF-formula; ::_thesis: for E being non empty set st H is universal holds for f being Function of VAR,E holds ( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable 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) ) let E be non empty set ; ::_thesis: ( H is universal implies for f being Function of VAR,E holds ( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable 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) ) ) assume H is universal ; ::_thesis: for f being Function of VAR,E holds ( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable 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) ) then H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44; hence for f being Function of VAR,E holds ( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable 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) ) by Th6; ::_thesis: verum end; definition let D be non empty set ; let f be Function of VAR,D; let H be ZF-formula; predD,f |= H means :Def4: :: ZF_MODEL:def 4 f in St (H,D); end; :: deftheorem Def4 defines |= ZF_MODEL:def_4_:_ for D being non empty set for f being Function of VAR,D for H being ZF-formula holds ( D,f |= H iff f in St (H,D) ); theorem :: ZF_MODEL:12 for E being non empty set for f being Function of VAR,E for x, y being Variable holds ( E,f |= x '=' y iff f . x = f . y ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for x, y being Variable holds ( E,f |= x '=' y iff f . x = f . y ) let f be Function of VAR,E; ::_thesis: for x, y being Variable holds ( E,f |= x '=' y iff f . x = f . y ) let x, y be Variable; ::_thesis: ( E,f |= x '=' y iff f . x = f . y ) ( E,f |= x '=' y iff f in St ((x '=' y),E) ) by Def4; hence ( E,f |= x '=' y iff f . x = f . y ) by Th2; ::_thesis: verum end; theorem :: ZF_MODEL:13 for E being non empty set for f being Function of VAR,E for x, y being Variable holds ( E,f |= x 'in' y iff f . x in f . y ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for x, y being Variable holds ( E,f |= x 'in' y iff f . x in f . y ) let f be Function of VAR,E; ::_thesis: for x, y being Variable holds ( E,f |= x 'in' y iff f . x in f . y ) let x, y be Variable; ::_thesis: ( E,f |= x 'in' y iff f . x in f . y ) ( E,f |= x 'in' y iff f in St ((x 'in' y),E) ) by Def4; hence ( E,f |= x 'in' y iff f . x in f . y ) by Th3; ::_thesis: verum end; theorem Th14: :: ZF_MODEL:14 for E being non empty set for f being Function of VAR,E for H being ZF-formula holds ( E,f |= H iff not E,f |= 'not' H ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H being ZF-formula holds ( E,f |= H iff not E,f |= 'not' H ) let f be Function of VAR,E; ::_thesis: for H being ZF-formula holds ( E,f |= H iff not E,f |= 'not' H ) let H be ZF-formula; ::_thesis: ( E,f |= H iff not E,f |= 'not' H ) A1: ( E,f |= 'not' H iff f in St (('not' H),E) ) by Def4; ( E,f |= H iff f in St (H,E) ) by Def4; hence ( E,f |= H iff not E,f |= 'not' H ) by A1, Th4; ::_thesis: verum end; theorem Th15: :: ZF_MODEL:15 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) let f be Function of VAR,E; ::_thesis: for H, H9 being ZF-formula holds ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) let H, H9 be ZF-formula; ::_thesis: ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) A1: ( E,f |= H iff f in St (H,E) ) by Def4; A2: ( E,f |= H9 iff f in St (H9,E) ) by Def4; ( E,f |= H '&' H9 iff f in St ((H '&' H9),E) ) by Def4; hence ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) by A1, A2, Th5; ::_thesis: verum end; theorem Th16: :: ZF_MODEL:16 for E being non empty set for f being Function of VAR,E for H being ZF-formula for x being Variable holds ( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H being ZF-formula for x being Variable holds ( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) let f be Function of VAR,E; ::_thesis: for H being ZF-formula for x being Variable holds ( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) let H be ZF-formula; ::_thesis: for x being Variable holds ( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) let x be Variable; ::_thesis: ( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) A1: ( ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) implies E,f |= H ) proof A2: for y being Variable st f . y <> f . y holds x = y ; assume for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ; ::_thesis: E,f |= H hence E,f |= H by A2; ::_thesis: verum end; A3: ( E,f |= All (x,H) iff f in St ((All (x,H)),E) ) by Def4; A4: ( ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) implies for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) proof assume A5: for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ; ::_thesis: for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) let g be Function of VAR,E; ::_thesis: ( ( for y being Variable st g . y <> f . y holds x = y ) implies g in St (H,E) ) assume for y being Variable st g . y <> f . y holds x = y ; ::_thesis: g in St (H,E) then E,g |= H by A5; hence g in St (H,E) by Def4; ::_thesis: verum end; A6: ( ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ) implies for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) proof assume A7: for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds g in St (H,E) ; ::_thesis: for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H let g be Function of VAR,E; ::_thesis: ( ( for y being Variable st g . y <> f . y holds x = y ) implies E,g |= H ) assume for y being Variable st g . y <> f . y holds x = y ; ::_thesis: E,g |= H then g in St (H,E) by A7; hence E,g |= H by Def4; ::_thesis: verum end; ( E,f |= H iff f in St (H,E) ) by Def4; hence ( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H ) by A3, A6, A4, A1, Th6; ::_thesis: verum end; theorem :: ZF_MODEL:17 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) ) let f be Function of VAR,E; ::_thesis: for H, H9 being ZF-formula holds ( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) ) let H, H9 be ZF-formula; ::_thesis: ( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) ) ( E,f |= ('not' H) '&' ('not' H9) iff ( E,f |= 'not' H & E,f |= 'not' H9 ) ) by Th15; hence ( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) ) by Th14; ::_thesis: verum end; theorem Th18: :: ZF_MODEL:18 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) ) let f be Function of VAR,E; ::_thesis: for H, H9 being ZF-formula holds ( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) ) let H, H9 be ZF-formula; ::_thesis: ( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) ) ( E,f |= H '&' ('not' H9) iff ( E,f |= H & E,f |= 'not' H9 ) ) by Th15; hence ( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) ) by Th14; ::_thesis: verum end; theorem :: ZF_MODEL:19 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) let f be Function of VAR,E; ::_thesis: for H, H9 being ZF-formula holds ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) let H, H9 be ZF-formula; ::_thesis: ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) ( E,f |= (H => H9) '&' (H9 => H) iff ( E,f |= H => H9 & E,f |= H9 => H ) ) by Th15; hence ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) by Th18; ::_thesis: verum end; theorem Th20: :: ZF_MODEL:20 for E being non empty set for f being Function of VAR,E for H being ZF-formula for x being Variable holds ( E,f |= Ex (x,H) iff ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) ) proof let E be non empty set ; ::_thesis: for f being Function of VAR,E for H being ZF-formula for x being Variable holds ( E,f |= Ex (x,H) iff ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) ) let f be Function of VAR,E; ::_thesis: for H being ZF-formula for x being Variable holds ( E,f |= Ex (x,H) iff ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) ) let H be ZF-formula; ::_thesis: for x being Variable holds ( E,f |= Ex (x,H) iff ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) ) let x be Variable; ::_thesis: ( E,f |= Ex (x,H) iff ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) ) A1: ( E,f |= 'not' (All (x,('not' H))) iff not E,f |= All (x,('not' H)) ) by Th14; thus ( E,f |= Ex (x,H) implies ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) ) ::_thesis: ( ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) implies E,f |= Ex (x,H) ) proof assume E,f |= Ex (x,H) ; ::_thesis: ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) then consider g being Function of VAR,E such that A2: for y being Variable st g . y <> f . y holds x = y and A3: not E,g |= 'not' H by A1, Th16; E,g |= H by A3, Th14; hence ex g being Function of VAR,E st ( ( for y being Variable st g . y <> f . y holds x = y ) & E,g |= H ) by A2; ::_thesis: verum end; given g being Function of VAR,E such that A4: for y being Variable st g . y <> f . y holds x = y and A5: E,g |= H ; ::_thesis: E,f |= Ex (x,H) not E,g |= 'not' H by A5, Th14; hence E,f |= Ex (x,H) by A1, A4, Th16; ::_thesis: verum end; theorem :: ZF_MODEL:21 for H being ZF-formula for x, y being Variable for E being non empty set for f being Function of VAR,E holds ( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) proof let H be ZF-formula; ::_thesis: for x, y being Variable for E being non empty set for f being Function of VAR,E holds ( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) let x, y be Variable; ::_thesis: for E being non empty set for f being Function of VAR,E holds ( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) let E be non empty set ; ::_thesis: for f being Function of VAR,E holds ( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) let f be Function of VAR,E; ::_thesis: ( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) thus ( E,f |= All (x,y,H) implies for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) ::_thesis: ( ( for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ) implies E,f |= All (x,y,H) ) proof assume A1: E,f |= All (x,y,H) ; ::_thesis: for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H A2: for g being Function of VAR,E st ( for z being Variable st g . z <> f . z holds x = z ) holds for h being Function of VAR,E st ( for z being Variable st h . z <> g . z holds y = z ) holds E,h |= H proof let g be Function of VAR,E; ::_thesis: ( ( for z being Variable st g . z <> f . z holds x = z ) implies for h being Function of VAR,E st ( for z being Variable st h . z <> g . z holds y = z ) holds E,h |= H ) assume for z being Variable st g . z <> f . z holds x = z ; ::_thesis: for h being Function of VAR,E st ( for z being Variable st h . z <> g . z holds y = z ) holds E,h |= H then E,g |= All (y,H) by A1, Th16; hence for h being Function of VAR,E st ( for z being Variable st h . z <> g . z holds y = z ) holds E,h |= H by Th16; ::_thesis: verum end; let g be Function of VAR,E; ::_thesis: ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) implies E,g |= H ) assume A3: for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ; ::_thesis: E,g |= H set h = g +* (y,(f . y)); for z being Variable st (g +* (y,(f . y))) . z <> f . z holds x = z proof let z be Variable; ::_thesis: ( (g +* (y,(f . y))) . z <> f . z implies x = z ) assume that A4: (g +* (y,(f . y))) . z <> f . z and A5: x <> z ; ::_thesis: contradiction A6: y <> z by A4, FUNCT_7:128; then g . z = f . z by A3, A5; hence contradiction by A4, A6, FUNCT_7:32; ::_thesis: verum end; then ( ( for z being Variable st g . z <> (g +* (y,(f . y))) . z holds y = z ) implies E,g |= H ) by A2; hence E,g |= H by FUNCT_7:32; ::_thesis: verum end; assume A7: for g being Function of VAR,E st ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) holds E,g |= H ; ::_thesis: E,f |= All (x,y,H) now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_z_being_Variable_st_g_._z_<>_f_._z_holds_ x_=_z_)_holds_ E,g_|=_All_(y,H) let g be Function of VAR,E; ::_thesis: ( ( for z being Variable st g . z <> f . z holds x = z ) implies E,g |= All (y,H) ) assume A8: for z being Variable st g . z <> f . z holds x = z ; ::_thesis: E,g |= All (y,H) now__::_thesis:_for_h_being_Function_of_VAR,E_st_(_for_z_being_Variable_st_h_._z_<>_g_._z_holds_ y_=_z_)_holds_ E,h_|=_H let h be Function of VAR,E; ::_thesis: ( ( for z being Variable st h . z <> g . z holds y = z ) implies E,h |= H ) assume A9: for z being Variable st h . z <> g . z holds y = z ; ::_thesis: E,h |= H now__::_thesis:_for_z_being_Variable_st_h_._z_<>_f_._z_&_x_<>_z_holds_ not_y_<>_z let z be Variable; ::_thesis: ( h . z <> f . z & x <> z implies not y <> z ) assume that A10: ( h . z <> f . z & x <> z ) and A11: y <> z ; ::_thesis: contradiction h . z = g . z by A9, A11; hence contradiction by A8, A10; ::_thesis: verum end; hence E,h |= H by A7; ::_thesis: verum end; hence E,g |= All (y,H) by Th16; ::_thesis: verum end; hence E,f |= All (x,y,H) by Th16; ::_thesis: verum end; theorem :: ZF_MODEL:22 for H being ZF-formula for x, y being Variable for E being non empty set for f being Function of VAR,E holds ( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) proof let H be ZF-formula; ::_thesis: for x, y being Variable for E being non empty set for f being Function of VAR,E holds ( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) let x, y be Variable; ::_thesis: for E being non empty set for f being Function of VAR,E holds ( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) let E be non empty set ; ::_thesis: for f being Function of VAR,E holds ( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) let f be Function of VAR,E; ::_thesis: ( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) thus ( E,f |= Ex (x,y,H) implies ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) ::_thesis: ( ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) implies E,f |= Ex (x,y,H) ) proof assume E,f |= Ex (x,y,H) ; ::_thesis: ex g being Function of VAR,E st ( ( for z being Variable holds ( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) then consider g being Function of VAR,E such that A1: for z being Variable st g . z <> f . z holds x = z and A2: E,g |= Ex (y,H) by Th20; consider h being Function of VAR,E such that A3: for z being Variable st h . z <> g . z holds y = z and A4: E,h |= H by A2, Th20; take h ; ::_thesis: ( ( for z being Variable holds ( not h . z <> f . z or x = z or y = z ) ) & E,h |= H ) thus for z being Variable holds ( not h . z <> f . z or x = z or y = z ) ::_thesis: E,h |= H proof let z be Variable; ::_thesis: ( not h . z <> f . z or x = z or y = z ) assume that A5: h . z <> f . z and A6: x <> z and A7: y <> z ; ::_thesis: contradiction g . z = f . z by A1, A6; hence contradiction by A3, A5, A7; ::_thesis: verum end; thus E,h |= H by A4; ::_thesis: verum end; given g being Function of VAR,E such that A8: for z being Variable holds ( not g . z <> f . z or x = z or y = z ) and A9: E,g |= H ; ::_thesis: E,f |= Ex (x,y,H) set h = f +* (x,(g . x)); now__::_thesis:_for_z_being_Variable_st_g_._z_<>_(f_+*_(x,(g_._x)))_._z_holds_ not_y_<>_z let z be Variable; ::_thesis: ( g . z <> (f +* (x,(g . x))) . z implies not y <> z ) assume that A10: g . z <> (f +* (x,(g . x))) . z and A11: y <> z ; ::_thesis: contradiction A12: x <> z by A10, FUNCT_7:128; then g . z = f . z by A8, A11; hence contradiction by A10, A12, FUNCT_7:32; ::_thesis: verum end; then A13: E,f +* (x,(g . x)) |= Ex (y,H) by A9, Th20; for z being Variable st (f +* (x,(g . x))) . z <> f . z holds x = z by FUNCT_7:32; hence E,f |= Ex (x,y,H) by A13, Th20; ::_thesis: verum end; definition let E be non empty set ; let H be ZF-formula; predE |= H means :Def5: :: ZF_MODEL:def 5 for f being Function of VAR,E holds E,f |= H; end; :: deftheorem Def5 defines |= ZF_MODEL:def_5_:_ for E being non empty set for H being ZF-formula holds ( E |= H iff for f being Function of VAR,E holds E,f |= H ); theorem :: ZF_MODEL:23 for H being ZF-formula for x being Variable for E being non empty set holds ( E |= All (x,H) iff E |= H ) proof let H be ZF-formula; ::_thesis: for x being Variable for E being non empty set holds ( E |= All (x,H) iff E |= H ) let x be Variable; ::_thesis: for E being non empty set holds ( E |= All (x,H) iff E |= H ) let E be non empty set ; ::_thesis: ( E |= All (x,H) iff E |= H ) thus ( E |= All (x,H) implies E |= H ) ::_thesis: ( E |= H implies E |= All (x,H) ) proof assume A1: for f being Function of VAR,E holds E,f |= All (x,H) ; :: according to ZF_MODEL:def_5 ::_thesis: E |= H let f be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f |= H A2: for y being Variable st f . y <> f . y holds x = y ; E,f |= All (x,H) by A1; hence E,f |= H by A2, Th16; ::_thesis: verum end; assume A3: E |= H ; ::_thesis: E |= All (x,H) let f be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f |= All (x,H) for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds x = y ) holds E,g |= H by A3, Def5; hence E,f |= All (x,H) by Th16; ::_thesis: verum end; definition func the_axiom_of_extensionality -> ZF-formula equals :: ZF_MODEL:def 6 All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))); correctness coherence All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) is ZF-formula; ; func the_axiom_of_pairs -> ZF-formula equals :: ZF_MODEL:def 7 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 coherence 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))))))))) is ZF-formula; ; func the_axiom_of_unions -> ZF-formula equals :: ZF_MODEL:def 8 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 coherence 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))))))))))) is ZF-formula; ; func the_axiom_of_infinity -> ZF-formula equals :: ZF_MODEL:def 9 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 coherence 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))))))))))))) is ZF-formula; ; func the_axiom_of_power_sets -> ZF-formula equals :: ZF_MODEL:def 10 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 coherence 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))))))))))) is ZF-formula; ; end; :: deftheorem defines the_axiom_of_extensionality ZF_MODEL:def_6_:_ the_axiom_of_extensionality = All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))); :: deftheorem defines the_axiom_of_pairs ZF_MODEL:def_7_:_ the_axiom_of_pairs = 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))))))))); :: deftheorem defines the_axiom_of_unions ZF_MODEL:def_8_:_ the_axiom_of_unions = 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))))))))))); :: deftheorem defines the_axiom_of_infinity ZF_MODEL:def_9_:_ the_axiom_of_infinity = 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))))))))))))); :: deftheorem defines the_axiom_of_power_sets ZF_MODEL:def_10_:_ the_axiom_of_power_sets = 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))))))))))); definition let H be ZF-formula; func the_axiom_of_substitution_for H -> ZF-formula equals :: ZF_MODEL:def 11 (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 coherence (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)))))))))) is ZF-formula; ; end; :: deftheorem defines the_axiom_of_substitution_for ZF_MODEL:def_11_:_ for H being ZF-formula holds the_axiom_of_substitution_for H = (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)))))))))); definition let E be non empty set ; attrE is being_a_model_of_ZF means :: ZF_MODEL:def 12 ( 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 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds E |= the_axiom_of_substitution_for H ) ); end; :: deftheorem defines being_a_model_of_ZF ZF_MODEL:def_12_:_ for E being non empty set holds ( E is being_a_model_of_ZF iff ( 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 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds E |= the_axiom_of_substitution_for H ) ) );