let H be ZF-formula; :: thesis: ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

defpred S_{2}[ Nat] means for H being ZF-formula st card (Free H) = $1 holds

ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) );

A1: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]

A11: S_{2}[ 0 ]
_{2}[i]
from NAT_1:sch 2(A11, A1);

hence ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) ) by A10; :: thesis: verum

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

defpred S

ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) );

A1: for i being Nat st S

S

proof

A10:
card (Free H) = card (Free H)
;
let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A2: S_{2}[i]
; :: thesis: S_{2}[i + 1]

let H be ZF-formula; :: thesis: ( card (Free H) = i + 1 implies ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) ) )

set e = the Element of Free H;

assume A3: card (Free H) = i + 1 ; :: thesis: ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

then A4: Free H <> {} ;

then reconsider x = the Element of Free H as Variable by TARSKI:def 3;

A5: {x} c= Free H by A4, ZFMISC_1:31;

A6: Free (All (x,H)) = (Free H) \ {x} by ZF_LANG1:62;

x in {x} by ZFMISC_1:31;

then A7: not x in Free (All (x,H)) by A6, XBOOLE_0:def 5;

(Free (All (x,H))) \/ {x} = (Free H) \/ {x} by A6, XBOOLE_1:39;

then (Free (All (x,H))) \/ {x} = Free H by A5, XBOOLE_1:12;

then (card (Free (All (x,H)))) + 1 = card (Free H) by A7, CARD_2:41;

then consider S being ZF-formula such that

A8: Free S = {} and

A9: for M being non empty set holds

( M |= S iff M |= All (x,H) ) by A2, A3, XCMPLX_1:2;

take S ; :: thesis: ( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

thus Free S = {} by A8; :: thesis: for M being non empty set holds

( M |= S iff M |= H )

let M be non empty set ; :: thesis: ( M |= S iff M |= H )

( M |= H iff M |= All (x,H) ) by ZF_MODEL:23;

hence ( M |= S iff M |= H ) by A9; :: thesis: verum

end;assume A2: S

let H be ZF-formula; :: thesis: ( card (Free H) = i + 1 implies ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) ) )

set e = the Element of Free H;

assume A3: card (Free H) = i + 1 ; :: thesis: ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

then A4: Free H <> {} ;

then reconsider x = the Element of Free H as Variable by TARSKI:def 3;

A5: {x} c= Free H by A4, ZFMISC_1:31;

A6: Free (All (x,H)) = (Free H) \ {x} by ZF_LANG1:62;

x in {x} by ZFMISC_1:31;

then A7: not x in Free (All (x,H)) by A6, XBOOLE_0:def 5;

(Free (All (x,H))) \/ {x} = (Free H) \/ {x} by A6, XBOOLE_1:39;

then (Free (All (x,H))) \/ {x} = Free H by A5, XBOOLE_1:12;

then (card (Free (All (x,H)))) + 1 = card (Free H) by A7, CARD_2:41;

then consider S being ZF-formula such that

A8: Free S = {} and

A9: for M being non empty set holds

( M |= S iff M |= All (x,H) ) by A2, A3, XCMPLX_1:2;

take S ; :: thesis: ( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

thus Free S = {} by A8; :: thesis: for M being non empty set holds

( M |= S iff M |= H )

let M be non empty set ; :: thesis: ( M |= S iff M |= H )

( M |= H iff M |= All (x,H) ) by ZF_MODEL:23;

hence ( M |= S iff M |= H ) by A9; :: thesis: verum

A11: S

proof

for i being Nat holds S
let H be ZF-formula; :: thesis: ( card (Free H) = 0 implies ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) ) )

assume A12: card (Free H) = 0 ; :: thesis: ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

take H ; :: thesis: ( Free H = {} & ( for M being non empty set holds

( M |= H iff M |= H ) ) )

thus ( Free H = {} & ( for M being non empty set holds

( M |= H iff M |= H ) ) ) by A12; :: thesis: verum

end;( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) ) )

assume A12: card (Free H) = 0 ; :: thesis: ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

take H ; :: thesis: ( Free H = {} & ( for M being non empty set holds

( M |= H iff M |= H ) ) )

thus ( Free H = {} & ( for M being non empty set holds

( M |= H iff M |= H ) ) ) by A12; :: thesis: verum

hence ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) ) by A10; :: thesis: verum