let n be Nat; :: thesis: ( ( for k being Nat st k < n holds

S_{1}[k] ) implies S_{1}[n] )

assume A1: for k being Nat st k < n holds

for x being Variable

for E being non empty set

for H being ZF-formula

for f being Function of VAR,E st len H = k & not x in Free H & E,f |= H holds

E,f |= All (x,H) ; :: thesis: S_{1}[n]

let x be Variable; :: thesis: for E being non empty set

for H being ZF-formula

for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds

E,f |= All (x,H)

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

for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds

E,f |= All (x,H)

let H be ZF-formula; :: thesis: for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds

E,f |= All (x,H)

let f be Function of VAR,E; :: thesis: ( len H = n & not x in Free H & E,f |= H implies E,f |= All (x,H) )

assume that

A2: len H = n and

A3: not x in Free H and

A4: E,f |= H ; :: thesis: E,f |= All (x,H)

S

assume A1: for k being Nat st k < n holds

for x being Variable

for E being non empty set

for H being ZF-formula

for f being Function of VAR,E st len H = k & not x in Free H & E,f |= H holds

E,f |= All (x,H) ; :: thesis: S

let x be Variable; :: thesis: for E being non empty set

for H being ZF-formula

for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds

E,f |= All (x,H)

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

for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds

E,f |= All (x,H)

let H be ZF-formula; :: thesis: for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds

E,f |= All (x,H)

let f be Function of VAR,E; :: thesis: ( len H = n & not x in Free H & E,f |= H implies E,f |= All (x,H) )

assume that

A2: len H = n and

A3: not x in Free H and

A4: E,f |= H ; :: thesis: E,f |= All (x,H)

A5: now :: thesis: ( H is being_equality implies E,f |= All (x,H) )

assume A6:
H is being_equality
; :: thesis: E,f |= All (x,H)

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

then A7: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2;

A8: H = (Var1 H) '=' (Var2 H) by A6, ZF_LANG:36;

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

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

then A7: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2;

A8: H = (Var1 H) '=' (Var2 H) by A6, ZF_LANG:36;

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

now :: 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

hence
E,f |= All (x,H)
by ZF_MODEL:16; :: thesis: verumx = 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 . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A7;

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

end;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 . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A7;

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

A10: now :: thesis: ( H is universal implies E,f |= All (x,H) )

assume A11:
H is universal
; :: thesis: E,f |= All (x,H)

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

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

then A13: ( not x in Free (the_scope_of H) or x in {(bound_in H)} ) by A3, XBOOLE_0:def 5;

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

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

then A13: ( not x in Free (the_scope_of H) or x in {(bound_in H)} ) by A3, XBOOLE_0:def 5;

A14: now :: thesis: ( x <> bound_in H implies E,f |= All (x,H) )

assume A15:
x <> bound_in H
; :: thesis: E,f |= All (x,H)

assume not E,f |= All (x,H) ; :: thesis: contradiction

then consider g being Function of VAR,E such that

A16: for y being Variable st g . y <> f . y holds

x = y and

A17: not E,g |= H by ZF_MODEL:16;

consider h being Function of VAR,E such that

A18: for y being Variable st h . y <> g . y holds

bound_in H = y and

A19: not E,h |= the_scope_of H by A12, A17, ZF_MODEL:16;

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

then A24: len (the_scope_of H) < len H by ZF_LANG:60;

for y being Variable st (f +* ((bound_in H),(h . (bound_in H)))) . y <> f . y holds

bound_in H = y by FUNCT_7:32;

then E,f +* ((bound_in H),(h . (bound_in H))) |= the_scope_of H by A4, A12, ZF_MODEL:16;

then E,f +* ((bound_in H),(h . (bound_in H))) |= All (x,(the_scope_of H)) by A1, A2, A13, A15, A24, TARSKI:def 1;

hence contradiction by A19, A20, ZF_MODEL:16; :: thesis: verum

end;assume not E,f |= All (x,H) ; :: thesis: contradiction

then consider g being Function of VAR,E such that

A16: for y being Variable st g . y <> f . y holds

x = y and

A17: not E,g |= H by ZF_MODEL:16;

consider h being Function of VAR,E such that

A18: for y being Variable st h . y <> g . y holds

