let H be ZF-formula; ex S being ZF-formula st
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
defpred S2[ 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 S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A2:
S2[
i]
;
S2[i + 1]
let H be
ZF-formula;
( 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
;
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
;
( Free S = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) )
thus
Free S = {}
by A8;
for M being non empty set holds
( M |= S iff M |= H )
let M be non
empty set ;
( M |= S iff M |= H )
(
M |= H iff
M |= All (
x,
H) )
by ZF_MODEL:23;
hence
(
M |= S iff
M |= H )
by A9;
verum
end;
A10:
card (Free H) = card (Free H)
;
A11:
S2[ 0 ]
for i being Nat holds S2[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; verum