let E be non empty set ; :: thesis: for H being ZF-formula

for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H holds

E,g |= H

defpred S_{2}[ ZF-formula] means for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free $1 ) & E,f |= $1 holds

E,g |= $1;

A1: for H being ZF-formula st H is atomic holds

S_{2}[H]
_{2}[ the_left_argument_of H] & S_{2}[ the_right_argument_of H] holds

S_{2}[H]
_{2}[ the_scope_of H] holds

S_{2}[H]
_{2}[ the_argument_of H] holds

S_{2}[H]
_{2}[H]
from ZF_LANG:sch 1(A1, A39, A16, A27); :: thesis: verum

for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H holds

E,g |= H

defpred S

not x in Free $1 ) & E,f |= $1 holds

E,g |= $1;

A1: for H being ZF-formula st H is atomic holds

S

proof

A16:
for H being ZF-formula st H is conjunctive & S
let H be ZF-formula; :: thesis: ( H is atomic implies S_{2}[H] )

assume A2: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: S_{2}[H]

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A3: for x being Variable st f . x <> g . x holds

not x in Free H and

A4: E,f |= H ; :: thesis: E,g |= H

end;assume A2: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: S

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A3: for x being Variable st f . x <> g . x holds

not x in Free H and

A4: E,f |= H ; :: thesis: E,g |= H

A5: now :: thesis: ( H is being_membership implies E,g |= H )

assume A6:
H is being_membership
; :: thesis: E,g |= H

then A7: Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;

then Var1 H in Free H by TARSKI:def 2;

then A8: f . (Var1 H) = g . (Var1 H) by A3;

Var2 H in Free H by A7, TARSKI:def 2;

then A9: f . (Var2 H) = g . (Var2 H) by A3;

A10: H = (Var1 H) 'in' (Var2 H) by A6, ZF_LANG:37;

then f . (Var1 H) in f . (Var2 H) by A4, ZF_MODEL:13;

hence E,g |= H by A10, A8, A9, ZF_MODEL:13; :: thesis: verum

end;then A7: Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;

then Var1 H in Free H by TARSKI:def 2;

then A8: f . (Var1 H) = g . (Var1 H) by A3;

Var2 H in Free H by A7, TARSKI:def 2;

then A9: f . (Var2 H) = g . (Var2 H) by A3;

A10: H = (Var1 H) 'in' (Var2 H) by A6, ZF_LANG:37;

then f . (Var1 H) in f . (Var2 H) by A4, ZF_MODEL:13;

hence E,g |= H by A10, A8, A9, ZF_MODEL:13; :: thesis: verum

now :: thesis: ( H is being_equality implies E,g |= H )

hence
E,g |= H
by A2, A5; :: thesis: verumassume A11:
H is being_equality
; :: thesis: E,g |= H

then A12: Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;

then Var1 H in Free H by TARSKI:def 2;

then A13: f . (Var1 H) = g . (Var1 H) by A3;

Var2 H in Free H by A12, TARSKI:def 2;

then A14: f . (Var2 H) = g . (Var2 H) by A3;

A15: H = (Var1 H) '=' (Var2 H) by A11, ZF_LANG:36;

then f . (Var1 H) = f . (Var2 H) by A4, ZF_MODEL:12;

hence E,g |= H by A15, A13, A14, ZF_MODEL:12; :: thesis: verum

end;then A12: Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;

then Var1 H in Free H by TARSKI:def 2;

then A13: f . (Var1 H) = g . (Var1 H) by A3;

Var2 H in Free H by A12, TARSKI:def 2;

then A14: f . (Var2 H) = g . (Var2 H) by A3;

A15: H = (Var1 H) '=' (Var2 H) by A11, ZF_LANG:36;

then f . (Var1 H) = f . (Var2 H) by A4, ZF_MODEL:12;

hence E,g |= H by A15, A13, A14, ZF_MODEL:12; :: thesis: verum

S

proof

A27:
for H being ZF-formula st H is universal & S
let H be ZF-formula; :: thesis: ( H is conjunctive & S_{2}[ the_left_argument_of H] & S_{2}[ the_right_argument_of H] implies S_{2}[H] )

assume A17: H is conjunctive ; :: thesis: ( not S_{2}[ the_left_argument_of H] or not S_{2}[ the_right_argument_of H] or S_{2}[H] )

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

assume that

A19: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_left_argument_of H) ) & E,f |= the_left_argument_of H holds

E,g |= the_left_argument_of H and

A20: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_right_argument_of H) ) & E,f |= the_right_argument_of H holds