bound_in H = y and

A19: not E,h |= the_scope_of H by A12, A17, ZF_MODEL:16;

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

A20: now :: thesis: for y being Variable st h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y holds

not x <> y

the_scope_of H is_immediate_constituent_of H
by A12;not x <> y

let y be Variable; :: thesis: ( h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y implies not x <> y )

assume A21: h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y ; :: thesis: not x <> y

assume x <> y ; :: thesis: contradiction

then A22: f . y = g . y by A16;

A23: y <> bound_in H by A21, FUNCT_7:128;

then (f +* ((bound_in H),(h . (bound_in H)))) . y = f . y by FUNCT_7:32;

hence contradiction by A18, A21, A23, A22; :: thesis: verum

end;assume A21: h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y ; :: thesis: not x <> y

assume x <> y ; :: thesis: contradiction

then A22: f . y = g . y by A16;

A23: y <> bound_in H by A21, FUNCT_7:128;

then (f +* ((bound_in H),(h . (bound_in H)))) . y = f . y by FUNCT_7:32;

hence contradiction by A18, A21, A23, A22; :: thesis: verum

then A24: len (the_scope_of H) < len H by ZF_LANG:60;

for y being Variable st (f +* ((bound_in H),(h . (bound_in H)))) . y <> f . y holds

bound_in H = y by FUNCT_7:32;

then E,f +* ((bound_in H),(h . (bound_in H))) |= the_scope_of H by A4, A12, ZF_MODEL:16;

then E,f +* ((bound_in H),(h . (bound_in H))) |= All (x,(the_scope_of H)) by A1, A2, A13, A15, A24, TARSKI:def 1;

hence contradiction by A19, A20, ZF_MODEL:16; :: thesis: verum

now :: thesis: ( x = bound_in H implies E,f |= All (x,H) )

hence
E,f |= All (x,H)
by A14; :: thesis: verumassume A25:
x = bound_in H
; :: thesis: E,f |= All (x,H)

hence E,f |= All (x,H) by A11, ZF_LANG:44; :: thesis: verum

end;now :: thesis: for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> f . y or x = y or bound_in H = y ) ) holds

E,g |= the_scope_of H

then
E,f |= All (x,(bound_in H),(the_scope_of H))
by ZF_MODEL:21;( not g . y <> f . y or x = y or bound_in H = y ) ) holds

E,g |= the_scope_of H

let g be Function of VAR,E; :: thesis: ( ( for y being Variable holds

( not g . y <> f . y or x = y or bound_in H = y ) ) implies E,g |= the_scope_of H )

assume for y being Variable holds

( not g . y <> f . y or x = y or bound_in H = y ) ; :: thesis: E,g |= the_scope_of H

then for y being Variable st g . y <> f . y holds

bound_in H = y by A25;

hence E,g |= the_scope_of H by A4, A12, ZF_MODEL:16; :: thesis: verum

end;( not g . y <> f . y or x = y or bound_in H = y ) ) implies E,g |= the_scope_of H )

assume for y being Variable holds

( not g . y <> f . y or x = y or bound_in H = y ) ; :: thesis: E,g |= the_scope_of H

then for y being Variable st g . y <> f . y holds

bound_in H = y by A25;

hence E,g |= the_scope_of H by A4, A12, ZF_MODEL:16; :: thesis: verum

hence E,f |= All (x,H) by A11, ZF_LANG:44; :: thesis: verum

A26: now :: thesis: ( H is conjunctive implies E,f |= All (x,H) )

assume A27:
H is conjunctive
; :: thesis: E,f |= All (x,H)

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

then the_right_argument_of H is_immediate_constituent_of H ;

then A29: len (the_right_argument_of H) < len H by ZF_LANG:60;

the_left_argument_of H is_immediate_constituent_of H by A28;

then A30: len (the_left_argument_of H) < len H by ZF_LANG:60;

A31: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A27, ZF_MODEL:1;

then A32: not x in Free (the_left_argument_of H) by A3, XBOOLE_0:def 3;

A33: not x in Free (the_right_argument_of H) by A3, A31, XBOOLE_0:def 3;

E,f |= the_right_argument_of H by A4, A28, ZF_MODEL:15;

