let H be ZF-formula; :: thesis: ( ex i being Element of NAT st

for j being Element of NAT st x. j in variables_in H holds

j < i & not for x being Variable holds x in variables_in H )

defpred S_{1}[ ZF-formula] means ex i being Element of NAT st

for j being Element of NAT st x. j in variables_in $1 holds

j < i;

A1: for x, y being Variable holds

( S_{1}[x '=' y] & S_{1}[x 'in' y] )
_{1}[H1] & S_{1}[H2] holds

S_{1}[H1 '&' H2]

for x being Variable st S_{1}[H] holds

S_{1}[ All (x,H)]
_{1}[H] holds

S_{1}[ 'not' H]
_{1}[H]
from ZF_LANG1:sch 1(A1, A16, A8, A12);

then consider i being Element of NAT such that

A17: for j being Element of NAT st x. j in variables_in H holds

j < i ;

thus ex i being Element of NAT st

for j being Element of NAT st x. j in variables_in H holds

j < i by A17; :: thesis: not for x being Variable holds x in variables_in H

take x. i ; :: thesis: not x. i in variables_in H

thus not x. i in variables_in H by A17; :: thesis: verum

for j being Element of NAT st x. j in variables_in H holds

j < i & not for x being Variable holds x in variables_in H )

defpred S

for j being Element of NAT st x. j in variables_in $1 holds

j < i;

A1: for x, y being Variable holds