E,g |= the_right_argument_of H ; :: thesis: S_{2}[H]

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A21: for x being Variable st f . x <> g . x holds

not x in Free H and

A22: E,f |= H ; :: thesis: E,g |= H

A23: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A17, ZF_MODEL:1;

then A26: E,g |= the_right_argument_of H by A20, A24;

E,f |= the_left_argument_of H by A18, A22, ZF_MODEL:15;

then E,g |= the_left_argument_of H by A19, A25;

hence E,g |= H by A18, A26, ZF_MODEL:15; :: thesis: verum

end;assume A17: H is conjunctive ; :: thesis: ( not S

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

assume that

A19: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_left_argument_of H) ) & E,f |= the_left_argument_of H holds

E,g |= the_left_argument_of H and

A20: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_right_argument_of H) ) & E,f |= the_right_argument_of H holds

E,g |= the_right_argument_of H ; :: thesis: S

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A21: for x being Variable st f . x <> g . x holds

not x in Free H and

A22: E,f |= H ; :: thesis: E,g |= H

A23: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A17, ZF_MODEL:1;

A24: now :: thesis: for x being Variable st f . x <> g . x holds

not x in Free (the_right_argument_of H)

not x in Free (the_right_argument_of H)

let x be Variable; :: thesis: ( f . x <> g . x implies not x in Free (the_right_argument_of H) )

assume f . x <> g . x ; :: thesis: not x in Free (the_right_argument_of H)

then not x in Free H by A21;

hence not x in Free (the_right_argument_of H) by A23, XBOOLE_0:def 3; :: thesis: verum

end;assume f . x <> g . x ; :: thesis: not x in Free (the_right_argument_of H)

then not x in Free H by A21;

hence not x in Free (the_right_argument_of H) by A23, XBOOLE_0:def 3; :: thesis: verum

A25: now :: thesis: for x being Variable st f . x <> g . x holds

not x in Free (the_left_argument_of H)

E,f |= the_right_argument_of H
by A18, A22, ZF_MODEL:15;not x in Free (the_left_argument_of H)

let x be Variable; :: thesis: ( f . x <> g . x implies not x in Free (the_left_argument_of H) )

assume f . x <> g . x ; :: thesis: not x in Free (the_left_argument_of H)

then not x in Free H by A21;

hence not x in Free (the_left_argument_of H) by A23, XBOOLE_0:def 3; :: thesis: verum

end;assume f . x <> g . x ; :: thesis: not x in Free (the_left_argument_of H)

then not x in Free H by A21;

hence not x in Free (the_left_argument_of H) by A23, XBOOLE_0:def 3; :: thesis: verum

then A26: E,g |= the_right_argument_of H by A20, A24;

E,f |= the_left_argument_of H by A18, A22, ZF_MODEL:15;

then E,g |= the_left_argument_of H by A19, A25;

hence E,g |= H by A18, A26, ZF_MODEL:15; :: thesis: verum

S

proof

A39:
for H being ZF-formula st H is negative & S
let H be ZF-formula; :: thesis: ( H is universal & S_{2}[ the_scope_of H] implies S_{2}[H] )

assume A28: H is universal ; :: thesis: ( not S_{2}[ the_scope_of H] or S_{2}[H] )

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

assume A30: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_scope_of H) ) & E,f |= the_scope_of H holds

E,g |= the_scope_of H ; :: thesis: S_{2}[H]

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A31: for x being Variable st f . x <> g . x holds

not x in Free H and

A32: E,f |= H ; :: thesis: E,g |= H

A33: Free H = (Free (the_scope_of H)) \ {(bound_in H)} by A28, ZF_MODEL:1;

end;assume A28: H is universal ; :: thesis: ( not S

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

assume A30: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_scope_of H) ) & E,f |= the_scope_of H holds

E,g |= the_scope_of H ; :: thesis: S

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A31: for x being Variable st f . x <> g . x holds

not x in Free H and

A32: E,f |= H ; :: thesis: E,g |= H

A33: Free H = (Free (the_scope_of H)) \ {(bound_in H)} by A28, ZF_MODEL:1;

now :: thesis: for j being Function of VAR,E st ( for x being Variable st j . x <> g . x holds

bound_in H = x ) holds

E,j |= the_scope_of H

hence
E,g |= H
by A29, ZF_MODEL:16; :: thesis: verumbound_in H = x ) holds

E,j |= the_scope_of H

let j be Function of VAR,E; :: thesis: ( ( for x being Variable st j . x <> g . x holds

bound_in H = x ) implies E,j |= the_scope_of H )