then A34: E,f |= All (x,(the_right_argument_of H)) by A1, A2, A33, A29;

E,f |= the_left_argument_of H by A4, A28, ZF_MODEL:15;

then A35: E,f |= All (x,(the_left_argument_of H)) by A1, A2, A32, A30;

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

then the_right_argument_of H is_immediate_constituent_of H ;

then A29: len (the_right_argument_of H) < len H by ZF_LANG:60;

the_left_argument_of H is_immediate_constituent_of H by A28;

then A30: len (the_left_argument_of H) < len H by ZF_LANG:60;

A31: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A27, ZF_MODEL:1;

then A32: not x in Free (the_left_argument_of H) by A3, XBOOLE_0:def 3;

A33: not x in Free (the_right_argument_of H) by A3, A31, XBOOLE_0:def 3;

E,f |= the_right_argument_of H by A4, A28, ZF_MODEL:15;

then A34: E,f |= All (x,(the_right_argument_of H)) by A1, A2, A33, A29;

E,f |= the_left_argument_of H by A4, A28, ZF_MODEL:15;

then A35: E,f |= All (x,(the_left_argument_of H)) by A1, A2, A32, A30;

now :: 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

hence
E,f |= All (x,H)
by ZF_MODEL:16; :: thesis: verumx = 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 ( E,g |= the_left_argument_of H & E,g |= the_right_argument_of H ) by A35, A34, ZF_MODEL:16;

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

end;x = y ) implies E,g |= H )

assume for y being Variable st g . y <> f . y holds

x = y ; :: thesis: E,g |= H

then ( E,g |= the_left_argument_of H & E,g |= the_right_argument_of H ) by A35, A34, ZF_MODEL:16;

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

A36: now :: thesis: ( H is being_membership implies E,f |= All (x,H) )

assume A37:
H is being_membership
; :: thesis: E,f |= All (x,H)

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

then A38: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2;

A39: H = (Var1 H) 'in' (Var2 H) by A37, ZF_LANG:37;

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

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

then A38: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2;

A39: H = (Var1 H) 'in' (Var2 H) by A37, ZF_LANG:37;

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

now :: 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

hence
E,f |= All (x,H)
by ZF_MODEL:16; :: thesis: verumx = 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 . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A38;

hence E,g |= H by A39, A40, ZF_MODEL:13; :: thesis: verum

end;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 . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A38;

hence E,g |= H by A39, A40, ZF_MODEL:13; :: thesis: verum

now :: thesis: ( H is negative implies E,f |= All (x,H) )

hence
E,f |= All (x,H)
by A5, A36, A26, A10, ZF_LANG:9; :: thesis: verumassume A41:
H is negative
; :: thesis: E,f |= All (x,H)

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

then the_argument_of H is_immediate_constituent_of H ;

then A43: len (the_argument_of H) < len H by ZF_LANG:60;

A44: not x in Free (the_argument_of H) by A3, A41, ZF_MODEL:1;

assume not E,f |= All (x,H) ; :: thesis: contradiction

then consider g being Function of VAR,E such that

A45: for y being Variable st g . y <> f . y holds

x = y and

A46: not E,g |= H by ZF_MODEL:16;

E,g |= the_argument_of H by A42, A46, ZF_MODEL:14;

then E,g |= All (x,(the_argument_of H)) by A1, A2, A43, A44;

then E,f |= the_argument_of H by A45, ZF_MODEL:16;

hence contradiction by A4, A42, ZF_MODEL:14; :: thesis: verum

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

then the_argument_of H is_immediate_constituent_of H ;

then A43: len (the_argument_of H) < len H by ZF_LANG:60;

A44: not x in Free (the_argument_of H) by A3, A41, ZF_MODEL:1;

assume not E,f |= All (x,H) ; :: thesis: contradiction

then consider g being Function of VAR,E such that

A45: for y being Variable st g . y <> f . y holds

x = y and

A46: not E,g |= H by ZF_MODEL:16;

E,g |= the_argument_of H by A42, A46, ZF_MODEL:14;

then E,g |= All (x,(the_argument_of H)) by A1, A2, A43, A44;

then E,f |= the_argument_of H by A45, ZF_MODEL:16;

hence contradiction by A4, A42, ZF_MODEL:14; :: thesis: verum