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