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[ Element of 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 Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be
Element of
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 ) ) ) )
consider e being
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 <> {}
by CARD_1:47, NAT_1:5;
then reconsider x =
e as
Variable by TARSKI:def 3;
A5:
{x} c= Free H
by A4, ZFMISC_1:37;
A6:
Free (All x,H) = (Free H) \ {x}
by ZF_LANG1:67;
x in {x}
by ZFMISC_1:37;
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:54;
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:25;
hence
(
M |= S iff
M |= H )
by A9;
verum
end;
A10:
card (Free H) = card (Free H)
;
A11:
S2[ 0 ]
for i being Element of NAT holds S2[i]
from NAT_1:sch 1(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