( S

proof

A8:
for H1, H2 being ZF-formula st S
let x, y be Variable; :: thesis: ( S_{1}[x '=' y] & S_{1}[x 'in' y] )

consider i being Element of NAT such that

A2: x = x. i by ZF_LANG1:77;

consider j being Element of NAT such that

A3: y = x. j by ZF_LANG1:77;

j <= j + i by NAT_1:11;

then A4: j < (i + j) + 1 by NAT_1:13;

i <= i + j by NAT_1:11;

then A5: i < (i + j) + 1 by NAT_1:13;

A6: variables_in (x '=' y) = {x,y} by ZF_LANG1:138;

thus S_{1}[x '=' y]
:: thesis: S_{1}[x 'in' y]

j < (i + j) + 1

let k be Element of NAT ; :: thesis: ( x. k in variables_in (x 'in' y) implies k < (i + j) + 1 )

A7: variables_in (x 'in' y) = {x,y} by ZF_LANG1:139;

assume x. k in variables_in (x 'in' y) ; :: thesis: k < (i + j) + 1

then ( x. k = x. i or x. k = x. j ) by A2, A3, A7, TARSKI:def 2;

hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; :: thesis: verum

end;consider i being Element of NAT such that

A2: x = x. i by ZF_LANG1:77;

consider j being Element of NAT such that

A3: y = x. j by ZF_LANG1:77;

j <= j + i by NAT_1:11;

then A4: j < (i + j) + 1 by NAT_1:13;

i <= i + j by NAT_1:11;

then A5: i < (i + j) + 1 by NAT_1:13;

A6: variables_in (x '=' y) = {x,y} by ZF_LANG1:138;

thus S

proof

take
(i + j) + 1
; :: thesis: for j being Element of NAT st x. j in variables_in (x 'in' y) holds
take
(i + j) + 1
; :: thesis: for j being Element of NAT st x. j in variables_in (x '=' y) holds

j < (i + j) + 1

let k be Element of NAT ; :: thesis: ( x. k in variables_in (x '=' y) implies k < (i + j) + 1 )

assume x. k in variables_in (x '=' y) ; :: thesis: k < (i + j) + 1

then ( x. k = x. i or x. k = x. j ) by A2, A3, A6, TARSKI:def 2;

hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; :: thesis: verum

end;j < (i + j) + 1

let k be Element of NAT ; :: thesis: ( x. k in variables_in (x '=' y) implies k < (i + j) + 1 )

assume x. k in variables_in (x '=' y) ; :: thesis: k < (i + j) + 1

then ( x. k = x. i or x. k = x. j ) by A2, A3, A6, TARSKI:def 2;

hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; :: thesis: verum

j < (i + j) + 1

let k be Element of NAT ; :: thesis: ( x. k in variables_in (x 'in' y) implies k < (i + j) + 1 )

A7: variables_in (x 'in' y) = {x,y} by ZF_LANG1:139;

assume x. k in variables_in (x 'in' y) ; :: thesis: k < (i + j) + 1

then ( x. k = x. i or x. k = x. j ) by A2, A3, A7, TARSKI:def 2;

hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; :: thesis: verum

S

proof

A12:
for H being ZF-formula
let H1, H2 be ZF-formula; :: thesis: ( S_{1}[H1] & S_{1}[H2] implies S_{1}[H1 '&' H2] )

given i1 being Element of NAT such that A9: for j being Element of NAT st x. j in variables_in H1 holds

j < i1 ; :: thesis: ( not S_{1}[H2] or S_{1}[H1 '&' H2] )

given i2 being Element of NAT such that A10: for j being Element of NAT st x. j in variables_in H2 holds

j < i2 ; :: thesis: S_{1}[H1 '&' H2]

( i1 <= i2 or i1 > i2 ) ;

then consider i being Element of NAT such that

A11: ( ( i1 <= i2 & i = i2 ) or ( i1 > i2 & i = i1 ) ) ;

take i ; :: thesis: for j being Element of NAT st x. j in variables_in (H1 '&' H2) holds

j < i

let j be Element of NAT ; :: thesis: ( x. j in variables_in (H1 '&' H2) implies j < i )

assume x. j in variables_in (H1 '&' H2) ; :: thesis: j < i

then x. j in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;

then ( x. j in variables_in H1 or x. j in variables_in H2 ) by XBOOLE_0:def 3;

then ( j < i1 or j < i2 ) by A9, A10;

hence j < i by A11, XXREAL_0:2; :: thesis: verum

end;given i1 being Element of NAT such that A9: for j being Element of NAT st x. j in variables_in H1 holds

j < i1 ; :: thesis: ( not S

given i2 being Element of NAT such that A10: for j being Element of NAT st x. j in variables_in H2 holds

j < i2 ; :: thesis: S

( i1 <= i2 or i1 > i2 ) ;

then consider i being Element of NAT such that

A11: ( ( i1 <= i2 & i = i2 ) or ( i1 > i2 & i = i1 ) ) ;

take i ; :: thesis: for j being Element of NAT st x. j in variables_in (H1 '&' H2) holds

j < i

let j be Element of NAT ; :: thesis: ( x. j in variables_in (H1 '&' H2) implies j < i )

assume x. j in variables_in (H1 '&' H2) ; :: thesis: j < i

then x. j in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;

then ( x. j in variables_in H1 or x. j in variables_in H2 ) by XBOOLE_0:def 3;

then ( j < i1 or j < i2 ) by A9, A10;

hence j < i by A11, XXREAL_0:2; :: thesis: verum

for x being Variable st S

S

proof

A16:
for H being ZF-formula st S
let H be ZF-formula; :: thesis: for x being Variable st S_{1}[H] holds

S_{1}[ All (x,H)]

let x be Variable; :: thesis: ( S_{1}[H] implies S_{1}[ All (x,H)] )

given i1 being Element of NAT such that A13: for j being Element of NAT st x. j in variables_in H holds

j < i1 ; :: thesis: S_{1}[ All (x,H)]

consider i2 being Element of NAT such that

A14: x = x. i2 by ZF_LANG1:77;

( i1 <= i2 + 1 or i1 > i2 + 1 ) ;

then consider i being Element of NAT such that

A15: ( ( i1 <= i2 + 1 & i = i2 + 1 ) or ( i1 > i2 + 1 & i = i1 ) ) ;

take i ; :: thesis: for j being Element of NAT st x. j in variables_in (All (x,H)) holds

j < i

let j be Element of NAT ; :: thesis: ( x. j in variables_in (All (x,H)) implies j < i )

assume x. j in variables_in (All (x,H)) ; :: thesis: j < i

then x. j in (variables_in H) \/ {x} by ZF_LANG1:142;

then ( x. j in variables_in H or ( x. j in {x} & i2 + 0 = i2 & 0 < 1 ) ) by XBOOLE_0:def 3;

then ( j < i1 or ( x. j = x. i2 & i2 < i2 + 1 ) ) by A13, A14, TARSKI:def 1, XREAL_1:6;

then ( j < i1 or j < i2 + 1 ) by ZF_LANG1:76;

hence j < i by A15, XXREAL_0:2; :: thesis: verum

end;S

let x be Variable; :: thesis: ( S

given i1 being Element of NAT such that A13: for j being Element of NAT st x. j in variables_in H holds

j < i1 ; :: thesis: S

consider i2 being Element of NAT such that

A14: x = x. i2 by ZF_LANG1:77;

( i1 <= i2 + 1 or i1 > i2 + 1 ) ;

then consider i being Element of NAT such that

A15: ( ( i1 <= i2 + 1 & i = i2 + 1 ) or ( i1 > i2 + 1 & i = i1 ) ) ;

take i ; :: thesis: for j being Element of NAT st x. j in variables_in (All (x,H)) holds

j < i

let j be Element of NAT ; :: thesis: ( x. j in variables_in (All (x,H)) implies j < i )

assume x. j in variables_in (All (x,H)) ; :: thesis: j < i

then x. j in (variables_in H) \/ {x} by ZF_LANG1:142;

then ( x. j in variables_in H or ( x. j in {x} & i2 + 0 = i2 & 0 < 1 ) ) by XBOOLE_0:def 3;

then ( j < i1 or ( x. j = x. i2 & i2 < i2 + 1 ) ) by A13, A14, TARSKI:def 1, XREAL_1:6;

then ( j < i1 or j < i2 + 1 ) by ZF_LANG1:76;

hence j < i by A15, XXREAL_0:2; :: thesis: verum

S

proof

for H being ZF-formula holds S
let H be ZF-formula; :: thesis: ( S_{1}[H] implies S_{1}[ 'not' H] )

variables_in ('not' H) = variables_in H by ZF_LANG1:140;

hence ( S_{1}[H] implies S_{1}[ 'not' H] )
; :: thesis: verum

end;variables_in ('not' H) = variables_in H by ZF_LANG1:140;

hence ( S

then consider i being Element of NAT such that

A17: for j being Element of NAT st x. j in variables_in H holds

j < i ;

thus ex i being Element of NAT st

for j being Element of NAT st x. j in variables_in H holds

j < i by A17; :: thesis: not for x being Variable holds x in variables_in H

take x. i ; :: thesis: not x. i in variables_in H

thus not x. i in variables_in H by A17; :: thesis: verum