:: A Model of ZF Set Theory Language
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, TARSKI, ARYTM_3,
CARD_1, ORDINAL4, FUNCT_1, XBOOLEAN, BVFUNC_2, RELAT_1, CLASSES2, NAT_1,
ARYTM_1, ZF_LANG, ORDINAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ORDINAL1,
NAT_1, NUMBERS, FINSEQ_1, XXREAL_0, TREES_3;
constructors XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, NUMBERS, TREES_3;
registrations ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, CARD_1, XBOOLE_0, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, FUNCT_1, NAT_1, FINSEQ_1, XBOOLE_0, XREAL_1, XXREAL_0,
ORDINAL1;
schemes NAT_1, XFAMILY;
begin
reserve k,m,n for Element of NAT,
a,X,Y for set,
D,D1,D2 for non empty set;
reserve p,q for FinSequence of NAT;
::
:: The Construction of ZF Set Theory Language
::
:: The set and the mode of ZF-language variables
definition
func VAR -> Subset of NAT equals
{ k : 5 <= k };
coherence
proof
set X = { k : 5 <= k };
X c= NAT
proof
let a be object;
assume a in X;
then ex k st a = k & 5 <= k;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster VAR -> non empty;
coherence
proof
5 in { k : 5 <= k };
hence thesis;
end;
end;
definition
mode Variable is Element of VAR;
end;
definition
let n;
func x.n -> Variable equals
5 + n;
coherence
proof
set x = 5 + n;
5 <= x by NAT_1:11;
then x in { k : 5 <= k };
hence thesis;
end;
end;
reserve x,y,z,t for Variable;
:: The operations to make ZF-formulae
registration
cluster -> natural for Variable;
coherence;
end;
definition
let x,y;
func x '=' y -> FinSequence of NAT equals
<*0*>^<*x*>^<*y*>;
coherence;
func x 'in' y -> FinSequence of NAT equals
<*1*>^<*x*>^<*y*>;
coherence;
end;
theorem
x '=' y = z '=' t implies x = z & y = t
proof
A1: <*0*>^<*x*>^<*y*> = <*0*>^(<*x*>^<*y*>) & <*0*>^<*z*>^<*t*> = <*0*>^(<*z
*>^ <*t*>) by FINSEQ_1:32;
A2: <*x,y*>.1 = x & <*x,y*>.2 = y;
A3: <*x*>^<*y*> = <*x,y*> & <*z*>^<*t*> = <*z,t*> by FINSEQ_1:def 9;
A4: <*z,t*>.1 = z & <*z,t*>.2 = t;
assume x '=' y = z '=' t;
hence thesis by A1,A2,A4,A3,FINSEQ_1:33;
end;
theorem
x 'in' y = z 'in' t implies x = z & y = t
proof
A1: <*1*>^<*x*>^<*y*> = <*1*>^(<*x*>^<*y*>) & <*1*>^<*z*>^<*t*> = <*1*>^(<*z
*>^ <*t*>) by FINSEQ_1:32;
A2: <*x,y*>.1 = x & <*x,y*>.2 = y;
A3: <*x*>^<*y*> = <*x,y*> & <*z*>^<*t*> = <*z,t*> by FINSEQ_1:def 9;
A4: <*z,t*>.1 = z & <*z,t*>.2 = t;
assume x 'in' y = z 'in' t;
hence thesis by A1,A2,A4,A3,FINSEQ_1:33;
end;
definition
let p;
func 'not' p -> FinSequence of NAT equals
<*2*>^p;
coherence;
let q;
func p '&' q -> FinSequence of NAT equals
<*3*>^p^q;
coherence;
end;
definition
let x,p;
func All(x,p)-> FinSequence of NAT equals
<*4*>^<*x*>^p;
coherence;
end;
theorem Th3:
All(x,p) = All(y,q) implies x = y & p = q
proof
A1: <*4*>^<*x*>^p = <*4*>^(<*x*>^p) & <*4*>^<*y*>^q = <*4*>^(<*y*>^q) by
FINSEQ_1:32;
A2: (<*x*>^p).1 = x & (<*y*>^q).1 = y by FINSEQ_1:41;
assume
A3: All(x,p) = All(y,q);
hence x = y by A1,A2,FINSEQ_1:33;
<*x*>^p = <*y*>^q by A3,A1,FINSEQ_1:33;
hence thesis by A2,FINSEQ_1:33;
end;
:: The set of all well formed formulae of ZF-language
definition
func WFF -> non empty set means
:Def8:
(for a st a in it holds a is
FinSequence of NAT ) & (for x,y holds x '=' y in it & x 'in' y in it ) & (for p
st p in it holds 'not' p in it ) & (for p,q st p in it & q in it holds p '&' q
in it ) & (for x,p st p in it holds All(x,p) in it ) & for D st (for a st a in
D holds a is FinSequence of NAT ) & (for x,y holds x '=' y in D & x 'in' y in D
) & (for p st p in D holds 'not' p in D ) & (for p,q st p in D & q in D holds p
'&' q in D ) & (for x,p st p in D holds All(x,p) in D ) holds it c= D;
existence
proof
defpred P[set] means (for a st a in $1 holds a is FinSequence of NAT ) & (
for x,y holds x '=' y in $1 & x 'in' y in $1 ) & (for p st p in $1 holds 'not'
p in $1 ) & (for p,q st p in $1 & q in $1 holds p '&' q in $1 ) & (for x,p st p
in $1 holds All(x,p) in $1 );
defpred Y[set] means for D st P[D] holds $1 in D;
consider Y such that
A1: a in Y iff a in NAT* & Y[a] from XFAMILY:sch 1;
now
set a = x.0 '=' x.0;
take b = a;
a in NAT* & for D st P[D] holds a in D by FINSEQ_1:def 11;
hence b in Y by A1;
end;
then reconsider Y as non empty set;
take Y;
thus a in Y implies a is FinSequence of NAT
proof
assume a in Y;
then a in NAT* by A1;
hence thesis by FINSEQ_1:def 11;
end;
thus x '=' y in Y & x 'in' y in Y
proof
x '=' y in NAT* & for D st P[D] holds x '=' y in D by FINSEQ_1:def 11;
hence x '=' y in Y by A1;
x 'in' y in NAT* & for D st P[D] holds x 'in' y in D by FINSEQ_1:def 11;
hence thesis by A1;
end;
thus p in Y implies 'not' p in Y
proof
assume
A2: p in Y;
A3: for D st P[D] holds 'not' p in D
proof
let D;
assume
A4: P[D];
then p in D by A1,A2;
hence thesis by A4;
end;
'not' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A3;
end;
thus for q,p holds q in Y & p in Y implies q '&' p in Y
proof
let q,p;
assume
A5: q in Y & p in Y;
A6: for D st P[D] holds q '&' p in D
proof
let D;
assume
A7: P[D];
then p in D & q in D by A1,A5;
hence thesis by A7;
end;
q '&' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A6;
end;
thus for x,p st p in Y holds All(x,p) in Y
proof
let x,p such that
A8: p in Y;
A9: for D st P[D] holds All(x,p) in D
proof
let D;
assume
A10: P[D];
then p in D by A1,A8;
hence thesis by A10;
end;
All(x,p) in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A9;
end;
let D such that
A11: P[D];
let a be object;
assume a in Y;
hence thesis by A1,A11;
end;
uniqueness
proof
let D1,D2;
assume ( ( for a st a in D1 holds a is FinSequence of NAT)& for x,y
holds x '=' y in D1 & x 'in' y in D1 )&( ( for p st p in D1 holds 'not' p in D1
)& for p,q st p in D1 & q in D1 holds p '&' q in D1 ) & ( for x,p st p in D1
holds All(x,p) in D1)&( ( for D st (for a st a in D holds a is FinSequence of
NAT ) & (for x, y holds x '=' y in D & x 'in' y in D ) & ( for p st p in D
holds 'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for
x,p st p in D holds All (x,p) in D ) holds D1 c= D)& for a st a in D2 holds a
is FinSequence of NAT ) &( ( ( for x,y holds x '=' y in D2 & x 'in' y in D2)&
for p st p in D2 holds 'not' p in D2 )&( ( for p,q st p in D2 & q in D2 holds p
'&' q in D2)& for x,p st p in D2 holds All(x,p) in D2 ) & for D st (for a st a
in D holds a is FinSequence of NAT ) & (for x, y holds x '=' y in D & x 'in' y
in D ) & (for p st p in D holds 'not' p in D ) & (for p,q st p in D & q in D
holds p '&' q in D ) & (for x,p st p in D holds All(x,p) in D ) holds D2 c= D )
;
then D1 c= D2 & D2 c= D1;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition
let IT be FinSequence of NAT;
attr IT is ZF-formula-like means
:Def9:
IT is Element of WFF;
end;
registration
cluster ZF-formula-like for FinSequence of NAT;
existence
proof
set x = the Element of WFF;
reconsider x as FinSequence of NAT by Def8;
take x;
thus x is Element of WFF;
end;
end;
definition
mode ZF-formula is ZF-formula-like FinSequence of NAT;
end;
theorem
a is ZF-formula iff a in WFF
proof
thus a is ZF-formula implies a in WFF
proof
assume a is ZF-formula;
then a is Element of WFF by Def9;
hence thesis;
end;
assume a in WFF;
hence thesis by Def8,Def9;
end;
reserve F,F1,G,G1,H,H1 for ZF-formula;
registration
let x,y;
cluster x '=' y -> ZF-formula-like;
coherence
by Def8;
cluster x 'in' y -> ZF-formula-like;
coherence
by Def8;
end;
registration
let H;
cluster 'not' H -> ZF-formula-like;
coherence
proof
H is Element of WFF by Def9;
then 'not' H is Element of WFF by Def8;
hence thesis;
end;
let G;
cluster H '&' G -> ZF-formula-like;
coherence
proof
H is Element of WFF & G is Element of WFF by Def9;
then H '&' G is Element of WFF by Def8;
hence thesis;
end;
end;
registration
let x,H;
cluster All(x,H) -> ZF-formula-like;
coherence
proof
H is Element of WFF by Def9;
then All(x,H) is Element of WFF by Def8;
hence thesis;
end;
end;
::
:: The Properties of ZF-formulae
::
definition
let H;
attr H is being_equality means
ex x,y st H = x '=' y;
attr H is being_membership means
ex x,y st H = x 'in' y;
attr H is negative means
ex H1 st H = 'not' H1;
attr H is conjunctive means
ex F,G st H = F '&' G;
attr H is universal means
ex x,H1 st H = All(x,H1);
end;
theorem
(H is being_equality iff ex x,y st H = x '=' y) & (H is
being_membership iff ex x,y st H = x 'in' y) & (H is negative iff ex H1 st H =
'not' H1) & (H is conjunctive iff ex F,G st H = F '&' G) & (H is universal iff
ex x,H1 st H = All(x,H1) );
definition
let H;
attr H is atomic means
H is being_equality or H is being_membership;
end;
definition
let F,G;
func F 'or' G -> ZF-formula equals
'not'('not' F '&' 'not' G);
coherence;
func F => G -> ZF-formula equals
'not' (F '&' 'not' G);
coherence;
end;
definition
let F,G;
func F <=> G -> ZF-formula equals
(F => G) '&' (G => F);
coherence;
end;
definition
let x,H;
func Ex(x,H) -> ZF-formula equals
'not' All(x,'not' H);
coherence;
end;
definition
let H;
attr H is disjunctive means
ex F,G st H = F 'or' G;
attr H is conditional means
ex F,G st H = F => G;
attr H is biconditional means
ex F,G st H = F <=> G;
attr H is existential means
ex x,H1 st H = Ex(x,H1);
end;
theorem
(H is disjunctive iff ex F,G st H = F 'or' G) & (H is conditional iff
ex F,G st H = F => G) & (H is biconditional iff ex F,G st H = F <=> G) & (H is
existential iff ex x,H1 st H = Ex(x,H1) );
definition
let x,y,H;
func All(x,y,H) -> ZF-formula equals
All(x,All(y,H));
coherence;
func Ex(x,y,H) -> ZF-formula equals
Ex(x,Ex(y,H));
coherence;
end;
theorem
All(x,y,H) = All(x,All(y,H)) & Ex(x,y,H) = Ex(x,Ex(y,H));
definition
let x,y,z,H;
func All(x,y,z,H) -> ZF-formula equals
All(x,All(y,z,H));
coherence;
func Ex(x,y,z,H) -> ZF-formula equals
Ex(x,Ex(y,z,H));
coherence;
end;
theorem
All(x,y,z,H) = All(x,All(y,z,H)) & Ex(x,y,z,H) = Ex(x,Ex(y,z,H));
theorem Th9:
H is being_equality or H is being_membership or H is negative or
H is conjunctive or H is universal
proof
A1: H is Element of WFF by Def9;
assume
A2: not thesis;
then x.0 '=' x.1 <> H;
then
A3: not x.0 '=' x.1 in { H } by TARSKI:def 1;
A4: now
let x,y;
x '=' y <> H by A2;
then
A5: not x '=' y in { H } by TARSKI:def 1;
x '=' y in WFF by Def8;
hence x '=' y in WFF \ { H } by A5,XBOOLE_0:def 5;
x 'in' y <> H by A2;
then
A6: not x 'in' y in { H } by TARSKI:def 1;
x 'in' y in WFF by Def8;
hence x 'in' y in WFF \ { H } by A6,XBOOLE_0:def 5;
end;
A7: now
let x,p;
assume
A8: p in WFF \ { H };
then reconsider H1 = p as ZF-formula by Def9;
All(x,H1) <> H by A2;
then
A9: not All(x,p) in { H } by TARSKI:def 1;
All(x,p) in WFF by A8,Def8;
hence All(x,p) in WFF \ { H } by A9,XBOOLE_0:def 5;
end;
A10: now
let p,q;
assume
A11: p in WFF \ { H } & q in WFF \ { H };
then reconsider F = p, G = q as ZF-formula by Def9;
F '&' G <> H by A2;
then
A12: not p '&' q in { H } by TARSKI:def 1;
p '&' q in WFF by A11,Def8;
hence p '&' q in WFF \ { H } by A12,XBOOLE_0:def 5;
end;
A13: now
let p;
assume
A14: p in WFF \ { H };
then reconsider H1 = p as ZF-formula by Def9;
'not' H1 <> H by A2;
then
A15: not 'not' p in { H } by TARSKI:def 1;
'not' p in WFF by A14,Def8;
hence 'not' p in WFF \ { H } by A15,XBOOLE_0:def 5;
end;
x.0 '=' x.1 in WFF by Def8;
then
A16: WFF \ { H } is non empty set by A3,XBOOLE_0:def 5;
for a st a in WFF \ { H } holds a is FinSequence of NAT by Def8;
then WFF c= WFF \ { H } by A16,A4,A13,A10,A7,Def8;
then H in WFF \ { H } by A1;
then not H in { H } by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
theorem Th10:
H is atomic or H is negative or H is conjunctive or H is universal
by Th9;
theorem Th11:
H is atomic implies len H = 3
proof
A1: now
assume H is being_equality;
then consider x,y such that
A2: H = x '=' y;
H = <* 0,x,y *> by A2,FINSEQ_1:def 10;
hence thesis by FINSEQ_1:45;
end;
A3: now
assume H is being_membership;
then consider x,y such that
A4: H = x 'in' y;
H = <* 1,x,y *> by A4,FINSEQ_1:def 10;
hence thesis by FINSEQ_1:45;
end;
assume H is atomic;
hence thesis by A1,A3;
end;
theorem Th12:
H is atomic or ex H1 st len H1 + 1 <= len H
proof
A1: now
let H;
assume H is universal;
then consider x,H1 such that
A2: H = All(x,H1);
take H1;
A3: len <*4,x*> = 2 & <*4*>^<*x*> =<*4,x*> by FINSEQ_1:44,def 9;
A4: 1 + 1 + len H1 = 1 + (1 + len H1);
len H = len(<*4*>^<*x*>) + len H1 by A2,FINSEQ_1:22;
hence len H1 + 1 <= len H by A3,A4,NAT_1:11;
end;
A5: now
let H;
assume H is negative;
then consider H1 such that
A6: H = 'not' H1;
take H1;
len H = len <*2*> + len H1 by A6,FINSEQ_1:22;
hence len H1 + 1 <= len H by FINSEQ_1:40;
end;
A7: now
let H;
assume H is conjunctive;
then consider H1,F1 such that
A8: H = H1 '&' F1;
take H1;
A9: len(<*3*>^H1) = len <*3*> + len H1 & len <*3*> = 1 by FINSEQ_1:22,40;
len H = len(<*3*>^H1) + len F1 by A8,FINSEQ_1:22;
hence len H1 + 1 <= len H by A9,NAT_1:11;
end;
assume not H is atomic;
then H is negative or H is conjunctive or H is universal by Th10;
hence thesis by A5,A7,A1;
end;
theorem Th13:
3 <= len H
proof
now
assume not H is atomic;
then consider H1 such that
A1: len H1 + 1 <= len H by Th12;
A2: now
assume not H1 is atomic;
then consider F such that
A3: len F + 1 <= len H1 by Th12;
A4: now
assume not F is atomic;
then consider F1 such that
A5: len F1 + 1 <= len F by Th12;
0 + 1 <= len F1 + 1 by XREAL_1:7;
then 1 <= len F by A5,XXREAL_0:2;
then 1 + 1 <= len F + 1 by XREAL_1:7;
then 2 <= len H1 by A3,XXREAL_0:2;
then 2 + 1 <= len H1 + 1 by XREAL_1:7;
hence thesis by A1,XXREAL_0:2;
end;
A6: len F + 1 + 1 <= len H1 + 1 by A3,XREAL_1:7;
now
assume F is atomic;
then len F = 3 by Th11;
then 3 + 1 + 1 <= len H by A1,A6,XXREAL_0:2;
hence thesis by XXREAL_0:2;
end;
hence thesis by A4;
end;
now
assume H1 is atomic;
then 3 + 1 <= len H by A1,Th11;
hence thesis by XXREAL_0:2;
end;
hence thesis by A2;
end;
hence thesis by Th11;
end;
theorem
len H = 3 implies H is atomic
proof
assume
A1: len H = 3;
assume not H is atomic;
then consider H1 such that
A2: len H1 + 1 <= len H by Th12;
3 <= len H1 by Th13;
then 3 + 1 <= len H1 + 1 by XREAL_1:7;
hence contradiction by A1,A2,XXREAL_0:2;
end;
theorem Th15:
for x,y holds (x '=' y).1 = 0 & (x 'in' y ).1 = 1
proof
let x,y;
thus (x '=' y).1 = (<*0*>^(<*x*>^<*y*>)).1 by FINSEQ_1:32
.= 0 by FINSEQ_1:41;
thus (x 'in' y).1 = (<*1*>^(<*x*>^<*y*>)).1 by FINSEQ_1:32
.= 1 by FINSEQ_1:41;
end;
theorem Th16:
for F,G holds (F '&' G).1 = 3
proof
let F,G;
thus (F '&' G).1 = (<*3*>^(F^G)).1 by FINSEQ_1:32
.= 3 by FINSEQ_1:41;
end;
theorem Th17:
for x,H holds All(x,H).1 = 4
proof
let x,H;
thus All(x,H).1 = (<*4*>^(<*x*>^H)).1 by FINSEQ_1:32
.= 4 by FINSEQ_1:41;
end;
theorem Th18:
H is being_equality implies H.1 = 0
proof
assume H is being_equality;
then consider x,y such that
A1: H = x '=' y;
H = <* 0,x,y *> by A1,FINSEQ_1:def 10;
hence thesis;
end;
theorem Th19:
H is being_membership implies H.1 = 1
proof
assume H is being_membership;
then consider x,y such that
A1: H = x 'in' y;
H = <* 1,x,y *> by A1,FINSEQ_1:def 10;
hence thesis;
end;
theorem Th20:
H is negative implies H.1 = 2
by FINSEQ_1:41;
theorem Th21:
H is conjunctive implies H.1 = 3
proof
assume H is conjunctive;
then consider F,G such that
A1: H = F '&' G;
<*3*>^F^G = <*3*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
theorem Th22:
H is universal implies H.1 = 4
proof
assume H is universal;
then consider x,H1 such that
A1: H = All(x,H1);
<*4*>^<*x*>^H1 = <*4*>^(<*x*>^H1) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
theorem Th23:
H is being_equality & H.1 = 0 or H is being_membership & H.1 = 1
or H is negative & H.1 = 2 or H is conjunctive & H.1 = 3 or H is universal & H.
1 = 4
proof
per cases by Th9;
case
H is being_equality;
hence thesis by Th18;
end;
case
H is being_membership;
hence thesis by Th19;
end;
case
H is negative;
hence thesis by Th20;
end;
case
H is conjunctive;
hence thesis by Th21;
end;
case
H is universal;
hence thesis by Th22;
end;
end;
theorem
H.1 = 0 implies H is being_equality by Th23;
theorem
H.1 = 1 implies H is being_membership by Th23;
theorem
H.1 = 2 implies H is negative by Th23;
theorem
H.1 = 3 implies H is conjunctive by Th23;
theorem
H.1 = 4 implies H is universal by Th23;
reserve sq,sq9 for FinSequence;
theorem Th29:
H = F^sq implies H = F
proof
defpred P[Nat] means for H,F,sq st len H = $1 & H = F^sq holds H = F;
for n being Nat st for k being Nat st k < n for H,F,sq st len H = k & H
= F^sq holds H = F for H,F,sq st len H = n & H = F^sq holds H = F
proof
let n be Nat such that
A1: for k be Nat st k < n for H,F,sq st len H = k & H = F^sq holds H = F;
let H,F,sq such that
A2: len H = n and
A3: H = F^sq;
3 <= len F by Th13;
then dom F = Seg len F & 1 <= len F by FINSEQ_1:def 3,XXREAL_0:2;
then
A4: 1 in dom F by FINSEQ_1:1;
A5: now
A6: len <*2*> = 1 by FINSEQ_1:40;
assume
A7: H is negative;
then consider H1 such that
A8: H = 'not' H1;
(F^sq).1 = 2 by A3,A7,Th20;
then F.1 = 2 by A4,FINSEQ_1:def 7;
then F is negative by Th23;
then consider F1 such that
A9: F = 'not' F1;
len <*2*> + len H1 = len H by A8,FINSEQ_1:22;
then
A10: len H1 < len H by A6,NAT_1:13;
<*2*>^F1^sq = <*2*>^(F1^sq) by FINSEQ_1:32;
then H1 = F1^sq by A3,A8,A9,FINSEQ_1:33;
hence thesis by A1,A2,A8,A9,A10;
end;
A11: now
assume
A12: H is conjunctive;
then consider G1,G such that
A13: H = G1 '&' G;
A14: len G + (1 + len G1) = len G + 1 + len G1;
A15: len(<*3*>^G1) = len <*3*> + len G1 & len <*3*> = 1 by FINSEQ_1:22,40;
len(<*3*>^G1) + len G = len H by A13,FINSEQ_1:22;
then len G + 1 <= len H by A15,A14,NAT_1:11;
then
A16: len G < len H by NAT_1:13;
(F^sq).1 = 3 by A3,A12,Th21;
then F.1 = 3 by A4,FINSEQ_1:def 7;
then F is conjunctive by Th23;
then consider F1,H1 such that
A17: F = F1 '&' H1;
A18: now
A19: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A20: F1 = G1^sq9;
A21: len(F^sq) = len F + len sq & len <*3*> = 1 by FINSEQ_1:22,40;
len(<*3*>^F1) = len <*3*> + len F1 & len F = len(<*3*>^F1) + len
H1 by A17,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A21,A19,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A20;
end;
A22: <*3*>^F1^H1 = <*3*>^(F1^H1) & <*3*>^(F1^H1)^sq = <*3*>^(F1^H1^sq)
by FINSEQ_1:32;
A23: now
given sq9 such that
A24: G1 = F1^sq9;
A25: len <*3*> = 1 by FINSEQ_1:40;
len(<*3*>^G1) + len G = len H & len(<*3*>^G1) = len <*3*> + len
G1 by A13,FINSEQ_1:22;
then len G1 + 1 <= len H by A25,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A24;
end;
A26: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
<*3*>^G1^G = <*3*>^(G1^G) by FINSEQ_1:32;
then
A27: G1^G = F1^(H1^sq) by A3,A13,A17,A22,A26,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A27,A23,A18,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A17,A22,A26,A16;
end;
A28: now
assume
A29: H is universal;
then consider x,H1 such that
A30: H = All(x,H1);
A31: <*4*>^<*x*> = <*4,x*> by FINSEQ_1:def 9;
A32: len <*4,x*> = 2 & 1 + (1 + len H1) = 1 + len H1 + 1 by FINSEQ_1:44;
len(<*4*>^<*x*>) + len H1 = len H by A30,FINSEQ_1:22;
then len H1 + 1 <= len H by A32,A31,NAT_1:11;
then
A33: len H1 < len H by NAT_1:13;
(F^sq).1 = 4 by A3,A29,Th22;
then F.1 = 4 by A4,FINSEQ_1:def 7;
then F is universal by Th23;
then consider y,F1 such that
A34: F = All(y,F1);
A35: (<*x*>^H1).1 = x & (<*y*>^(F1^sq)).1 = y by FINSEQ_1:41;
A36: <*4*>^<*y*>^F1^sq = <*4*>^<*y*>^(F1^sq) by FINSEQ_1:32;
<*4*>^<*x*>^H1 = <*4*>^(<*x*>^H1) & <*4*>^<*y*>^(F1^sq) = <*4*>^(<*
y*>^(F1^ sq)) by FINSEQ_1:32;
then <*x*>^H1 = <*y*>^(F1^sq) by A3,A30,A34,A36,FINSEQ_1:33;
then H1 = F1^sq by A35,FINSEQ_1:33;
hence thesis by A1,A2,A3,A34,A36,A33;
end;
A37: len F + len sq = len(F^sq) by FINSEQ_1:22;
now
A38: 3 <= len F by Th13;
assume H is atomic;
then
A39: len H = 3 by Th11;
then len F <= 3 by A3,A37,NAT_1:11;
then 3 + len sq = 3 + 0 by A3,A37,A39,A38,XXREAL_0:1;
then sq = {};
hence thesis by A3,FINSEQ_1:34;
end;
hence thesis by A5,A28,A11,Th10;
end;
then
A40: for k being Nat st for n being Nat st n < k holds P[n] holds P[k];
A41: for n being Nat holds P[n] from NAT_1:sch 4(A40);
len H = len H;
hence thesis by A41;
end;
theorem Th30:
H '&' G = H1 '&' G1 implies H = H1 & G = G1
proof
assume
A1: H '&' G = H1 '&' G1;
<*3*>^H^G = <*3*>^(H^G) & <*3*>^H1^G1 = <*3*>^(H1^G1) by FINSEQ_1:32;
then
A2: H^G = H1^G1 by A1,FINSEQ_1:33;
then
A3: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A4: len H <= len H1 implies ex sq st H1 = H^sq by A2,FINSEQ_1:47;
hence H = H1 by A3,Th29;
(ex sq st H1 = H^sq) implies H1 = H by Th29;
hence thesis by A1,A3,A4,Th29,FINSEQ_1:33;
end;
theorem Th31:
F 'or' G = F1 'or' G1 implies F = F1 & G = G1
proof
assume F 'or' G = F1 'or' G1;
then 'not' F '&' 'not' G = 'not' F1 '&' 'not' G1 by FINSEQ_1:33;
then 'not' F = 'not' F1 & 'not' G = 'not' G1 by Th30;
hence thesis by FINSEQ_1:33;
end;
theorem Th32:
F => G = F1 => G1 implies F = F1 & G = G1
proof
assume F => G = F1 => G1;
then
A1: F '&' 'not' G = F1 '&' 'not' G1 by FINSEQ_1:33;
hence F = F1 by Th30;
'not' G = 'not' G1 by A1,Th30;
hence thesis by FINSEQ_1:33;
end;
theorem Th33:
F <=> G = F1 <=> G1 implies F = F1 & G = G1
proof
assume F <=> G = F1 <=> G1;
then F => G = F1=> G1 by Th30;
hence thesis by Th32;
end;
theorem Th34:
Ex(x,H) = Ex(y,G) implies x = y & H = G
proof
assume Ex(x,H) = Ex(y,G);
then
A1: All(x,'not' H) = All(y,'not' G) by FINSEQ_1:33;
then 'not' H = 'not' G by Th3;
hence thesis by A1,Th3,FINSEQ_1:33;
end;
::
:: The Select Function of ZF-fomrulae
::
definition
let H;
assume
A1: H is atomic;
func Var1 H -> Variable equals
:Def28:
H.2;
coherence
proof
H is being_equality or H is being_membership by A1;
then consider k,x,y such that
A2: H = <*k*>^<*x*>^<*y*>;
H = <* k,x,y *> by A2,FINSEQ_1:def 10;
hence thesis;
end;
func Var2 H -> Variable equals
:Def29:
H.3;
coherence
proof
H is being_equality or H is being_membership by A1;
then consider k,x,y such that
A3: H = <*k*>^<*x*>^<*y*>;
H = <* k,x,y *> by A3,FINSEQ_1:def 10;
hence thesis;
end;
end;
theorem
H is atomic implies Var1 H = H.2 & Var2 H = H.3 by Def28,Def29;
theorem Th36:
H is being_equality implies H = (Var1 H) '=' Var2 H
proof
assume
A1: H is being_equality;
then consider x,y such that
A2: H = x '=' y;
<*0*>^<*x*>^<*y*> = <*0,x,y*> by FINSEQ_1:def 10;
then
A3: H.2 = x & H.3 = y by A2;
A4: H is atomic by A1;
then H.2 = Var1 H by Def28;
hence thesis by A2,A4,A3,Def29;
end;
theorem Th37:
H is being_membership implies H = (Var1 H) 'in' Var2 H
proof
assume
A1: H is being_membership;
then consider x,y such that
A2: H = x 'in' y;
<*1*>^<*x*>^<*y*> = <*1,x,y*> by FINSEQ_1:def 10;
then
A3: H.2 = x & H.3 = y by A2;
A4: H is atomic by A1;
then H.2 = Var1 H by Def28;
hence thesis by A2,A4,A3,Def29;
end;
definition
let H;
assume
A1: H is negative;
func the_argument_of H -> ZF-formula means
:Def30:
'not' it = H;
existence by A1;
uniqueness by FINSEQ_1:33;
end;
definition
let H;
assume
A1: H is conjunctive or H is disjunctive;
func the_left_argument_of H -> ZF-formula means
:Def31:
ex H1 st it '&' H1 = H if H is conjunctive otherwise ex H1 st it 'or' H1 = H;
existence by A1;
uniqueness by Th30,Th31;
consistency;
func the_right_argument_of H -> ZF-formula means
:Def32:
ex H1 st H1 '&' it = H if H is conjunctive otherwise ex H1 st H1 'or' it = H;
existence
by A1;
uniqueness by Th30,Th31;
consistency;
end;
theorem
H is conjunctive implies (F = the_left_argument_of H iff ex G st F '&'
G = H) & (F = the_right_argument_of H iff ex G st G '&' F = H) by Def31,Def32;
theorem Th39:
H is disjunctive implies (F = the_left_argument_of H iff ex G st
F 'or' G = H) & (F = the_right_argument_of H iff ex G st G 'or' F = H)
proof
assume
A1: H is disjunctive;
then ex F,G st H = F 'or' G;
then H.1 = 2 by FINSEQ_1:41;
then not H is conjunctive by Th21;
hence thesis by A1,Def31,Def32;
end;
theorem Th40:
H is conjunctive implies H = (the_left_argument_of H) '&'
the_right_argument_of H
proof
assume
A1: H is conjunctive;
then ex F1 st H = (the_left_argument_of H) '&' F1 by Def31;
hence thesis by A1,Def32;
end;
theorem
H is disjunctive implies H = (the_left_argument_of H) 'or'
the_right_argument_of H
proof
assume
A1: H is disjunctive;
then ex F1 st H = (the_left_argument_of H) 'or' F1 by Th39;
hence thesis by A1,Th39;
end;
definition
let H;
assume
A1: H is universal or H is existential;
func bound_in H -> Variable means
:Def33:
ex H1 st All(it,H1) = H if H is universal otherwise ex H1 st Ex(it,H1) = H;
existence by A1;
uniqueness by Th3,Th34;
consistency;
func the_scope_of H -> ZF-formula means
:Def34:
ex x st All(x,it) = H if H is universal otherwise ex x st Ex(x,it) = H;
existence
by A1;
uniqueness by Th3,Th34;
consistency;
end;
theorem
H is universal implies (x = bound_in H iff ex H1 st All(x,H1) = H) & (
H1 = the_scope_of H iff ex x st All(x,H1) = H) by Def33,Def34;
theorem Th43:
H is existential implies (x = bound_in H iff ex H1 st Ex(x,H1) =
H) & (H1 = the_scope_of H iff ex x st Ex(x,H1) = H)
proof
assume
A1: H is existential;
then ex y,F st H = Ex(y,F);
then H.1 = 2 by FINSEQ_1:41;
then not H is universal by Th22;
hence thesis by A1,Def33,Def34;
end;
theorem Th44:
H is universal implies H = All(bound_in H,the_scope_of H)
proof
assume
A1: H is universal;
then ex x st H = All(x,the_scope_of H) by Def34;
hence thesis by A1,Def33;
end;
theorem
H is existential implies H = Ex(bound_in H,the_scope_of H)
proof
assume
A1: H is existential;
then ex x st H = Ex(x,the_scope_of H) by Th43;
hence thesis by A1,Th43;
end;
definition
let H;
assume
A1: H is conditional;
func the_antecedent_of H -> ZF-formula means
:Def35:
ex H1 st H = it => H1;
existence by A1;
uniqueness by Th32;
func the_consequent_of H -> ZF-formula means
:Def36:
ex H1 st H = H1 => it;
existence
by A1;
uniqueness by Th32;
end;
theorem
H is conditional implies (F = the_antecedent_of H iff ex G st H = F =>
G) & (F = the_consequent_of H iff ex G st H = G => F) by Def35,Def36;
theorem
H is conditional implies H = (the_antecedent_of H) => the_consequent_of H
proof
assume
A1: H is conditional;
then ex F st H = (the_antecedent_of H) => F by Def35;
hence thesis by A1,Def36;
end;
definition
let H;
assume
A1: H is biconditional;
func the_left_side_of H -> ZF-formula means
:Def37:
ex H1 st H = it <=> H1;
existence by A1;
uniqueness by Th33;
func the_right_side_of H -> ZF-formula means
:Def38:
ex H1 st H = H1 <=> it;
existence
by A1;
uniqueness by Th33;
end;
theorem
H is biconditional implies (F = the_left_side_of H iff ex G st H = F
<=> G) & (F = the_right_side_of H iff ex G st H = G <=> F) by Def37,Def38;
theorem
H is biconditional implies H = (the_left_side_of H) <=> the_right_side_of H
proof
assume
A1: H is biconditional;
then ex F st H = (the_left_side_of H) <=> F by Def37;
hence thesis by A1,Def38;
end;
::
:: The Immediate Constituents of ZF-formulae
::
definition
let H,F;
pred H is_immediate_constituent_of F means
F = 'not' H or ( ex H1 st
F = H '&' H1 or F = H1 '&' H ) or ex x st F = All(x,H);
end;
theorem Th50:
not H is_immediate_constituent_of x '=' y
proof
assume H is_immediate_constituent_of x '=' y;
then
A1: x '=' y = 'not' H or ( ex H1 st x '=' y = H '&' H1 or x '=' y = H1 '&' H
) or ex z st x '=' y = All(z,H);
(x '=' y).1 = 0 by Th15;
hence contradiction by A1,Th16,Th17,FINSEQ_1:41;
end;
theorem Th51:
not H is_immediate_constituent_of x 'in' y
proof
assume H is_immediate_constituent_of x 'in' y;
then
A1: x 'in' y = 'not' H or ( ex H1 st x 'in' y = H '&' H1 or x 'in' y = H1
'&' H ) or ex z st x 'in' y = All(z,H);
(x 'in' y).1 = 1 by Th15;
hence contradiction by A1,Th16,Th17,FINSEQ_1:41;
end;
theorem Th52:
F is_immediate_constituent_of 'not' H iff F = H
proof
thus F is_immediate_constituent_of 'not' H implies F = H
proof
A1: now
given x such that
A2: 'not' H = All(x,F);
('not' H).1 = 2 by FINSEQ_1:41;
hence contradiction by A2,Th17;
end;
A3: now
given H1 such that
A4: 'not' H = F '&' H1 or 'not' H = H1 '&' F;
('not' H).1 = 2 by FINSEQ_1:41;
hence contradiction by A4,Th16;
end;
assume F is_immediate_constituent_of 'not' H;
then
'not' H = 'not' F or ( ex H1 st 'not' H = F '&' H1 or 'not' H = H1 '&'
F ) or ex x st 'not' H = All(x,F);
hence thesis by A3,A1,FINSEQ_1:33;
end;
thus thesis;
end;
theorem Th53:
F is_immediate_constituent_of G '&' H iff F = G or F = H
proof
thus F is_immediate_constituent_of G '&' H implies F = G or F = H
proof
A1: now
given x such that
A2: G '&' H = All(x,F);
(G '&' H).1 = 3 by Th16;
hence contradiction by A2,Th17;
end;
A3: now
assume
A4: G '&' H = 'not' F;
(G '&' H).1 = 3 by Th16;
hence contradiction by A4,FINSEQ_1:41;
end;
assume F is_immediate_constituent_of G '&' H;
then ex H1 st G '&' H = F '&' H1 or G '&' H = H1 '&' F by A3,A1;
hence thesis by Th30;
end;
assume F = G or F = H;
hence thesis;
end;
theorem Th54:
F is_immediate_constituent_of All(x,H) iff F = H
proof
thus F is_immediate_constituent_of All(x,H) implies F = H
proof
A1: now
given G such that
A2: All(x,H) = F '&' G or All(x,H) = G '&' F;
(F '&' G).1 = 3 & (G '&' F).1 = 3 by Th16;
hence contradiction by A2,Th17;
end;
A3: now
assume
A4: All(x,H) = 'not' F;
All(x,H).1 = 4 by Th17;
hence contradiction by A4,FINSEQ_1:41;
end;
assume F is_immediate_constituent_of All(x,H);
then ex y st All(x,H) = All(y,F) by A3,A1;
hence thesis by Th3;
end;
thus thesis;
end;
theorem
H is atomic implies not F is_immediate_constituent_of H
proof
A1: H is being_equality implies thesis by Th50;
H is being_membership implies thesis by Th51;
hence thesis by A1;
end;
theorem Th56:
H is negative implies
(F is_immediate_constituent_of H iff F = the_argument_of H)
proof
assume H is negative;
then H = 'not' the_argument_of H by Def30;
hence thesis by Th52;
end;
theorem Th57:
H is conjunctive implies (F is_immediate_constituent_of H iff F
= the_left_argument_of H or F = the_right_argument_of H)
proof
assume H is conjunctive;
then H = (the_left_argument_of H) '&' the_right_argument_of H by Th40;
hence thesis by Th53;
end;
theorem Th58:
H is universal implies (F is_immediate_constituent_of H iff F =
the_scope_of H)
proof
assume H is universal;
then H = All(bound_in H,the_scope_of H) by Th44;
hence thesis by Th54;
end;
::
:: The Subformulae and The Proper Subformulae of ZF-formulae
::
reserve L,L9 for FinSequence;
definition
let H,F;
pred H is_subformula_of F means
ex n,L st 1 <= n & len L = n & L.1 =
H & L.n = F & for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 &
H1 is_immediate_constituent_of F1;
end;
theorem Th59:
H is_subformula_of H
proof
take 1 , <*H*>;
thus 1 <= 1;
thus len <*H*> = 1 by FINSEQ_1:40;
thus <*H*>.1 = H & <*H*>.1 = H;
thus thesis;
end;
definition
let H,F;
pred H is_proper_subformula_of F means
H is_subformula_of F & H <> F;
end;
theorem Th60:
H is_immediate_constituent_of F implies len H < len F
proof
A1: now
assume F = 'not' H;
then len F = len <*2*> + len H by FINSEQ_1:22
.= len H + 1 by FINSEQ_1:40;
hence thesis by NAT_1:13;
end;
A2: now
given H1 such that
A3: F = H '&' H1 or F = H1 '&' H;
A4: len(<*3*>^H1^H) = len(<*3*>^(H1^H)) by FINSEQ_1:32
.= len <*3*> + len(H1^H) by FINSEQ_1:22
.= 1 + len(H1^H) by FINSEQ_1:40
.= 1 + (len H + len H1) by FINSEQ_1:22
.= 1 + len H + len H1;
len(<*3*>^H^H1) = len(<*3*>^H) + len H1 by FINSEQ_1:22
.= len <*3*> + len H + len H1 by FINSEQ_1:22
.= 1 + len H + len H1 by FINSEQ_1:40;
then 1 + len H <= len F by A3,A4,NAT_1:11;
hence thesis by NAT_1:13;
end;
A5: now
given x such that
A6: F = All(x,H);
len F = len(<*4*>^<*x*>) + len H by A6,FINSEQ_1:22
.= len <*4*> + len <*x*> + len H by FINSEQ_1:22
.= 1 + len <*x*> + len H by FINSEQ_1:40
.= 1 + 1 + len H by FINSEQ_1:40
.= (1 + len H) + 1;
then 1 + len H <= len F by NAT_1:11;
hence thesis by NAT_1:13;
end;
assume H is_immediate_constituent_of F;
hence thesis by A1,A2,A5;
end;
theorem Th61:
H is_immediate_constituent_of F implies H is_proper_subformula_of F
proof
assume
A1: H is_immediate_constituent_of F;
thus H is_subformula_of F
proof
take n = 2 , L = <* H,F *>;
thus 1 <= n;
thus len L = n by FINSEQ_1:44;
thus L.1 = H & L.n = F;
let k;
assume that
A2: 1 <= k and
A3: k < n;
take H,F;
k < 1 + 1 by A3;
then k <= 1 by NAT_1:13;
then k = 1 by A2,XXREAL_0:1;
hence L.k = H & L.(k + 1) = F;
thus thesis by A1;
end;
assume H = F;
then len H = len F;
hence contradiction by A1,Th60;
end;
theorem Th62:
H is_proper_subformula_of F implies len H < len F
proof
assume H is_subformula_of F;
then consider n,L such that
A1: 1 <= n and
len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1;
defpred P[Nat] means 1 <= $1 & $1 < n implies for H1 st L.($1 + 1
) = H1 holds len H < len H1;
A5: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A6: 1 <= k & k < n implies for H1 st L.(k + 1) = H1 holds len H < len H1 and
A7: 1 <= k + 1 and
A8: k + 1 < n;
consider F1,G such that
A9: L.(k + 1) = F1 and
A10: L.(k + 1 + 1) = G & F1 is_immediate_constituent_of G by A4,A7,A8;
let H1 such that
A11: L.(k + 1 + 1) = H1;
A12: now
given m be Nat such that
A13: k = m + 1;
len H < len F1 by A6,A8,A9,A13,NAT_1:11,13;
hence thesis by A11,A10,Th60,XXREAL_0:2;
end;
k = 0 implies len H < len H1 by A2,A11,A9,A10,Th60;
hence thesis by A12,NAT_1:6;
end;
assume H <> F;
then 1 < n by A1,A2,A3,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A14: n = 2 + k by NAT_1:10;
A15: P[0];
A16: for k being Nat holds P[k] from NAT_1:sch 2(A15,A5);
reconsider k as Element of NAT by ORDINAL1:def 12;
A17: 1 + 1 + k = (1 + k) + 1;
then 1 + k < n by A14,NAT_1:13;
hence thesis by A3,A16,A14,A17,NAT_1:11;
end;
theorem Th63:
H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F
proof
assume H is_subformula_of F;
then consider n,L such that
A1: 1 <= n and
len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1;
assume H <> F;
then 1 < n by A1,A2,A3,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A5: n = 2 + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
1 + 1 + k = (1 + k) + 1;
then 1 + k < n by A5,NAT_1:13;
then consider H1,F1 such that
L.(1 + k) = H1 and
A6: L.(1 + k + 1) = F1 & H1 is_immediate_constituent_of F1 by A4,NAT_1:11;
take H1;
thus thesis by A3,A5,A6;
end;
reserve j,j1 for Element of NAT;
theorem Th64:
F is_proper_subformula_of G & G is_proper_subformula_of H
implies F is_proper_subformula_of H
proof
assume that
A1: F is_subformula_of G and
A2: F <> G and
A3: G is_subformula_of H and
A4: G <> H;
consider m,L9 such that
A5: 1 <= m and
A6: len L9 = m and
A7: L9.1 = G and
A8: L9.m = H and
A9: for k st 1 <= k & k < m ex H1,F1 st L9.k = H1 & L9.(k + 1) = F1 &
H1 is_immediate_constituent_of F1 by A3;
consider n,L such that
A10: 1 <= n and
A11: len L = n and
A12: L.1 = F and
A13: L.n = G and
A14: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A1;
1 < n by A2,A10,A12,A13,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A15: n = 2 + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
thus F is_subformula_of H
proof
take l = 1 + k + m, K = L1^L9;
A16: 1 + k + m - (1 + k) = m;
m <= m + (1 + k) by NAT_1:11;
hence 1 <= l by A5,XXREAL_0:2;
1 + 1 + k = 1 + k + 1;
then
A17: 1 + k <= n by A15,NAT_1:11;
then
A18: len L1 = 1 + k by A11,FINSEQ_1:17;
hence
A19: len K = l by A6,FINSEQ_1:22;
A20: now
let j;
assume 1 <= j & j <= 1 + k;
then
A21: j in Seg(1 + k) by FINSEQ_1:1;
then j in dom L1 by A11,A17,FINSEQ_1:17;
then K.j = L1.j by FINSEQ_1:def 7;
hence K.j = L.j by A21,FUNCT_1:49;
end;
1 <= 1 + k by NAT_1:11;
hence K.1 = F by A12,A20;
len L1 + 1 <= len L1 + m by A5,XREAL_1:7;
then len L1 < l by A18,NAT_1:13;
then K.l = L9.(l - len L1) by A19,FINSEQ_1:24;
hence K.l = H by A11,A8,A17,A16,FINSEQ_1:17;
let j such that
A22: 1 <= j and
A23: j < l;
j + 0 <= j + 1 by XREAL_1:7;
then
A24: 1 <= j + 1 by A22,XXREAL_0:2;
A25: now
assume
A26: j < 1 + k;
then
A27: j + 1 <= 1 + k by NAT_1:13;
then j + 1 <= n by A17,XXREAL_0:2;
then j < n by NAT_1:13;
then consider F1,G1 such that
A28: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A14,A22;
take F1, G1;
thus K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A20
,A22,A24,A26,A27,A28;
end;
A29: now
A30: j + 1 <= l by A23,NAT_1:13;
assume
A31: 1 + k < j;
then
A32: 1 + k < j + 1 by NAT_1:13;
1 + k + 1 <= j by A31,NAT_1:13;
then consider j1 be Nat such that
A33: j = 1 + k + 1 + j1 by NAT_1:10;
reconsider j1 as Element of NAT by ORDINAL1:def 12;
j - (1 + k) < l - (1 + k) by A23,XREAL_1:9;
then consider F1,G1 such that
A34: L9.(1 + j1) = F1 & L9.(1 + j1 + 1) = G1 & F1
is_immediate_constituent_of G1 by A9,A33,NAT_1:11;
take F1, G1;
A35: 1 + j1 + (1 + k) - (1 + k) = 1 + j1 + (1 + k) + -(1 + k);
j + 1 - len L1 = 1 + (j + -len L1)
.= 1 + j1 + 1 by A11,A17,A33,A35,FINSEQ_1:17;
hence K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by
A18,A19,A23,A31,A32,A30,A35,A34,FINSEQ_1:24;
end;
now
A36: j + 1 <= l & j + 1 - j = j + 1 + -j by A23,NAT_1:13;
assume
A37: j = 1 + k;
then j < 1 + k + 1 by NAT_1:13;
then consider F1,G1 such that
A38: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1
by A14,A15,A22;
take F1, G1;
1 + k < j + 1 by A37,NAT_1:13;
hence
K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A13,A7
,A15,A18,A19,A20,A22,A37,A36,A38,FINSEQ_1:24;
end;
hence thesis by A25,A29,XXREAL_0:1;
end;
assume
A39: F = H;
F is_proper_subformula_of G by A1,A2;
then
A40: len F < len G by Th62;
G is_proper_subformula_of H by A3,A4;
hence contradiction by A39,A40,Th62;
end;
theorem Th65:
F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H
proof
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H;
now
assume F <> G;
then
A3: F is_proper_subformula_of G by A1;
now
assume G <> H;
then G is_proper_subformula_of H by A2;
then F is_proper_subformula_of H by A3,Th64;
hence thesis;
end;
hence thesis by A1;
end;
hence thesis by A2;
end;
theorem
G is_subformula_of H & H is_subformula_of G implies G = H
proof
assume that
A1: G is_subformula_of H and
A2: H is_subformula_of G;
assume
A3: G <> H;
then G is_proper_subformula_of H by A1;
then
A4: len G < len H by Th62;
H is_proper_subformula_of G by A2,A3;
hence contradiction by A4,Th62;
end;
theorem Th67:
not F is_proper_subformula_of x '=' y
proof
assume F is_proper_subformula_of x '=' y;
then ex G st G is_immediate_constituent_of x '=' y by Th63;
hence contradiction by Th50;
end;
theorem Th68:
not F is_proper_subformula_of x 'in' y
proof
assume F is_proper_subformula_of x 'in' y;
then ex G st G is_immediate_constituent_of x 'in' y by Th63;
hence contradiction by Th51;
end;
theorem Th69:
F is_proper_subformula_of 'not' H implies F is_subformula_of H
proof
assume that
A1: F is_subformula_of 'not' H and
A2: F <> 'not' H;
consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = 'not' H and
A7: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A1;
1 < n by A2,A3,A5,A6,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A8: n = 2 + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k, L1;
thus
A9: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A4,A8,FINSEQ_1:17;
A10: now
let j be Nat;
assume 1 <= j & j <= m;
then j in { j1 where j1 is Nat : 1 <= j1 & j1 <= 1 + k };
then j in Seg(1 + k) by FINSEQ_1:def 1;
hence L1.j = L.j by FUNCT_1:49;
end;
hence L1.1 = F by A5,A9;
m < m + 1 by NAT_1:13;
then consider F1,G1 such that
A11: L.m = F1 and
A12: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A8,NAT_1:11;
F1 = H by A6,A8,A12,Th52;
hence L1.m = H by A9,A10,A11;
let j;
assume that
A13: 1 <= j and
A14: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A8,A14,XXREAL_0:2;
then consider F1,G1 such that
A15: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A13;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A13,A14,NAT_1:13;
hence thesis by A10,A13,A14,A15;
end;
theorem Th70:
F is_proper_subformula_of G '&' H implies F is_subformula_of G
or F is_subformula_of H
proof
assume that
A1: F is_subformula_of G '&' H and
A2: F <> G '&' H;
consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = G '&' H and
A7: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A1;
1 < n by A2,A3,A5,A6,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A8: n = 2 + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
1 + 1 + k = 1 + k + 1;
then 1 + k < n by A8,NAT_1:13;
then consider H1,G1 such that
A9: L.(1 + k) = H1 and
A10: L.(1 + k + 1) = G1 & H1 is_immediate_constituent_of G1 by A7,NAT_1:11;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
F is_subformula_of H1
proof
take m = 1 + k, L1;
thus
A11: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A4,A8,FINSEQ_1:17;
A12: now
let j be Nat;
assume 1 <= j & j <= m;
then j in { j1 where j1 is Nat : 1 <= j1 & j1 <= 1 + k };
then j in Seg(1 + k) by FINSEQ_1:def 1;
hence L1.j = L.j by FUNCT_1:49;
end;
hence L1.1 = F by A5,A11;
thus L1.m = H1 by A9,A11,A12;
let j;
assume that
A13: 1 <= j and
A14: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A8,A14,XXREAL_0:2;
then consider F1,G1 such that
A15: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A13;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A13,A14,NAT_1:13;
hence thesis by A12,A13,A14,A15;
end;
hence thesis by A6,A8,A10,Th53;
end;
theorem Th71:
F is_proper_subformula_of All(x,H) implies F is_subformula_of H
proof
assume that
A1: F is_subformula_of All(x,H) and
A2: F <> All(x,H);
consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = All(x,H) and
A7: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
is_immediate_constituent_of F1 by A1;
1 < n by A2,A3,A5,A6,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k be Nat such that
A8: n = 2 + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k, L1;
thus
A9: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A4,A8,FINSEQ_1:17;
A10: now
let j be Nat;
assume 1 <= j & j <= m;
then j in { j1 where j1 is Nat : 1 <= j1 & j1 <= 1 + k };
then j in Seg(1 + k) by FINSEQ_1:def 1;
hence L1.j = L.j by FUNCT_1:49;
end;
hence L1.1 = F by A5,A9;
m < m + 1 by NAT_1:13;
then consider F1,G1 such that
A11: L.m = F1 and
A12: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A8,NAT_1:11;
F1 = H by A6,A8,A12,Th54;
hence L1.m = H by A9,A10,A11;
let j;
assume that
A13: 1 <= j and
A14: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A8,A14,XXREAL_0:2;
then consider F1,G1 such that
A15: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A13;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A13,A14,NAT_1:13;
hence thesis by A10,A13,A14,A15;
end;
theorem
H is atomic implies not F is_proper_subformula_of H
proof
assume H is atomic;
then H is being_equality or H is being_membership;
then H = (Var1 H) '=' Var2 H or H = (Var1 H) 'in' Var2 H by Th36,Th37;
hence thesis by Th67,Th68;
end;
theorem
H is negative implies the_argument_of H is_proper_subformula_of H
proof
assume H is negative;
then the_argument_of H is_immediate_constituent_of H by Th56;
hence thesis by Th61;
end;
theorem
H is conjunctive implies the_left_argument_of H
is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H
proof
assume H is conjunctive;
then the_left_argument_of H is_immediate_constituent_of H &
the_right_argument_of H is_immediate_constituent_of H by Th57;
hence thesis by Th61;
end;
theorem
H is universal implies the_scope_of H is_proper_subformula_of H
proof
assume H is universal;
then the_scope_of H is_immediate_constituent_of H by Th58;
hence thesis by Th61;
end;
theorem Th76:
H is_subformula_of x '=' y iff H = x '=' y
proof
thus H is_subformula_of x '=' y implies H = x '=' y
proof
assume
A1: H is_subformula_of x '=' y;
assume H <> x '=' y;
then H is_proper_subformula_of x '=' y by A1;
then ex F st F is_immediate_constituent_of x '=' y by Th63;
hence contradiction by Th50;
end;
thus thesis by Th59;
end;
theorem Th77:
H is_subformula_of x 'in' y iff H = x 'in' y
proof
thus H is_subformula_of x 'in' y implies H = x 'in' y
proof
assume
A1: H is_subformula_of x 'in' y;
assume H <> x 'in' y;
then H is_proper_subformula_of x 'in' y by A1;
then ex F st F is_immediate_constituent_of x 'in' y by Th63;
hence contradiction by Th51;
end;
assume H = x 'in' y;
hence thesis by Th59;
end;
::
:: The Set of Subformulae of ZF-formulae
::
definition
let H;
func Subformulae H -> set means
:Def42:
a in it iff ex F st F = a & F is_subformula_of H;
existence
proof
defpred X[set] means ex F st F = $1 & F is_subformula_of H;
consider X such that
A1: a in X iff a in NAT* & X[a] from XFAMILY:sch 1;
take X;
let a;
thus a in X implies ex F st F = a & F is_subformula_of H by A1;
given F such that
A2: F = a & F is_subformula_of H;
F in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A2;
end;
uniqueness
proof
let X,Y such that
A3: a in X iff ex F st F = a & F is_subformula_of H and
A4: a in Y iff ex F st F = a & F is_subformula_of H;
now
let a be object;
thus a in X implies a in Y
proof
assume a in X;
then ex F st F = a & F is_subformula_of H by A3;
hence thesis by A4;
end;
assume a in Y;
then ex F st F = a & F is_subformula_of H by A4;
hence a in X by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th78:
G in Subformulae H implies G is_subformula_of H
proof
assume G in Subformulae H;
then ex F st F = G & F is_subformula_of H by Def42;
hence thesis;
end;
theorem
F is_subformula_of H implies Subformulae F c= Subformulae H
proof
assume
A1: F is_subformula_of H;
let a be object;
assume a in Subformulae F;
then consider F1 such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def42;
F1 is_subformula_of H by A1,A3,Th65;
hence thesis by A2,Def42;
end;
theorem Th80:
Subformulae x '=' y = { x '=' y }
proof
now
let a be object;
thus a in Subformulae x '=' y implies a in { x '=' y }
proof
assume a in Subformulae x '=' y;
then consider F such that
A1: F = a and
A2: F is_subformula_of x '=' y by Def42;
F = x '=' y by A2,Th76;
hence thesis by A1,TARSKI:def 1;
end;
assume a in { x '=' y };
then
A3: a = x '=' y by TARSKI:def 1;
x '=' y is_subformula_of x '=' y by Th59;
hence a in Subformulae x '=' y by A3,Def42;
end;
hence thesis by TARSKI:2;
end;
theorem Th81:
Subformulae x 'in' y = { x 'in' y }
proof
now
let a be object;
thus a in Subformulae x 'in' y implies a in { x 'in' y }
proof
assume a in Subformulae x 'in' y;
then consider F such that
A1: F = a and
A2: F is_subformula_of x 'in' y by Def42;
F = x 'in' y by A2,Th77;
hence thesis by A1,TARSKI:def 1;
end;
assume a in { x 'in' y };
then
A3: a = x 'in' y by TARSKI:def 1;
x 'in' y is_subformula_of x 'in' y by Th59;
hence a in Subformulae x 'in' y by A3,Def42;
end;
hence thesis by TARSKI:2;
end;
theorem Th82:
Subformulae 'not' H = Subformulae H \/ { 'not' H }
proof
now
let a be object;
A1: now
assume a in { 'not' H };
then
A2: a = 'not' H by TARSKI:def 1;
'not' H is_subformula_of 'not' H by Th59;
hence a in Subformulae 'not' H by A2,Def42;
end;
thus a in Subformulae 'not' H implies a in Subformulae H \/ { 'not' H }
proof
assume a in Subformulae 'not' H;
then consider F such that
A3: F = a and
A4: F is_subformula_of 'not' H by Def42;
now
assume F <> 'not' H;
then F is_proper_subformula_of 'not' H by A4;
then F is_subformula_of H by Th69;
hence a in Subformulae H by A3,Def42;
end;
then a in Subformulae H or a in { 'not' H } by A3,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
A5: now
assume a in Subformulae H;
then consider F such that
A6: F = a and
A7: F is_subformula_of H by Def42;
H is_immediate_constituent_of 'not' H;
then H is_proper_subformula_of 'not' H by Th61;
then H is_subformula_of 'not' H;
then F is_subformula_of 'not' H by A7,Th65;
hence a in Subformulae 'not' H by A6,Def42;
end;
assume a in Subformulae H \/ { 'not' H };
hence a in Subformulae 'not' H by A5,A1,XBOOLE_0:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem Th83:
Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F }
proof
now
let a be object;
A1: a in Subformulae H \/ Subformulae F implies a in Subformulae H or a
in Subformulae F by XBOOLE_0:def 3;
thus a in Subformulae H '&' F implies a in Subformulae H \/ Subformulae F
\/ { H '&' F }
proof
assume a in Subformulae H '&' F;
then consider G such that
A2: G = a and
A3: G is_subformula_of H '&' F by Def42;
now
assume G <> H '&' F;
then G is_proper_subformula_of H '&' F by A3;
then G is_subformula_of H or G is_subformula_of F by Th70;
then a in Subformulae H or a in Subformulae F by A2,Def42;
hence a in Subformulae H \/ Subformulae F by XBOOLE_0:def 3;
end;
then a in Subformulae H \/ Subformulae F or a in { H '&' F } by A2,
TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
A4: now
assume a in { H '&' F };
then
A5: a = H '&' F by TARSKI:def 1;
H '&' F is_subformula_of H '&' F by Th59;
hence a in Subformulae H '&' F by A5,Def42;
end;
A6: now
assume a in Subformulae F;
then consider G such that
A7: G = a and
A8: G is_subformula_of F by Def42;
F is_immediate_constituent_of H '&' F;
then F is_proper_subformula_of H '&' F by Th61;
then F is_subformula_of H '&' F;
then G is_subformula_of H '&' F by A8,Th65;
hence a in Subformulae H '&' F by A7,Def42;
end;
A9: now
assume a in Subformulae H;
then consider G such that
A10: G = a and
A11: G is_subformula_of H by Def42;
H is_immediate_constituent_of H '&' F;
then H is_proper_subformula_of H '&' F by Th61;
then H is_subformula_of H '&' F;
then G is_subformula_of H '&' F by A11,Th65;
hence a in Subformulae H '&' F by A10,Def42;
end;
assume a in Subformulae H \/ Subformulae F \/ { H '&' F };
hence a in Subformulae H '&' F by A1,A9,A6,A4,XBOOLE_0:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem Th84:
Subformulae All(x,H) = Subformulae H \/ { All(x,H) }
proof
now
let a be object;
A1: now
assume a in { All(x,H) };
then
A2: a = All(x,H) by TARSKI:def 1;
All(x,H) is_subformula_of All(x,H) by Th59;
hence a in Subformulae All(x,H) by A2,Def42;
end;
thus a in Subformulae All(x,H) implies a in Subformulae H \/ { All(x,H) }
proof
assume a in Subformulae All(x,H);
then consider F such that
A3: F = a and
A4: F is_subformula_of All(x,H) by Def42;
now
assume F <> All(x,H);
then F is_proper_subformula_of All(x,H) by A4;
then F is_subformula_of H by Th71;
hence a in Subformulae H by A3,Def42;
end;
then a in Subformulae H or a in { All(x,H) } by A3,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
A5: now
assume a in Subformulae H;
then consider F such that
A6: F = a and
A7: F is_subformula_of H by Def42;
H is_immediate_constituent_of All(x,H);
then H is_proper_subformula_of All(x,H) by Th61;
then H is_subformula_of All(x,H);
then F is_subformula_of All(x,H) by A7,Th65;
hence a in Subformulae All(x,H) by A6,Def42;
end;
assume a in Subformulae H \/ { All(x,H) };
hence a in Subformulae All(x,H) by A5,A1,XBOOLE_0:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem
H is atomic iff Subformulae H = { H }
proof
thus H is atomic implies Subformulae H = { H }
proof
assume H is atomic;
then H is being_equality or H is being_membership;
then H = (Var1 H) '=' Var2 H or H = (Var1 H) 'in' Var2 H by Th36,Th37;
hence thesis by Th80,Th81;
end;
assume
A1: Subformulae H = { H };
A2: now
assume H = 'not' the_argument_of H;
then
A3: the_argument_of H is_immediate_constituent_of H;
then the_argument_of H is_proper_subformula_of H by Th61;
then the_argument_of H is_subformula_of H;
then
A4: the_argument_of H in Subformulae H by Def42;
len(the_argument_of H) <> len H by A3,Th60;
hence contradiction by A1,A4,TARSKI:def 1;
end;
A5: now
assume H = (the_left_argument_of H) '&' the_right_argument_of H;
then
A6: the_left_argument_of H is_immediate_constituent_of H;
then the_left_argument_of H is_proper_subformula_of H by Th61;
then the_left_argument_of H is_subformula_of H;
then
A7: the_left_argument_of H in Subformulae H by Def42;
len(the_left_argument_of H) <> len H by A6,Th60;
hence contradiction by A1,A7,TARSKI:def 1;
end;
assume not H is atomic;
then H is negative or H is conjunctive or H is universal by Th10;
then H = 'not' the_argument_of H or H = (the_left_argument_of H) '&'
the_right_argument_of H or H = All(bound_in H,the_scope_of H) by Def30,Th40
,Th44;
then
A8: the_scope_of H is_immediate_constituent_of H by A2,A5;
then the_scope_of H is_proper_subformula_of H by Th61;
then the_scope_of H is_subformula_of H;
then
A9: the_scope_of H in Subformulae H by Def42;
len(the_scope_of H) <> len H by A8,Th60;
hence contradiction by A1,A9,TARSKI:def 1;
end;
theorem
H is negative implies Subformulae H = Subformulae the_argument_of H \/ { H }
proof
assume H is negative;
then H = 'not' the_argument_of H by Def30;
hence thesis by Th82;
end;
theorem
H is conjunctive implies Subformulae H = Subformulae
the_left_argument_of H \/ Subformulae the_right_argument_of H \/ { H }
proof
assume H is conjunctive;
then H = (the_left_argument_of H) '&' the_right_argument_of H by Th40;
hence thesis by Th83;
end;
theorem
H is universal implies Subformulae H = Subformulae the_scope_of H \/ { H }
proof
assume H is universal;
then H = All(bound_in H,the_scope_of H) by Th44;
hence thesis by Th84;
end;
theorem
(H is_immediate_constituent_of G or H is_proper_subformula_of G or H
is_subformula_of G) & G in Subformulae F implies H in Subformulae F
proof
assume that
A1: H is_immediate_constituent_of G or H is_proper_subformula_of G or H
is_subformula_of G and
A2: G in Subformulae F;
H is_proper_subformula_of G or H is_subformula_of G by A1,Th61;
then
A3: H is_subformula_of G;
G is_subformula_of F by A2,Th78;
then H is_subformula_of F by A3,Th65;
hence thesis by Def42;
end;
::
:: The Structural Induction Schemes
::
scheme
ZFInd { P[ZF-formula] } : for H holds P[H]
provided
A1: for H st H is atomic holds P[H] and
A2: for H st H is negative & P[the_argument_of H] holds P[H] and
A3: for H st H is conjunctive & P[the_left_argument_of H] & P[
the_right_argument_of H] holds P[H] and
A4: for H st H is universal & P[the_scope_of H] holds P[H]
proof
defpred Q[Nat] means for H st len H = $1 holds P[H];
A5: for n being Nat st for k being Nat st k < n holds Q[k] holds Q[n]
proof
let n be Nat such that
A6: for k being Nat st k < n for H st len H = k holds P[H];
let H such that
A7: len H = n;
A8: now
assume
A9: H is conjunctive;
then
A10: H = (the_left_argument_of H) '&' the_right_argument_of H by Th40;
then the_right_argument_of H is_immediate_constituent_of H;
then len the_right_argument_of H < len H by Th60;
then
A11: P[the_right_argument_of H] by A6,A7;
the_left_argument_of H is_immediate_constituent_of H by A10;
then len the_left_argument_of H < len H by Th60;
then P[the_left_argument_of H] by A6,A7;
hence thesis by A3,A9,A11;
end;
A12: now
assume
A13: H is universal;
then H = All(bound_in H,the_scope_of H) by Th44;
then the_scope_of H is_immediate_constituent_of H;
then len the_scope_of H < len H by Th60;
hence thesis by A4,A6,A7,A13;
end;
now
assume
A14: H is negative;
then H = 'not' the_argument_of H by Def30;
then the_argument_of H is_immediate_constituent_of H;
then len the_argument_of H < len H by Th60;
hence thesis by A2,A6,A7,A14;
end;
hence thesis by A1,A8,A12,Th10;
end;
A15: for n being Nat holds Q[n] from NAT_1:sch 4(A5);
let H;
len H = len H;
hence thesis by A15;
end;
scheme
ZFCompInd { P[ZF-formula] } : for H holds P[H]
provided
A1: for H st for F st F is_proper_subformula_of H holds P[F] holds P[H]
proof
defpred Q[Nat] means for H st len H = $1 holds P[H];
A2: for n being Nat st for k be Nat st k < n holds Q[k] holds Q[n]
proof
let n be Nat such that
A3: for k being Nat st k < n for H st len H = k holds P[H];
let H such that
A4: len H = n;
now
let F;
assume F is_proper_subformula_of H;
then len F < len H by Th62;
hence P[F] by A3,A4;
end;
hence thesis by A1;
end;
A5: for n being Nat holds Q[n] from NAT_1:sch 4 (A2);
let H;
len H = len H;
hence thesis by A5;
end;