assume A34: for x being Variable st j . x <> g . x holds

bound_in H = x ; :: thesis: E,j |= the_scope_of H

set h = f +* ((bound_in H),(j . (bound_in H)));

bound_in H = x by FUNCT_7:32;

then E,f +* ((bound_in H),(j . (bound_in H))) |= the_scope_of H by A29, A32, ZF_MODEL:16;

hence E,j |= the_scope_of H by A30, A35; :: thesis: verum

end;bound_in H = x ) implies E,j |= the_scope_of H )

assume A34: for x being Variable st j . x <> g . x holds

bound_in H = x ; :: thesis: E,j |= the_scope_of H

set h = f +* ((bound_in H),(j . (bound_in H)));

A35: now :: thesis: for x being Variable st (f +* ((bound_in H),(j . (bound_in H)))) . x <> j . x holds

not x in Free (the_scope_of H)

for x being Variable st (f +* ((bound_in H),(j . (bound_in H)))) . x <> f . x holds not x in Free (the_scope_of H)

let x be Variable; :: thesis: ( (f +* ((bound_in H),(j . (bound_in H)))) . x <> j . x implies not x in Free (the_scope_of H) )

assume A36: (f +* ((bound_in H),(j . (bound_in H)))) . x <> j . x ; :: thesis: not x in Free (the_scope_of H)

then A37: x <> bound_in H by FUNCT_7:128;

then ( (f +* ((bound_in H),(j . (bound_in H)))) . x = f . x & j . x = g . x ) by A34, FUNCT_7:32;

then A38: not x in Free H by A31, A36;

not x in {(bound_in H)} by A37, TARSKI:def 1;

hence not x in Free (the_scope_of H) by A33, A38, XBOOLE_0:def 5; :: thesis: verum

end;assume A36: (f +* ((bound_in H),(j . (bound_in H)))) . x <> j . x ; :: thesis: not x in Free (the_scope_of H)

then A37: x <> bound_in H by FUNCT_7:128;

then ( (f +* ((bound_in H),(j . (bound_in H)))) . x = f . x & j . x = g . x ) by A34, FUNCT_7:32;

then A38: not x in Free H by A31, A36;

not x in {(bound_in H)} by A37, TARSKI:def 1;

hence not x in Free (the_scope_of H) by A33, A38, XBOOLE_0:def 5; :: thesis: verum

bound_in H = x by FUNCT_7:32;

then E,f +* ((bound_in H),(j . (bound_in H))) |= the_scope_of H by A29, A32, ZF_MODEL:16;

hence E,j |= the_scope_of H by A30, A35; :: thesis: verum

S

proof

thus
for H being ZF-formula holds S
let H be ZF-formula; :: thesis: ( H is negative & S_{2}[ the_argument_of H] implies S_{2}[H] )

assume A40: H is negative ; :: thesis: ( not S_{2}[ the_argument_of H] or S_{2}[H] )

then A41: Free H = Free (the_argument_of H) by ZF_MODEL:1;

assume A42: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_argument_of H) ) & E,f |= the_argument_of H holds

E,g |= the_argument_of H ; :: thesis: S_{2}[H]

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A43: for x being Variable st f . x <> g . x holds

not x in Free H and

A44: E,f |= H and

A45: not E,g |= H ; :: thesis: contradiction

A46: H = 'not' (the_argument_of H) by A40, ZF_LANG:def 30;

then E,g |= the_argument_of H by A45, ZF_MODEL:14;

then E,f |= the_argument_of H by A41, A42, A43;

hence contradiction by A46, A44, ZF_MODEL:14; :: thesis: verum

end;assume A40: H is negative ; :: thesis: ( not S

then A41: Free H = Free (the_argument_of H) by ZF_MODEL:1;

assume A42: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free (the_argument_of H) ) & E,f |= the_argument_of H holds

E,g |= the_argument_of H ; :: thesis: S

let f, g be Function of VAR,E; :: thesis: ( ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H implies E,g |= H )

assume that

A43: for x being Variable st f . x <> g . x holds

not x in Free H and

A44: E,f |= H and

A45: not E,g |= H ; :: thesis: contradiction

A46: H = 'not' (the_argument_of H) by A40, ZF_LANG:def 30;

then E,g |= the_argument_of H by A45, ZF_MODEL:14;

then E,f |= the_argument_of H by A41, A42, A43;

hence contradiction by A46, A44, ZF_MODEL:14; :: thesis: verum