zf_lang.miz
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 ;
definition
::
ZF_LANG:def1
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;
::
ZF_LANG:def2
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;
registration
cluster ->
natural for
Variable;
coherence ;
end
definition
let x, y;
::
ZF_LANG:def3
func x
'=' y ->
FinSequence of
NAT equals ((
<*
0 *>
^
<*x*>)
^
<*y*>);
coherence ;
::
ZF_LANG:def4
func x
'in' y ->
FinSequence of
NAT equals ((
<*1*>
^
<*x*>)
^
<*y*>);
coherence ;
end
theorem ::
ZF_LANG:1
(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 by
FINSEQ_1: 44;
A3: (
<*x*>
^
<*y*>)
=
<*x, y*> & (
<*z*>
^
<*t*>)
=
<*z, t*> by
FINSEQ_1:def 9;
A4: (
<*z, t*>
. 1)
= z & (
<*z, t*>
. 2)
= t by
FINSEQ_1: 44;
assume (x
'=' y)
= (z
'=' t);
hence thesis by
A1,
A2,
A4,
A3,
FINSEQ_1: 33;
end;
theorem ::
ZF_LANG:2
(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 by
FINSEQ_1: 44;
A3: (
<*x*>
^
<*y*>)
=
<*x, y*> & (
<*z*>
^
<*t*>)
=
<*z, t*> by
FINSEQ_1:def 9;
A4: (
<*z, t*>
. 1)
= z & (
<*z, t*>
. 2)
= t by
FINSEQ_1: 44;
assume (x
'in' y)
= (z
'in' t);
hence thesis by
A1,
A2,
A4,
A3,
FINSEQ_1: 33;
end;
definition
let p;
::
ZF_LANG:def5
func
'not' p ->
FinSequence of
NAT equals (
<*2*>
^ p);
coherence ;
let q;
::
ZF_LANG:def6
func p
'&' q ->
FinSequence of
NAT equals ((
<*3*>
^ p)
^ q);
coherence ;
end
definition
let x, p;
::
ZF_LANG:def7
func
All (x,p) ->
FinSequence of
NAT equals ((
<*4*>
^
<*x*>)
^ p);
coherence ;
end
theorem ::
ZF_LANG:3
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;
definition
::
ZF_LANG:def8
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 ;
::
ZF_LANG:def9
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 ::
ZF_LANG:4
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
definition
let H;
::
ZF_LANG:def10
attr H is
being_equality means ex x, y st H
= (x
'=' y);
::
ZF_LANG:def11
attr H is
being_membership means ex x, y st H
= (x
'in' y);
::
ZF_LANG:def12
attr H is
negative means ex H1 st H
= (
'not' H1);
::
ZF_LANG:def13
attr H is
conjunctive means ex F, G st H
= (F
'&' G);
::
ZF_LANG:def14
attr H is
universal means ex x, H1 st H
= (
All (x,H1));
end
theorem ::
ZF_LANG:5
(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;
::
ZF_LANG:def15
attr H is
atomic means H is
being_equality or H is
being_membership;
end
definition
let F, G;
::
ZF_LANG:def16
func F
'or' G ->
ZF-formula equals (
'not' ((
'not' F)
'&' (
'not' G)));
coherence ;
::
ZF_LANG:def17
func F
=> G ->
ZF-formula equals (
'not' (F
'&' (
'not' G)));
coherence ;
end
definition
let F, G;
::
ZF_LANG:def18
func F
<=> G ->
ZF-formula equals ((F
=> G)
'&' (G
=> F));
coherence ;
end
definition
let x, H;
::
ZF_LANG:def19
func
Ex (x,H) ->
ZF-formula equals (
'not' (
All (x,(
'not' H))));
coherence ;
end
definition
let H;
::
ZF_LANG:def20
attr H is
disjunctive means ex F, G st H
= (F
'or' G);
::
ZF_LANG:def21
attr H is
conditional means ex F, G st H
= (F
=> G);
::
ZF_LANG:def22
attr H is
biconditional means ex F, G st H
= (F
<=> G);
::
ZF_LANG:def23
attr H is
existential means ex x, H1 st H
= (
Ex (x,H1));
end
theorem ::
ZF_LANG:6
(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;
::
ZF_LANG:def24
func
All (x,y,H) ->
ZF-formula equals (
All (x,(
All (y,H))));
coherence ;
::
ZF_LANG:def25
func
Ex (x,y,H) ->
ZF-formula equals (
Ex (x,(
Ex (y,H))));
coherence ;
end
theorem ::
ZF_LANG:7
(
All (x,y,H))
= (
All (x,(
All (y,H)))) & (
Ex (x,y,H))
= (
Ex (x,(
Ex (y,H))));
definition
let x, y, z, H;
::
ZF_LANG:def26
func
All (x,y,z,H) ->
ZF-formula equals (
All (x,(
All (y,z,H))));
coherence ;
::
ZF_LANG:def27
func
Ex (x,y,z,H) ->
ZF-formula equals (
Ex (x,(
Ex (y,z,H))));
coherence ;
end
theorem ::
ZF_LANG:8
(
All (x,y,z,H))
= (
All (x,(
All (y,z,H)))) & (
Ex (x,y,z,H))
= (
Ex (x,(
Ex (y,z,H))));
theorem ::
ZF_LANG:9
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 ::
ZF_LANG:10
Th10: H is
atomic or H is
negative or H is
conjunctive or H is
universal by
Th9;
theorem ::
ZF_LANG:11
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 ::
ZF_LANG:12
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,
FINSEQ_1: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,
FINSEQ_1: 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 ::
ZF_LANG:13
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 ::
ZF_LANG:14
(
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 ::
ZF_LANG:15
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 ::
ZF_LANG:16
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 ::
ZF_LANG:17
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 ::
ZF_LANG:18
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 by
FINSEQ_1: 45;
end;
theorem ::
ZF_LANG:19
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 by
FINSEQ_1: 45;
end;
theorem ::
ZF_LANG:20
Th20: H is
negative implies (H
. 1)
= 2 by
FINSEQ_1: 41;
theorem ::
ZF_LANG:21
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 ::
ZF_LANG:22
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 ::
ZF_LANG:23
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 ::
ZF_LANG:24
(H
. 1)
=
0 implies H is
being_equality by
Th23;
theorem ::
ZF_LANG:25
(H
. 1)
= 1 implies H is
being_membership by
Th23;
theorem ::
ZF_LANG:26
(H
. 1)
= 2 implies H is
negative by
Th23;
theorem ::
ZF_LANG:27
(H
. 1)
= 3 implies H is
conjunctive by
Th23;
theorem ::
ZF_LANG:28
(H
. 1)
= 4 implies H is
universal by
Th23;
reserve sq,sq9 for
FinSequence;
theorem ::
ZF_LANG:29
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 be
Nat st for k be
Nat st k
< n holds for H, F, sq st (
len H)
= k & H
= (F
^ sq) holds H
= F holds 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 holds 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,
FINSEQ_1: 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,
FINSEQ_1: 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,
FINSEQ_1: 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 be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k];
A41: for n be
Nat holds
P[n] from
NAT_1:sch 4(
A40);
(
len H)
= (
len H);
hence thesis by
A41;
end;
theorem ::
ZF_LANG:30
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 ::
ZF_LANG:31
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 ::
ZF_LANG:32
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 ::
ZF_LANG:33
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 ::
ZF_LANG:34
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;
definition
let H;
assume
A1: H is
atomic;
::
ZF_LANG:def28
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 by
FINSEQ_1: 45;
end;
::
ZF_LANG:def29
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 by
FINSEQ_1: 45;
end;
end
theorem ::
ZF_LANG:35
H is
atomic implies (
Var1 H)
= (H
. 2) & (
Var2 H)
= (H
. 3) by
Def28,
Def29;
theorem ::
ZF_LANG:36
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,
FINSEQ_1: 45;
A4: H is
atomic by
A1;
then (H
. 2)
= (
Var1 H) by
Def28;
hence thesis by
A2,
A4,
A3,
Def29;
end;
theorem ::
ZF_LANG:37
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,
FINSEQ_1: 45;
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;
::
ZF_LANG:def30
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;
::
ZF_LANG:def31
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 ;
::
ZF_LANG:def32
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 ::
ZF_LANG:38
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 ::
ZF_LANG:39
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 ::
ZF_LANG:40
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 ::
ZF_LANG:41
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;
::
ZF_LANG:def33
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 ;
::
ZF_LANG:def34
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 ::
ZF_LANG:42
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 ::
ZF_LANG:43
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 ::
ZF_LANG:44
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 ::
ZF_LANG:45
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;
::
ZF_LANG:def35
func
the_antecedent_of H ->
ZF-formula means
:
Def35: ex H1 st H
= (it
=> H1);
existence by
A1;
uniqueness by
Th32;
::
ZF_LANG:def36
func
the_consequent_of H ->
ZF-formula means
:
Def36: ex H1 st H
= (H1
=> it );
existence by
A1;
uniqueness by
Th32;
end
theorem ::
ZF_LANG:46
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 ::
ZF_LANG:47
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;
::
ZF_LANG:def37
func
the_left_side_of H ->
ZF-formula means
:
Def37: ex H1 st H
= (it
<=> H1);
existence by
A1;
uniqueness by
Th33;
::
ZF_LANG:def38
func
the_right_side_of H ->
ZF-formula means
:
Def38: ex H1 st H
= (H1
<=> it );
existence by
A1;
uniqueness by
Th33;
end
theorem ::
ZF_LANG:48
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 ::
ZF_LANG:49
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;
definition
let H, F;
::
ZF_LANG:def39
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 ::
ZF_LANG:50
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 ::
ZF_LANG:51
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 ::
ZF_LANG:52
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 ::
ZF_LANG:53
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 ::
ZF_LANG:54
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 ::
ZF_LANG:55
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 ::
ZF_LANG:56
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 ::
ZF_LANG:57
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 ::
ZF_LANG:58
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;
reserve L,L9 for
FinSequence;
definition
let H, F;
::
ZF_LANG:def40
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 holds ex H1, F1 st (L
. k)
= H1 & (L
. (k
+ 1))
= F1 & H1
is_immediate_constituent_of F1;
end
theorem ::
ZF_LANG:59
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 by
FINSEQ_1:def 8;
thus thesis;
end;
definition
let H, F;
::
ZF_LANG:def41
pred H
is_proper_subformula_of F means H
is_subformula_of F & H
<> F;
end
theorem ::
ZF_LANG:60
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 ::
ZF_LANG:61
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 by
FINSEQ_1: 44;
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 by
FINSEQ_1: 44;
thus thesis by
A1;
end;
assume H
= F;
then (
len H)
= (
len F);
hence contradiction by
A1,
Th60;
end;
theorem ::
ZF_LANG:62
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 holds 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 be
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,
NAT_1: 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 be
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 ::
ZF_LANG:63
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 holds 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 ::
ZF_LANG:64
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 holds 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 holds 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 ::
ZF_LANG:65
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 ::
ZF_LANG:66
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 ::
ZF_LANG:67
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 ::
ZF_LANG:68
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 ::
ZF_LANG:69
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 holds 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 be
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 ::
ZF_LANG:70
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 holds 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 be
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 ::
ZF_LANG:71
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 holds 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 be
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 ::
ZF_LANG:72
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 ::
ZF_LANG:73
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 ::
ZF_LANG:74
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 ::
ZF_LANG:75
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 ::
ZF_LANG:76
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 ::
ZF_LANG:77
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;
definition
let H;
::
ZF_LANG:def42
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 ::
ZF_LANG:78
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 ::
ZF_LANG:79
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 ::
ZF_LANG:80
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 ::
ZF_LANG:81
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 ::
ZF_LANG:82
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 ::
ZF_LANG:83
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 ::
ZF_LANG:84
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 ::
ZF_LANG:85
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 ::
ZF_LANG:86
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 ::
ZF_LANG:87
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 ::
ZF_LANG:88
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 ::
ZF_LANG:89
(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;
scheme ::
ZF_LANG:sch1
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];
defpred
Q[
Nat] means for H st (
len H)
= $1 holds P[H];
A5: for n be
Nat st for k be
Nat st k
< n holds
Q[k] holds
Q[n]
proof
let n be
Nat such that
A6: for k be
Nat st k
< n holds 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 be
Nat holds
Q[n] from
NAT_1:sch 4(
A5);
let H;
(
len H)
= (
len H);
hence thesis by
A15;
end;
scheme ::
ZF_LANG:sch2
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];
defpred
Q[
Nat] means for H st (
len H)
= $1 holds P[H];
A2: for n be
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 be
Nat st k
< n holds 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 be
Nat holds
Q[n] from
NAT_1:sch 4(
A2);
let H;
(
len H)
= (
len H);
hence thesis by
A5;
end;