:: ZF_LANG semantic presentation
begin
definition
func VAR -> Subset of NAT equals :: ZF_LANG:def 1
{ k where k is Element of NAT : 5 <= k } ;
coherence
{ k where k is Element of NAT : 5 <= k } is Subset of NAT
proof
set X = { k where k is Element of NAT : 5 <= k } ;
{ k where k is Element of NAT : 5 <= k } c= NAT
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : 5 <= k } or a in NAT )
assume a in { k where k is Element of NAT : 5 <= k } ; ::_thesis: a in NAT
then ex k being Element of NAT st
( a = k & 5 <= k ) ;
hence a in NAT ; ::_thesis: verum
end;
hence { k where k is Element of NAT : 5 <= k } is Subset of NAT ; ::_thesis: verum
end;
end;
:: deftheorem defines VAR ZF_LANG:def_1_:_
VAR = { k where k is Element of NAT : 5 <= k } ;
registration
cluster VAR -> non empty ;
coherence
not VAR is empty
proof
5 in { k where k is Element of NAT : 5 <= k } ;
hence not VAR is empty ; ::_thesis: verum
end;
end;
definition
mode Variable is Element of VAR ;
end;
definition
let n be Element of NAT ;
func x. n -> Variable equals :: ZF_LANG:def 2
5 + n;
coherence
5 + n is Variable
proof
set x = 5 + n;
5 <= 5 + n by NAT_1:11;
then 5 + n in { k where k is Element of NAT : 5 <= k } ;
hence 5 + n is Variable ; ::_thesis: verum
end;
end;
:: deftheorem defines x. ZF_LANG:def_2_:_
for n being Element of NAT holds x. n = 5 + n;
definition
let x be Variable;
:: original: <*
redefine func<*x*> -> FinSequence of NAT ;
coherence
<*x*> is FinSequence of NAT
proof
reconsider VAR9 = VAR as non empty Subset of NAT ;
reconsider x9 = x as Element of VAR9 ;
reconsider x9 = x9 as Element of NAT ;
<*x9*> is FinSequence of NAT ;
hence <*x*> is FinSequence of NAT ; ::_thesis: verum
end;
end;
definition
let x, y be Variable;
funcx '=' y -> FinSequence of NAT equals :: ZF_LANG:def 3
(<*0*> ^ <*x*>) ^ <*y*>;
coherence
(<*0*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;
funcx 'in' y -> FinSequence of NAT equals :: ZF_LANG:def 4
(<*1*> ^ <*x*>) ^ <*y*>;
coherence
(<*1*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ;
end;
:: deftheorem defines '=' ZF_LANG:def_3_:_
for x, y being Variable holds x '=' y = (<*0*> ^ <*x*>) ^ <*y*>;
:: deftheorem defines 'in' ZF_LANG:def_4_:_
for x, y being Variable holds x 'in' y = (<*1*> ^ <*x*>) ^ <*y*>;
theorem :: ZF_LANG:1
for x, y, z, t being Variable st x '=' y = z '=' t holds
( x = z & y = t )
proof
let x, y, z, t be Variable; ::_thesis: ( x '=' y = z '=' t implies ( x = z & y = t ) )
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 ; ::_thesis: ( x = z & y = t )
hence ( x = z & y = t ) by A1, A2, A4, A3, FINSEQ_1:33; ::_thesis: verum
end;
theorem :: ZF_LANG:2
for x, y, z, t being Variable st x 'in' y = z 'in' t holds
( x = z & y = t )
proof
let x, y, z, t be Variable; ::_thesis: ( x 'in' y = z 'in' t implies ( x = z & y = t ) )
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 ; ::_thesis: ( x = z & y = t )
hence ( x = z & y = t ) by A1, A2, A4, A3, FINSEQ_1:33; ::_thesis: verum
end;
definition
let p be FinSequence of NAT ;
func 'not' p -> FinSequence of NAT equals :: ZF_LANG:def 5
<*2*> ^ p;
coherence
<*2*> ^ p is FinSequence of NAT ;
let q be FinSequence of NAT ;
funcp '&' q -> FinSequence of NAT equals :: ZF_LANG:def 6
(<*3*> ^ p) ^ q;
coherence
(<*3*> ^ p) ^ q is FinSequence of NAT ;
end;
:: deftheorem defines 'not' ZF_LANG:def_5_:_
for p being FinSequence of NAT holds 'not' p = <*2*> ^ p;
:: deftheorem defines '&' ZF_LANG:def_6_:_
for p, q being FinSequence of NAT holds p '&' q = (<*3*> ^ p) ^ q;
definition
let x be Variable;
let p be FinSequence of NAT ;
func All (x,p) -> FinSequence of NAT equals :: ZF_LANG:def 7
(<*4*> ^ <*x*>) ^ p;
coherence
(<*4*> ^ <*x*>) ^ p is FinSequence of NAT ;
end;
:: deftheorem defines All ZF_LANG:def_7_:_
for x being Variable
for p being FinSequence of NAT holds All (x,p) = (<*4*> ^ <*x*>) ^ p;
theorem Th3: :: ZF_LANG:3
for p, q being FinSequence of NAT
for x, y being Variable st All (x,p) = All (y,q) holds
( x = y & p = q )
proof
let p, q be FinSequence of NAT ; ::_thesis: for x, y being Variable st All (x,p) = All (y,q) holds
( x = y & p = q )
let x, y be Variable; ::_thesis: ( All (x,p) = All (y,q) implies ( x = y & p = q ) )
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) ; ::_thesis: ( x = y & p = q )
hence x = y by A1, A2, FINSEQ_1:33; ::_thesis: p = q
<*x*> ^ p = <*y*> ^ q by A3, A1, FINSEQ_1:33;
hence p = q by A2, FINSEQ_1:33; ::_thesis: verum
end;
definition
func WFF -> non empty set means :Def8: :: ZF_LANG:def 8
( ( for a being set st a in it holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in it & x 'in' y in it ) ) & ( for p being FinSequence of NAT st p in it holds
'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds
p '&' q in it ) & ( for x being Variable
for p being FinSequence of NAT st p in it holds
All (x,p) in it ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
it c= D ) );
existence
ex b1 being non empty set st
( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
b1 c= D ) )
proof
defpred S1[ set ] means ( ( for a being set st a in $1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in $1 & x 'in' y in $1 ) ) & ( for p being FinSequence of NAT st p in $1 holds
'not' p in $1 ) & ( for p, q being FinSequence of NAT st p in $1 & q in $1 holds
p '&' q in $1 ) & ( for x being Variable
for p being FinSequence of NAT st p in $1 holds
All (x,p) in $1 ) );
defpred S2[ set ] means for D being non empty set st S1[D] holds
$1 in D;
consider Y being set such that
A1: for a being set holds
( a in Y iff ( a in NAT * & S2[a] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_ex_b_being_FinSequence_of_NAT_st_b_in_Y
set a = (x. 0) '=' (x. 0);
take b = (x. 0) '=' (x. 0); ::_thesis: b in Y
( (x. 0) '=' (x. 0) in NAT * & ( for D being non empty set st S1[D] holds
(x. 0) '=' (x. 0) in D ) ) by FINSEQ_1:def_11;
hence b in Y by A1; ::_thesis: verum
end;
then reconsider Y = Y as non empty set ;
take Y ; ::_thesis: ( ( for a being set st a in Y holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in Y & x 'in' y in Y ) ) & ( for p being FinSequence of NAT st p in Y holds
'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
Y c= D ) )
thus for a being set st a in Y holds
a is FinSequence of NAT ::_thesis: ( ( for x, y being Variable holds
( x '=' y in Y & x 'in' y in Y ) ) & ( for p being FinSequence of NAT st p in Y holds
'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
Y c= D ) )
proof
let a be set ; ::_thesis: ( a in Y implies a is FinSequence of NAT )
assume a in Y ; ::_thesis: a is FinSequence of NAT
then a in NAT * by A1;
hence a is FinSequence of NAT by FINSEQ_1:def_11; ::_thesis: verum
end;
thus for x, y being Variable holds
( x '=' y in Y & x 'in' y in Y ) ::_thesis: ( ( for p being FinSequence of NAT st p in Y holds
'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
Y c= D ) )
proof
let x, y be Variable; ::_thesis: ( x '=' y in Y & x 'in' y in Y )
( x '=' y in NAT * & ( for D being non empty set st S1[D] holds
x '=' y in D ) ) by FINSEQ_1:def_11;
hence x '=' y in Y by A1; ::_thesis: x 'in' y in Y
( x 'in' y in NAT * & ( for D being non empty set st S1[D] holds
x 'in' y in D ) ) by FINSEQ_1:def_11;
hence x 'in' y in Y by A1; ::_thesis: verum
end;
thus for p being FinSequence of NAT st p in Y holds
'not' p in Y ::_thesis: ( ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
Y c= D ) )
proof
let p be FinSequence of NAT ; ::_thesis: ( p in Y implies 'not' p in Y )
assume A2: p in Y ; ::_thesis: 'not' p in Y
A3: for D being non empty set st S1[D] holds
'not' p in D
proof
let D be non empty set ; ::_thesis: ( S1[D] implies 'not' p in D )
assume A4: S1[D] ; ::_thesis: 'not' p in D
then p in D by A1, A2;
hence 'not' p in D by A4; ::_thesis: verum
end;
'not' p in NAT * by FINSEQ_1:def_11;
hence 'not' p in Y by A1, A3; ::_thesis: verum
end;
thus for q, p being FinSequence of NAT st q in Y & p in Y holds
q '&' p in Y ::_thesis: ( ( for x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
Y c= D ) )
proof
let q, p be FinSequence of NAT ; ::_thesis: ( q in Y & p in Y implies q '&' p in Y )
assume A5: ( q in Y & p in Y ) ; ::_thesis: q '&' p in Y
A6: for D being non empty set st S1[D] holds
q '&' p in D
proof
let D be non empty set ; ::_thesis: ( S1[D] implies q '&' p in D )
assume A7: S1[D] ; ::_thesis: q '&' p in D
then ( p in D & q in D ) by A1, A5;
hence q '&' p in D by A7; ::_thesis: verum
end;
q '&' p in NAT * by FINSEQ_1:def_11;
hence q '&' p in Y by A1, A6; ::_thesis: verum
end;
thus for x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y ::_thesis: for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
Y c= D
proof
let x be Variable; ::_thesis: for p being FinSequence of NAT st p in Y holds
All (x,p) in Y
let p be FinSequence of NAT ; ::_thesis: ( p in Y implies All (x,p) in Y )
assume A8: p in Y ; ::_thesis: All (x,p) in Y
A9: for D being non empty set st S1[D] holds
All (x,p) in D
proof
let D be non empty set ; ::_thesis: ( S1[D] implies All (x,p) in D )
assume A10: S1[D] ; ::_thesis: All (x,p) in D
then p in D by A1, A8;
hence All (x,p) in D by A10; ::_thesis: verum
end;
All (x,p) in NAT * by FINSEQ_1:def_11;
hence All (x,p) in Y by A1, A9; ::_thesis: verum
end;
let D be non empty set ; ::_thesis: ( ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) implies Y c= D )
assume A11: S1[D] ; ::_thesis: Y c= D
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in D )
assume a in Y ; ::_thesis: a in D
hence a in D by A1, A11; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty set st ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
b1 c= D ) & ( for a being set st a in b2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b2 & x 'in' y in b2 ) ) & ( for p being FinSequence of NAT st p in b2 holds
'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds
p '&' q in b2 ) & ( for x being Variable
for p being FinSequence of NAT st p in b2 holds
All (x,p) in b2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
b2 c= D ) holds
b1 = b2
proof
let D1, D2 be non empty set ; ::_thesis: ( ( for a being set st a in D1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D1 & x 'in' y in D1 ) ) & ( for p being FinSequence of NAT st p in D1 holds
'not' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p '&' q in D1 ) & ( for x being Variable
for p being FinSequence of NAT st p in D1 holds
All (x,p) in D1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D2 & x 'in' y in D2 ) ) & ( for p being FinSequence of NAT st p in D2 holds
'not' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p '&' q in D2 ) & ( for x being Variable
for p being FinSequence of NAT st p in D2 holds
All (x,p) in D2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
D2 c= D ) implies D1 = D2 )
assume ( ( for a being set st a in D1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D1 & x 'in' y in D1 ) ) & ( for p being FinSequence of NAT st p in D1 holds
'not' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p '&' q in D1 ) & ( for x being Variable
for p being FinSequence of NAT st p in D1 holds
All (x,p) in D1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D2 & x 'in' y in D2 ) ) & ( for p being FinSequence of NAT st p in D2 holds
'not' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p '&' q in D2 ) & ( for x being Variable
for p being FinSequence of NAT st p in D2 holds
All (x,p) in D2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
D2 c= D ) ) ; ::_thesis: D1 = D2
then ( D1 c= D2 & D2 c= D1 ) ;
hence D1 = D2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines WFF ZF_LANG:def_8_:_
for b1 being non empty set holds
( b1 = WFF iff ( ( for a being set st a in b1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds
'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds
p '&' q in b1 ) & ( for x being Variable
for p being FinSequence of NAT st p in b1 holds
All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
b1 c= D ) ) );
definition
let IT be FinSequence of NAT ;
attrIT is ZF-formula-like means :Def9: :: ZF_LANG:def 9
IT is Element of WFF ;
end;
:: deftheorem Def9 defines ZF-formula-like ZF_LANG:def_9_:_
for IT being FinSequence of NAT holds
( IT is ZF-formula-like iff IT is Element of WFF );
registration
cluster Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like ZF-formula-like for FinSequence of NAT ;
existence
ex b1 being FinSequence of NAT st b1 is ZF-formula-like
proof
set x = the Element of WFF ;
reconsider x = the Element of WFF as FinSequence of NAT by Def8;
take x ; ::_thesis: x is ZF-formula-like
thus x is Element of WFF ; :: according to ZF_LANG:def_9 ::_thesis: verum
end;
end;
definition
mode ZF-formula is ZF-formula-like FinSequence of NAT ;
end;
theorem :: ZF_LANG:4
for a being set holds
( a is ZF-formula iff a in WFF )
proof
let a be set ; ::_thesis: ( a is ZF-formula iff a in WFF )
thus ( a is ZF-formula implies a in WFF ) ::_thesis: ( a in WFF implies a is ZF-formula )
proof
assume a is ZF-formula ; ::_thesis: a in WFF
then a is Element of WFF by Def9;
hence a in WFF ; ::_thesis: verum
end;
assume a in WFF ; ::_thesis: a is ZF-formula
hence a is ZF-formula by Def8, Def9; ::_thesis: verum
end;
registration
let x, y be Variable;
clusterx '=' y -> ZF-formula-like ;
coherence
x '=' y is ZF-formula-like
proof
x '=' y is Element of WFF by Def8;
hence x '=' y is ZF-formula-like by Def9; ::_thesis: verum
end;
clusterx 'in' y -> ZF-formula-like ;
coherence
x 'in' y is ZF-formula-like
proof
x 'in' y is Element of WFF by Def8;
hence x 'in' y is ZF-formula-like by Def9; ::_thesis: verum
end;
end;
registration
let H be ZF-formula;
cluster 'not' H -> ZF-formula-like ;
coherence
'not' H is ZF-formula-like
proof
H is Element of WFF by Def9;
then 'not' H is Element of WFF by Def8;
hence 'not' H is ZF-formula-like by Def9; ::_thesis: verum
end;
let G be ZF-formula;
clusterH '&' G -> ZF-formula-like ;
coherence
H '&' G is ZF-formula-like
proof
( H is Element of WFF & G is Element of WFF ) by Def9;
then H '&' G is Element of WFF by Def8;
hence H '&' G is ZF-formula-like by Def9; ::_thesis: verum
end;
end;
registration
let x be Variable;
let H be ZF-formula;
cluster All (x,H) -> ZF-formula-like ;
coherence
All (x,H) is ZF-formula-like
proof
H is Element of WFF by Def9;
then All (x,H) is Element of WFF by Def8;
hence All (x,H) is ZF-formula-like by Def9; ::_thesis: verum
end;
end;
definition
let H be ZF-formula;
attrH is being_equality means :Def10: :: ZF_LANG:def 10
ex x, y being Variable st H = x '=' y;
attrH is being_membership means :Def11: :: ZF_LANG:def 11
ex x, y being Variable st H = x 'in' y;
attrH is negative means :Def12: :: ZF_LANG:def 12
ex H1 being ZF-formula st H = 'not' H1;
attrH is conjunctive means :Def13: :: ZF_LANG:def 13
ex F, G being ZF-formula st H = F '&' G;
attrH is universal means :Def14: :: ZF_LANG:def 14
ex x being Variable ex H1 being ZF-formula st H = All (x,H1);
end;
:: deftheorem Def10 defines being_equality ZF_LANG:def_10_:_
for H being ZF-formula holds
( H is being_equality iff ex x, y being Variable st H = x '=' y );
:: deftheorem Def11 defines being_membership ZF_LANG:def_11_:_
for H being ZF-formula holds
( H is being_membership iff ex x, y being Variable st H = x 'in' y );
:: deftheorem Def12 defines negative ZF_LANG:def_12_:_
for H being ZF-formula holds
( H is negative iff ex H1 being ZF-formula st H = 'not' H1 );
:: deftheorem Def13 defines conjunctive ZF_LANG:def_13_:_
for H being ZF-formula holds
( H is conjunctive iff ex F, G being ZF-formula st H = F '&' G );
:: deftheorem Def14 defines universal ZF_LANG:def_14_:_
for H being ZF-formula holds
( H is universal iff ex x being Variable ex H1 being ZF-formula st H = All (x,H1) );
theorem :: ZF_LANG:5
for H being ZF-formula holds
( ( H is being_equality implies ex x, y being Variable st H = x '=' y ) & ( ex x, y being Variable st H = x '=' y implies H is being_equality ) & ( H is being_membership implies ex x, y being Variable st H = x 'in' y ) & ( ex x, y being Variable st H = x 'in' y implies H is being_membership ) & ( H is negative implies ex H1 being ZF-formula st H = 'not' H1 ) & ( ex H1 being ZF-formula st H = 'not' H1 implies H is negative ) & ( H is conjunctive implies ex F, G being ZF-formula st H = F '&' G ) & ( ex F, G being ZF-formula st H = F '&' G implies H is conjunctive ) & ( H is universal implies ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = All (x,H1) implies H is universal ) ) by Def10, Def11, Def12, Def13, Def14;
definition
let H be ZF-formula;
attrH is atomic means :Def15: :: ZF_LANG:def 15
( H is being_equality or H is being_membership );
end;
:: deftheorem Def15 defines atomic ZF_LANG:def_15_:_
for H being ZF-formula holds
( H is atomic iff ( H is being_equality or H is being_membership ) );
definition
let F, G be ZF-formula;
funcF 'or' G -> ZF-formula equals :: ZF_LANG:def 16
'not' (('not' F) '&' ('not' G));
coherence
'not' (('not' F) '&' ('not' G)) is ZF-formula ;
funcF => G -> ZF-formula equals :: ZF_LANG:def 17
'not' (F '&' ('not' G));
coherence
'not' (F '&' ('not' G)) is ZF-formula ;
end;
:: deftheorem defines 'or' ZF_LANG:def_16_:_
for F, G being ZF-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G));
:: deftheorem defines => ZF_LANG:def_17_:_
for F, G being ZF-formula holds F => G = 'not' (F '&' ('not' G));
definition
let F, G be ZF-formula;
funcF <=> G -> ZF-formula equals :: ZF_LANG:def 18
(F => G) '&' (G => F);
coherence
(F => G) '&' (G => F) is ZF-formula ;
end;
:: deftheorem defines <=> ZF_LANG:def_18_:_
for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F);
definition
let x be Variable;
let H be ZF-formula;
func Ex (x,H) -> ZF-formula equals :: ZF_LANG:def 19
'not' (All (x,('not' H)));
coherence
'not' (All (x,('not' H))) is ZF-formula ;
end;
:: deftheorem defines Ex ZF_LANG:def_19_:_
for x being Variable
for H being ZF-formula holds Ex (x,H) = 'not' (All (x,('not' H)));
definition
let H be ZF-formula;
attrH is disjunctive means :Def20: :: ZF_LANG:def 20
ex F, G being ZF-formula st H = F 'or' G;
attrH is conditional means :Def21: :: ZF_LANG:def 21
ex F, G being ZF-formula st H = F => G;
attrH is biconditional means :Def22: :: ZF_LANG:def 22
ex F, G being ZF-formula st H = F <=> G;
attrH is existential means :Def23: :: ZF_LANG:def 23
ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1);
end;
:: deftheorem Def20 defines disjunctive ZF_LANG:def_20_:_
for H being ZF-formula holds
( H is disjunctive iff ex F, G being ZF-formula st H = F 'or' G );
:: deftheorem Def21 defines conditional ZF_LANG:def_21_:_
for H being ZF-formula holds
( H is conditional iff ex F, G being ZF-formula st H = F => G );
:: deftheorem Def22 defines biconditional ZF_LANG:def_22_:_
for H being ZF-formula holds
( H is biconditional iff ex F, G being ZF-formula st H = F <=> G );
:: deftheorem Def23 defines existential ZF_LANG:def_23_:_
for H being ZF-formula holds
( H is existential iff ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) );
theorem :: ZF_LANG:6
for H being ZF-formula holds
( ( H is disjunctive implies ex F, G being ZF-formula st H = F 'or' G ) & ( ex F, G being ZF-formula st H = F 'or' G implies H is disjunctive ) & ( H is conditional implies ex F, G being ZF-formula st H = F => G ) & ( ex F, G being ZF-formula st H = F => G implies H is conditional ) & ( H is biconditional implies ex F, G being ZF-formula st H = F <=> G ) & ( ex F, G being ZF-formula st H = F <=> G implies H is biconditional ) & ( H is existential implies ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) implies H is existential ) ) by Def20, Def21, Def22, Def23;
definition
let x, y be Variable;
let H be ZF-formula;
func All (x,y,H) -> ZF-formula equals :: ZF_LANG:def 24
All (x,(All (y,H)));
coherence
All (x,(All (y,H))) is ZF-formula ;
func Ex (x,y,H) -> ZF-formula equals :: ZF_LANG:def 25
Ex (x,(Ex (y,H)));
coherence
Ex (x,(Ex (y,H))) is ZF-formula ;
end;
:: deftheorem defines All ZF_LANG:def_24_:_
for x, y being Variable
for H being ZF-formula holds All (x,y,H) = All (x,(All (y,H)));
:: deftheorem defines Ex ZF_LANG:def_25_:_
for x, y being Variable
for H being ZF-formula holds Ex (x,y,H) = Ex (x,(Ex (y,H)));
theorem :: ZF_LANG:7
for x, y being Variable
for H being ZF-formula holds
( All (x,y,H) = All (x,(All (y,H))) & Ex (x,y,H) = Ex (x,(Ex (y,H))) ) ;
definition
let x, y, z be Variable;
let H be ZF-formula;
func All (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 26
All (x,(All (y,z,H)));
coherence
All (x,(All (y,z,H))) is ZF-formula ;
func Ex (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 27
Ex (x,(Ex (y,z,H)));
coherence
Ex (x,(Ex (y,z,H))) is ZF-formula ;
end;
:: deftheorem defines All ZF_LANG:def_26_:_
for x, y, z being Variable
for H being ZF-formula holds All (x,y,z,H) = All (x,(All (y,z,H)));
:: deftheorem defines Ex ZF_LANG:def_27_:_
for x, y, z being Variable
for H being ZF-formula holds Ex (x,y,z,H) = Ex (x,(Ex (y,z,H)));
theorem :: ZF_LANG:8
for x, y, z being Variable
for H being ZF-formula holds
( All (x,y,z,H) = All (x,(All (y,z,H))) & Ex (x,y,z,H) = Ex (x,(Ex (y,z,H))) ) ;
theorem Th9: :: ZF_LANG:9
for H being ZF-formula holds
( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal )
proof
let H be ZF-formula; ::_thesis: ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal )
A1: H is Element of WFF by Def9;
assume A2: ( not H is being_equality & not H is being_membership & not H is negative & not H is conjunctive & not H is universal ) ; ::_thesis: contradiction
then (x. 0) '=' (x. 1) <> H by Def10;
then A3: not (x. 0) '=' (x. 1) in {H} by TARSKI:def_1;
A4: now__::_thesis:_for_x,_y_being_Variable_holds_
(_x_'='_y_in_WFF_\_{H}_&_x_'in'_y_in_WFF_\_{H}_)
let x, y be Variable; ::_thesis: ( x '=' y in WFF \ {H} & x 'in' y in WFF \ {H} )
x '=' y <> H by A2, Def10;
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; ::_thesis: x 'in' y in WFF \ {H}
x 'in' y <> H by A2, Def11;
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; ::_thesis: verum
end;
A7: now__::_thesis:_for_x_being_Variable
for_p_being_FinSequence_of_NAT_st_p_in_WFF_\_{H}_holds_
All_(x,p)_in_WFF_\_{H}
let x be Variable; ::_thesis: for p being FinSequence of NAT st p in WFF \ {H} holds
All (x,p) in WFF \ {H}
let p be FinSequence of NAT ; ::_thesis: ( p in WFF \ {H} implies All (x,p) in WFF \ {H} )
assume A8: p in WFF \ {H} ; ::_thesis: All (x,p) in WFF \ {H}
then reconsider H1 = p as ZF-formula by Def9;
All (x,H1) <> H by A2, Def14;
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; ::_thesis: verum
end;
A10: now__::_thesis:_for_p,_q_being_FinSequence_of_NAT_st_p_in_WFF_\_{H}_&_q_in_WFF_\_{H}_holds_
p_'&'_q_in_WFF_\_{H}
let p, q be FinSequence of NAT ; ::_thesis: ( p in WFF \ {H} & q in WFF \ {H} implies p '&' q in WFF \ {H} )
assume A11: ( p in WFF \ {H} & q in WFF \ {H} ) ; ::_thesis: p '&' q in WFF \ {H}
then reconsider F = p, G = q as ZF-formula by Def9;
F '&' G <> H by A2, Def13;
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; ::_thesis: verum
end;
A13: now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_WFF_\_{H}_holds_
'not'_p_in_WFF_\_{H}
let p be FinSequence of NAT ; ::_thesis: ( p in WFF \ {H} implies 'not' p in WFF \ {H} )
assume A14: p in WFF \ {H} ; ::_thesis: 'not' p in WFF \ {H}
then reconsider H1 = p as ZF-formula by Def9;
'not' H1 <> H by A2, Def12;
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; ::_thesis: verum
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 being set 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, TARSKI:def_3;
then not H in {H} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
theorem Th10: :: ZF_LANG:10
for H being ZF-formula holds
( H is atomic or H is negative or H is conjunctive or H is universal )
proof
let H be ZF-formula; ::_thesis: ( H is atomic or H is negative or H is conjunctive or H is universal )
assume ( not H is being_equality & not H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: ( H is negative or H is conjunctive or H is universal )
hence ( H is negative or H is conjunctive or H is universal ) by Th9; ::_thesis: verum
end;
theorem Th11: :: ZF_LANG:11
for H being ZF-formula st H is atomic holds
len H = 3
proof
let H be ZF-formula; ::_thesis: ( H is atomic implies len H = 3 )
A1: now__::_thesis:_(_H_is_being_equality_&_H_is_atomic_implies_len_H_=_3_)
assume H is being_equality ; ::_thesis: ( H is atomic implies len H = 3 )
then consider x, y being Variable such that
A2: H = x '=' y by Def10;
H = <*0,x,y*> by A2, FINSEQ_1:def_10;
hence ( H is atomic implies len H = 3 ) by FINSEQ_1:45; ::_thesis: verum
end;
A3: now__::_thesis:_(_H_is_being_membership_&_H_is_atomic_implies_len_H_=_3_)
assume H is being_membership ; ::_thesis: ( H is atomic implies len H = 3 )
then consider x, y being Variable such that
A4: H = x 'in' y by Def11;
H = <*1,x,y*> by A4, FINSEQ_1:def_10;
hence ( H is atomic implies len H = 3 ) by FINSEQ_1:45; ::_thesis: verum
end;
assume H is atomic ; ::_thesis: len H = 3
hence len H = 3 by A1, A3, Def15; ::_thesis: verum
end;
theorem Th12: :: ZF_LANG:12
for H being ZF-formula holds
( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )
proof
let H be ZF-formula; ::_thesis: ( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )
A1: now__::_thesis:_for_H_being_ZF-formula_st_H_is_universal_holds_
ex_H1_being_ZF-formula_st_(len_H1)_+_1_<=_len_H
let H be ZF-formula; ::_thesis: ( H is universal implies ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume H is universal ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then consider x being Variable, H1 being ZF-formula such that
A2: H = All (x,H1) by Def14;
take H1 = H1; ::_thesis: (len H1) + 1 <= len H
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; ::_thesis: verum
end;
A5: now__::_thesis:_for_H_being_ZF-formula_st_H_is_negative_holds_
ex_H1_being_ZF-formula_st_(len_H1)_+_1_<=_len_H
let H be ZF-formula; ::_thesis: ( H is negative implies ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume H is negative ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then consider H1 being ZF-formula such that
A6: H = 'not' H1 by Def12;
take H1 = H1; ::_thesis: (len H1) + 1 <= len H
len H = (len <*2*>) + (len H1) by A6, FINSEQ_1:22;
hence (len H1) + 1 <= len H by FINSEQ_1:40; ::_thesis: verum
end;
A7: now__::_thesis:_for_H_being_ZF-formula_st_H_is_conjunctive_holds_
ex_H1_being_ZF-formula_st_(len_H1)_+_1_<=_len_H
let H be ZF-formula; ::_thesis: ( H is conjunctive implies ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume H is conjunctive ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then consider H1, F1 being ZF-formula such that
A8: H = H1 '&' F1 by Def13;
take H1 = H1; ::_thesis: (len H1) + 1 <= len H
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; ::_thesis: verum
end;
assume not H is atomic ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then ( H is negative or H is conjunctive or H is universal ) by Th10;
hence ex H1 being ZF-formula st (len H1) + 1 <= len H by A5, A7, A1; ::_thesis: verum
end;
theorem Th13: :: ZF_LANG:13
for H being ZF-formula holds 3 <= len H
proof
let H be ZF-formula; ::_thesis: 3 <= len H
now__::_thesis:_(_not_H_is_atomic_implies_3_<=_len_H_)
assume not H is atomic ; ::_thesis: 3 <= len H
then consider H1 being ZF-formula such that
A1: (len H1) + 1 <= len H by Th12;
A2: now__::_thesis:_(_not_H1_is_atomic_implies_3_<=_len_H_)
assume not H1 is atomic ; ::_thesis: 3 <= len H
then consider F being ZF-formula such that
A3: (len F) + 1 <= len H1 by Th12;
A4: now__::_thesis:_(_not_F_is_atomic_implies_3_<=_len_H_)
assume not F is atomic ; ::_thesis: 3 <= len H
then consider F1 being ZF-formula such that
A5: (len F1) + 1 <= len F by Th12;
0 <= len F1 by NAT_1:2;
then 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 3 <= len H by A1, XXREAL_0:2; ::_thesis: verum
end;
A6: ((len F) + 1) + 1 <= (len H1) + 1 by A3, XREAL_1:7;
now__::_thesis:_(_F_is_atomic_implies_3_<=_len_H_)
assume F is atomic ; ::_thesis: 3 <= len H
then len F = 3 by Th11;
then (3 + 1) + 1 <= len H by A1, A6, XXREAL_0:2;
hence 3 <= len H by XXREAL_0:2; ::_thesis: verum
end;
hence 3 <= len H by A4; ::_thesis: verum
end;
now__::_thesis:_(_H1_is_atomic_implies_3_<=_len_H_)
assume H1 is atomic ; ::_thesis: 3 <= len H
then 3 + 1 <= len H by A1, Th11;
hence 3 <= len H by XXREAL_0:2; ::_thesis: verum
end;
hence 3 <= len H by A2; ::_thesis: verum
end;
hence 3 <= len H by Th11; ::_thesis: verum
end;
theorem :: ZF_LANG:14
for H being ZF-formula st len H = 3 holds
H is atomic
proof
let H be ZF-formula; ::_thesis: ( len H = 3 implies H is atomic )
assume A1: len H = 3 ; ::_thesis: H is atomic
assume not H is atomic ; ::_thesis: contradiction
then consider H1 being ZF-formula 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; ::_thesis: verum
end;
theorem Th15: :: ZF_LANG:15
for x, y being Variable holds
( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 )
proof
let x, y be Variable; ::_thesis: ( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 )
thus (x '=' y) . 1 = (<*0*> ^ (<*x*> ^ <*y*>)) . 1 by FINSEQ_1:32
.= 0 by FINSEQ_1:41 ; ::_thesis: (x 'in' y) . 1 = 1
thus (x 'in' y) . 1 = (<*1*> ^ (<*x*> ^ <*y*>)) . 1 by FINSEQ_1:32
.= 1 by FINSEQ_1:41 ; ::_thesis: verum
end;
theorem Th16: :: ZF_LANG:16
for F, G being ZF-formula holds (F '&' G) . 1 = 3
proof
let F, G be ZF-formula; ::_thesis: (F '&' G) . 1 = 3
thus (F '&' G) . 1 = (<*3*> ^ (F ^ G)) . 1 by FINSEQ_1:32
.= 3 by FINSEQ_1:41 ; ::_thesis: verum
end;
theorem Th17: :: ZF_LANG:17
for x being Variable
for H being ZF-formula holds (All (x,H)) . 1 = 4
proof
let x be Variable; ::_thesis: for H being ZF-formula holds (All (x,H)) . 1 = 4
let H be ZF-formula; ::_thesis: (All (x,H)) . 1 = 4
thus (All (x,H)) . 1 = (<*4*> ^ (<*x*> ^ H)) . 1 by FINSEQ_1:32
.= 4 by FINSEQ_1:41 ; ::_thesis: verum
end;
theorem Th18: :: ZF_LANG:18
for H being ZF-formula st H is being_equality holds
H . 1 = 0
proof
let H be ZF-formula; ::_thesis: ( H is being_equality implies H . 1 = 0 )
assume H is being_equality ; ::_thesis: H . 1 = 0
then consider x, y being Variable such that
A1: H = x '=' y by Def10;
H = <*0,x,y*> by A1, FINSEQ_1:def_10;
hence H . 1 = 0 by FINSEQ_1:45; ::_thesis: verum
end;
theorem Th19: :: ZF_LANG:19
for H being ZF-formula st H is being_membership holds
H . 1 = 1
proof
let H be ZF-formula; ::_thesis: ( H is being_membership implies H . 1 = 1 )
assume H is being_membership ; ::_thesis: H . 1 = 1
then consider x, y being Variable such that
A1: H = x 'in' y by Def11;
H = <*1,x,y*> by A1, FINSEQ_1:def_10;
hence H . 1 = 1 by FINSEQ_1:45; ::_thesis: verum
end;
theorem Th20: :: ZF_LANG:20
for H being ZF-formula st H is negative holds
H . 1 = 2
proof
let H be ZF-formula; ::_thesis: ( H is negative implies H . 1 = 2 )
assume H is negative ; ::_thesis: H . 1 = 2
then ex H1 being ZF-formula st H = 'not' H1 by Def12;
hence H . 1 = 2 by FINSEQ_1:41; ::_thesis: verum
end;
theorem Th21: :: ZF_LANG:21
for H being ZF-formula st H is conjunctive holds
H . 1 = 3
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive implies H . 1 = 3 )
assume H is conjunctive ; ::_thesis: H . 1 = 3
then consider F, G being ZF-formula such that
A1: H = F '&' G by Def13;
(<*3*> ^ F) ^ G = <*3*> ^ (F ^ G) by FINSEQ_1:32;
hence H . 1 = 3 by A1, FINSEQ_1:41; ::_thesis: verum
end;
theorem Th22: :: ZF_LANG:22
for H being ZF-formula st H is universal holds
H . 1 = 4
proof
let H be ZF-formula; ::_thesis: ( H is universal implies H . 1 = 4 )
assume H is universal ; ::_thesis: H . 1 = 4
then consider x being Variable, H1 being ZF-formula such that
A1: H = All (x,H1) by Def14;
(<*4*> ^ <*x*>) ^ H1 = <*4*> ^ (<*x*> ^ H1) by FINSEQ_1:32;
hence H . 1 = 4 by A1, FINSEQ_1:41; ::_thesis: verum
end;
theorem Th23: :: ZF_LANG:23
for H being ZF-formula holds
( ( 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
let H be ZF-formula; ::_thesis: ( ( 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 ) )
percases ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal ) by Th9;
case H is being_equality ; ::_thesis: H . 1 = 0
hence H . 1 = 0 by Th18; ::_thesis: verum
end;
case H is being_membership ; ::_thesis: H . 1 = 1
hence H . 1 = 1 by Th19; ::_thesis: verum
end;
case H is negative ; ::_thesis: H . 1 = 2
hence H . 1 = 2 by Th20; ::_thesis: verum
end;
case H is conjunctive ; ::_thesis: H . 1 = 3
hence H . 1 = 3 by Th21; ::_thesis: verum
end;
case H is universal ; ::_thesis: H . 1 = 4
hence H . 1 = 4 by Th22; ::_thesis: verum
end;
end;
end;
theorem :: ZF_LANG:24
for H being ZF-formula st H . 1 = 0 holds
H is being_equality by Th23;
theorem :: ZF_LANG:25
for H being ZF-formula st H . 1 = 1 holds
H is being_membership by Th23;
theorem :: ZF_LANG:26
for H being ZF-formula st H . 1 = 2 holds
H is negative by Th23;
theorem :: ZF_LANG:27
for H being ZF-formula st H . 1 = 3 holds
H is conjunctive by Th23;
theorem :: ZF_LANG:28
for H being ZF-formula st H . 1 = 4 holds
H is universal by Th23;
theorem Th29: :: ZF_LANG:29
for H, F being ZF-formula
for sq being FinSequence st H = F ^ sq holds
H = F
proof
let H, F be ZF-formula; ::_thesis: for sq being FinSequence st H = F ^ sq holds
H = F
let sq be FinSequence; ::_thesis: ( H = F ^ sq implies H = F )
defpred S1[ Nat] means for H, F being ZF-formula
for sq being FinSequence st len H = $1 & H = F ^ sq holds
H = F;
for n being Nat st ( for k being Nat st k < n holds
for H, F being ZF-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) holds
for H, F being ZF-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
for H, F being ZF-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ) implies for H, F being ZF-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F )
assume A1: for k being Nat st k < n holds
for H, F being ZF-formula
for sq being FinSequence st len H = k & H = F ^ sq holds
H = F ; ::_thesis: for H, F being ZF-formula
for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let H, F be ZF-formula; ::_thesis: for sq being FinSequence st len H = n & H = F ^ sq holds
H = F
let sq be FinSequence; ::_thesis: ( len H = n & H = F ^ sq implies H = F )
assume that
A2: len H = n and
A3: H = F ^ sq ; ::_thesis: H = F
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__::_thesis:_(_H_is_negative_implies_H_=_F_)
A6: len <*2*> = 1 by FINSEQ_1:40;
assume A7: H is negative ; ::_thesis: H = F
then consider H1 being ZF-formula such that
A8: H = 'not' H1 by Def12;
(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 being ZF-formula such that
A9: F = 'not' F1 by Def12;
(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 H = F by A1, A2, A8, A9, A10; ::_thesis: verum
end;
A11: now__::_thesis:_(_H_is_conjunctive_implies_H_=_F_)
assume A12: H is conjunctive ; ::_thesis: H = F
then consider G1, G being ZF-formula such that
A13: H = G1 '&' G by Def13;
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 being ZF-formula such that
A17: F = F1 '&' H1 by Def13;
A18: now__::_thesis:_(_ex_sq9_being_FinSequence_st_F1_=_G1_^_sq9_implies_F1_=_G1_)
A19: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ;
given sq9 being FinSequence such that A20: F1 = G1 ^ sq9 ; ::_thesis: F1 = G1
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; ::_thesis: verum
end;
A22: ( (<*3*> ^ F1) ^ H1 = <*3*> ^ (F1 ^ H1) & (<*3*> ^ (F1 ^ H1)) ^ sq = <*3*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32;
A23: now__::_thesis:_(_ex_sq9_being_FinSequence_st_G1_=_F1_^_sq9_implies_G1_=_F1_)
given sq9 being FinSequence such that A24: G1 = F1 ^ sq9 ; ::_thesis: G1 = F1
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; ::_thesis: verum
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 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47;
then G = H1 ^ sq by A27, A23, A18, FINSEQ_1:33, FINSEQ_1:47;
hence H = F by A1, A2, A3, A17, A22, A26, A16; ::_thesis: verum
end;
A28: now__::_thesis:_(_H_is_universal_implies_H_=_F_)
assume A29: H is universal ; ::_thesis: H = F
then consider x being Variable, H1 being ZF-formula such that
A30: H = All (x,H1) by Def14;
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 being Variable, F1 being ZF-formula such that
A34: F = All (y,F1) by Def14;
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 H = F by A1, A2, A3, A34, A36, A33; ::_thesis: verum
end;
A37: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:22;
now__::_thesis:_(_H_is_atomic_implies_H_=_F_)
A38: 3 <= len F by Th13;
assume H is atomic ; ::_thesis: H = F
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 H = F by A3, FINSEQ_1:34; ::_thesis: verum
end;
hence H = F by A5, A28, A11, Th10; ::_thesis: verum
end;
then A40: for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k] ;
A41: for n being Nat holds S1[n] from NAT_1:sch_4(A40);
len H = len H ;
hence ( H = F ^ sq implies H = F ) by A41; ::_thesis: verum
end;
theorem Th30: :: ZF_LANG:30
for H, G, H1, G1 being ZF-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )
proof
let H, G, H1, G1 be ZF-formula; ::_thesis: ( H '&' G = H1 '&' G1 implies ( H = H1 & G = G1 ) )
assume A1: H '&' G = H1 '&' G1 ; ::_thesis: ( H = H1 & G = 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 being FinSequence st H = H1 ^ sq ) by FINSEQ_1:47;
A4: ( len H <= len H1 implies ex sq being FinSequence st H1 = H ^ sq ) by A2, FINSEQ_1:47;
hence H = H1 by A3, Th29; ::_thesis: G = G1
( ex sq being FinSequence st H1 = H ^ sq implies H1 = H ) by Th29;
hence G = G1 by A1, A3, A4, Th29, FINSEQ_1:33; ::_thesis: verum
end;
theorem Th31: :: ZF_LANG:31
for F, G, F1, G1 being ZF-formula st F 'or' G = F1 'or' G1 holds
( F = F1 & G = G1 )
proof
let F, G, F1, G1 be ZF-formula; ::_thesis: ( F 'or' G = F1 'or' G1 implies ( F = F1 & G = G1 ) )
assume F 'or' G = F1 'or' G1 ; ::_thesis: ( F = F1 & G = 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 ( F = F1 & G = G1 ) by FINSEQ_1:33; ::_thesis: verum
end;
theorem Th32: :: ZF_LANG:32
for F, G, F1, G1 being ZF-formula st F => G = F1 => G1 holds
( F = F1 & G = G1 )
proof
let F, G, F1, G1 be ZF-formula; ::_thesis: ( F => G = F1 => G1 implies ( F = F1 & G = G1 ) )
assume F => G = F1 => G1 ; ::_thesis: ( F = F1 & G = G1 )
then A1: F '&' ('not' G) = F1 '&' ('not' G1) by FINSEQ_1:33;
hence F = F1 by Th30; ::_thesis: G = G1
'not' G = 'not' G1 by A1, Th30;
hence G = G1 by FINSEQ_1:33; ::_thesis: verum
end;
theorem Th33: :: ZF_LANG:33
for F, G, F1, G1 being ZF-formula st F <=> G = F1 <=> G1 holds
( F = F1 & G = G1 )
proof
let F, G, F1, G1 be ZF-formula; ::_thesis: ( F <=> G = F1 <=> G1 implies ( F = F1 & G = G1 ) )
assume F <=> G = F1 <=> G1 ; ::_thesis: ( F = F1 & G = G1 )
then F => G = F1 => G1 by Th30;
hence ( F = F1 & G = G1 ) by Th32; ::_thesis: verum
end;
theorem Th34: :: ZF_LANG:34
for x, y being Variable
for H, G being ZF-formula st Ex (x,H) = Ex (y,G) holds
( x = y & H = G )
proof
let x, y be Variable; ::_thesis: for H, G being ZF-formula st Ex (x,H) = Ex (y,G) holds
( x = y & H = G )
let H, G be ZF-formula; ::_thesis: ( Ex (x,H) = Ex (y,G) implies ( x = y & H = G ) )
assume Ex (x,H) = Ex (y,G) ; ::_thesis: ( x = y & H = G )
then A1: All (x,('not' H)) = All (y,('not' G)) by FINSEQ_1:33;
then 'not' H = 'not' G by Th3;
hence ( x = y & H = G ) by A1, Th3, FINSEQ_1:33; ::_thesis: verum
end;
definition
let H be ZF-formula;
assume A1: H is atomic ;
func Var1 H -> Variable equals :Def28: :: ZF_LANG:def 28
H . 2;
coherence
H . 2 is Variable
proof
A2: ( ex x, y being Variable st H = x 'in' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
A3: ( ex x, y being Variable st H = x '=' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
( H is being_equality or H is being_membership ) by A1, Def15;
then consider k being Element of NAT , x, y being Variable such that
A4: H = (<*k*> ^ <*x*>) ^ <*y*> by A3, A2, Def10, Def11;
H = <*k,x,y*> by A4, FINSEQ_1:def_10;
hence H . 2 is Variable by FINSEQ_1:45; ::_thesis: verum
end;
func Var2 H -> Variable equals :Def29: :: ZF_LANG:def 29
H . 3;
coherence
H . 3 is Variable
proof
A5: ( ex x, y being Variable st H = x 'in' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
A6: ( ex x, y being Variable st H = x '=' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
( H is being_equality or H is being_membership ) by A1, Def15;
then consider k being Element of NAT , x, y being Variable such that
A7: H = (<*k*> ^ <*x*>) ^ <*y*> by A6, A5, Def10, Def11;
H = <*k,x,y*> by A7, FINSEQ_1:def_10;
hence H . 3 is Variable by FINSEQ_1:45; ::_thesis: verum
end;
end;
:: deftheorem Def28 defines Var1 ZF_LANG:def_28_:_
for H being ZF-formula st H is atomic holds
Var1 H = H . 2;
:: deftheorem Def29 defines Var2 ZF_LANG:def_29_:_
for H being ZF-formula st H is atomic holds
Var2 H = H . 3;
theorem :: ZF_LANG:35
for H being ZF-formula st H is atomic holds
( Var1 H = H . 2 & Var2 H = H . 3 ) by Def28, Def29;
theorem Th36: :: ZF_LANG:36
for H being ZF-formula st H is being_equality holds
H = (Var1 H) '=' (Var2 H)
proof
let H be ZF-formula; ::_thesis: ( H is being_equality implies H = (Var1 H) '=' (Var2 H) )
assume A1: H is being_equality ; ::_thesis: H = (Var1 H) '=' (Var2 H)
then consider x, y being Variable such that
A2: H = x '=' y by Def10;
(<*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, Def15;
then H . 2 = Var1 H by Def28;
hence H = (Var1 H) '=' (Var2 H) by A2, A4, A3, Def29; ::_thesis: verum
end;
theorem Th37: :: ZF_LANG:37
for H being ZF-formula st H is being_membership holds
H = (Var1 H) 'in' (Var2 H)
proof
let H be ZF-formula; ::_thesis: ( H is being_membership implies H = (Var1 H) 'in' (Var2 H) )
assume A1: H is being_membership ; ::_thesis: H = (Var1 H) 'in' (Var2 H)
then consider x, y being Variable such that
A2: H = x 'in' y by Def11;
(<*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, Def15;
then H . 2 = Var1 H by Def28;
hence H = (Var1 H) 'in' (Var2 H) by A2, A4, A3, Def29; ::_thesis: verum
end;
definition
let H be ZF-formula;
assume A1: H is negative ;
func the_argument_of H -> ZF-formula means :Def30: :: ZF_LANG:def 30
'not' it = H;
existence
ex b1 being ZF-formula st 'not' b1 = H by A1, Def12;
uniqueness
for b1, b2 being ZF-formula st 'not' b1 = H & 'not' b2 = H holds
b1 = b2 by FINSEQ_1:33;
end;
:: deftheorem Def30 defines the_argument_of ZF_LANG:def_30_:_
for H being ZF-formula st H is negative holds
for b2 being ZF-formula holds
( b2 = the_argument_of H iff 'not' b2 = H );
definition
let H be ZF-formula;
assume A1: ( H is conjunctive or H is disjunctive ) ;
func the_left_argument_of H -> ZF-formula means :Def31: :: ZF_LANG:def 31
ex H1 being ZF-formula st it '&' H1 = H if H is conjunctive
otherwise ex H1 being ZF-formula st it 'or' H1 = H;
existence
( ( H is conjunctive implies ex b1, H1 being ZF-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st b1 'or' H1 = H ) ) by A1, Def13, Def20;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is conjunctive & ex H1 being ZF-formula st b1 '&' H1 = H & ex H1 being ZF-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st b1 'or' H1 = H & ex H1 being ZF-formula st b2 'or' H1 = H implies b1 = b2 ) ) by Th30, Th31;
consistency
for b1 being ZF-formula holds verum ;
func the_right_argument_of H -> ZF-formula means :Def32: :: ZF_LANG:def 32
ex H1 being ZF-formula st H1 '&' it = H if H is conjunctive
otherwise ex H1 being ZF-formula st H1 'or' it = H;
existence
( ( H is conjunctive implies ex b1, H1 being ZF-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H ) )
proof
thus ( H is conjunctive implies ex G, H1 being ZF-formula st H1 '&' G = H ) ::_thesis: ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H )
proof
assume H is conjunctive ; ::_thesis: ex G, H1 being ZF-formula st H1 '&' G = H
then consider G, F being ZF-formula such that
A2: G '&' F = H by Def13;
take F ; ::_thesis: ex H1 being ZF-formula st H1 '&' F = H
thus ex H1 being ZF-formula st H1 '&' F = H by A2; ::_thesis: verum
end;
thus ( not H is conjunctive implies ex G, H1 being ZF-formula st H1 'or' G = H ) ::_thesis: verum
proof
assume not H is conjunctive ; ::_thesis: ex G, H1 being ZF-formula st H1 'or' G = H
then consider G, F being ZF-formula such that
A3: G 'or' F = H by A1, Def20;
take F ; ::_thesis: ex H1 being ZF-formula st H1 'or' F = H
thus ex H1 being ZF-formula st H1 'or' F = H by A3; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b1 = H & ex H1 being ZF-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st H1 'or' b1 = H & ex H1 being ZF-formula st H1 'or' b2 = H implies b1 = b2 ) ) by Th30, Th31;
consistency
for b1 being ZF-formula holds verum ;
end;
:: deftheorem Def31 defines the_left_argument_of ZF_LANG:def_31_:_
for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds
for b2 being ZF-formula holds
( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 '&' H1 = H ) ) & ( not H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 'or' H1 = H ) ) );
:: deftheorem Def32 defines the_right_argument_of ZF_LANG:def_32_:_
for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds
for b2 being ZF-formula holds
( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 '&' b2 = H ) ) & ( not H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 'or' b2 = H ) ) );
theorem :: ZF_LANG:38
for H, F being ZF-formula st H is conjunctive holds
( ( F = the_left_argument_of H implies ex G being ZF-formula st F '&' G = H ) & ( ex G being ZF-formula st F '&' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G '&' F = H ) & ( ex G being ZF-formula st G '&' F = H implies F = the_right_argument_of H ) ) by Def31, Def32;
theorem Th39: :: ZF_LANG:39
for H, F being ZF-formula st H is disjunctive holds
( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) )
proof
let H, F be ZF-formula; ::_thesis: ( H is disjunctive implies ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) )
assume A1: H is disjunctive ; ::_thesis: ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) )
then ex F, G being ZF-formula st H = F 'or' G by Def20;
then H . 1 = 2 by FINSEQ_1:41;
then not H is conjunctive by Th21;
hence ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) by A1, Def31, Def32; ::_thesis: verum
end;
theorem Th40: :: ZF_LANG:40
for H being ZF-formula st H is conjunctive holds
H = (the_left_argument_of H) '&' (the_right_argument_of H)
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive implies H = (the_left_argument_of H) '&' (the_right_argument_of H) )
assume A1: H is conjunctive ; ::_thesis: H = (the_left_argument_of H) '&' (the_right_argument_of H)
then ex F1 being ZF-formula st H = (the_left_argument_of H) '&' F1 by Def31;
hence H = (the_left_argument_of H) '&' (the_right_argument_of H) by A1, Def32; ::_thesis: verum
end;
theorem :: ZF_LANG:41
for H being ZF-formula st H is disjunctive holds
H = (the_left_argument_of H) 'or' (the_right_argument_of H)
proof
let H be ZF-formula; ::_thesis: ( H is disjunctive implies H = (the_left_argument_of H) 'or' (the_right_argument_of H) )
assume A1: H is disjunctive ; ::_thesis: H = (the_left_argument_of H) 'or' (the_right_argument_of H)
then ex F1 being ZF-formula st H = (the_left_argument_of H) 'or' F1 by Th39;
hence H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A1, Th39; ::_thesis: verum
end;
definition
let H be ZF-formula;
assume A1: ( H is universal or H is existential ) ;
func bound_in H -> Variable means :Def33: :: ZF_LANG:def 33
ex H1 being ZF-formula st All (it,H1) = H if H is universal
otherwise ex H1 being ZF-formula st Ex (it,H1) = H;
existence
( ( H is universal implies ex b1 being Variable ex H1 being ZF-formula st All (b1,H1) = H ) & ( not H is universal implies ex b1 being Variable ex H1 being ZF-formula st Ex (b1,H1) = H ) ) by A1, Def14, Def23;
uniqueness
for b1, b2 being Variable holds
( ( H is universal & ex H1 being ZF-formula st All (b1,H1) = H & ex H1 being ZF-formula st All (b2,H1) = H implies b1 = b2 ) & ( not H is universal & ex H1 being ZF-formula st Ex (b1,H1) = H & ex H1 being ZF-formula st Ex (b2,H1) = H implies b1 = b2 ) ) by Th3, Th34;
consistency
for b1 being Variable holds verum ;
func the_scope_of H -> ZF-formula means :Def34: :: ZF_LANG:def 34
ex x being Variable st All (x,it) = H if H is universal
otherwise ex x being Variable st Ex (x,it) = H;
existence
( ( H is universal implies ex b1 being ZF-formula ex x being Variable st All (x,b1) = H ) & ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex (x,b1) = H ) )
proof
thus ( H is universal implies ex H1 being ZF-formula ex x being Variable st All (x,H1) = H ) ::_thesis: ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex (x,b1) = H )
proof
assume H is universal ; ::_thesis: ex H1 being ZF-formula ex x being Variable st All (x,H1) = H
then consider x being Variable, G being ZF-formula such that
A2: All (x,G) = H by Def14;
take G ; ::_thesis: ex x being Variable st All (x,G) = H
thus ex x being Variable st All (x,G) = H by A2; ::_thesis: verum
end;
thus ( not H is universal implies ex H1 being ZF-formula ex x being Variable st Ex (x,H1) = H ) ::_thesis: verum
proof
assume not H is universal ; ::_thesis: ex H1 being ZF-formula ex x being Variable st Ex (x,H1) = H
then consider x being Variable, G being ZF-formula such that
A3: Ex (x,G) = H by A1, Def23;
take G ; ::_thesis: ex x being Variable st Ex (x,G) = H
thus ex x being Variable st Ex (x,G) = H by A3; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being ZF-formula holds
( ( H is universal & ex x being Variable st All (x,b1) = H & ex x being Variable st All (x,b2) = H implies b1 = b2 ) & ( not H is universal & ex x being Variable st Ex (x,b1) = H & ex x being Variable st Ex (x,b2) = H implies b1 = b2 ) ) by Th3, Th34;
consistency
for b1 being ZF-formula holds verum ;
end;
:: deftheorem Def33 defines bound_in ZF_LANG:def_33_:_
for H being ZF-formula st ( H is universal or H is existential ) holds
for b2 being Variable holds
( ( H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st All (b2,H1) = H ) ) & ( not H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st Ex (b2,H1) = H ) ) );
:: deftheorem Def34 defines the_scope_of ZF_LANG:def_34_:_
for H being ZF-formula st ( H is universal or H is existential ) holds
for b2 being ZF-formula holds
( ( H is universal implies ( b2 = the_scope_of H iff ex x being Variable st All (x,b2) = H ) ) & ( not H is universal implies ( b2 = the_scope_of H iff ex x being Variable st Ex (x,b2) = H ) ) );
theorem :: ZF_LANG:42
for x being Variable
for H, H1 being ZF-formula st H is universal holds
( ( x = bound_in H implies ex H1 being ZF-formula st All (x,H1) = H ) & ( ex H1 being ZF-formula st All (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st All (x,H1) = H ) & ( ex x being Variable st All (x,H1) = H implies H1 = the_scope_of H ) ) by Def33, Def34;
theorem Th43: :: ZF_LANG:43
for x being Variable
for H, H1 being ZF-formula st H is existential holds
( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) )
proof
let x be Variable; ::_thesis: for H, H1 being ZF-formula st H is existential holds
( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) )
let H, H1 be ZF-formula; ::_thesis: ( H is existential implies ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) )
assume A1: H is existential ; ::_thesis: ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) )
then ex y being Variable ex F being ZF-formula st H = Ex (y,F) by Def23;
then H . 1 = 2 by FINSEQ_1:41;
then not H is universal by Th22;
hence ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) by A1, Def33, Def34; ::_thesis: verum
end;
theorem Th44: :: ZF_LANG:44
for H being ZF-formula st H is universal holds
H = All ((bound_in H),(the_scope_of H))
proof
let H be ZF-formula; ::_thesis: ( H is universal implies H = All ((bound_in H),(the_scope_of H)) )
assume A1: H is universal ; ::_thesis: H = All ((bound_in H),(the_scope_of H))
then ex x being Variable st H = All (x,(the_scope_of H)) by Def34;
hence H = All ((bound_in H),(the_scope_of H)) by A1, Def33; ::_thesis: verum
end;
theorem :: ZF_LANG:45
for H being ZF-formula st H is existential holds
H = Ex ((bound_in H),(the_scope_of H))
proof
let H be ZF-formula; ::_thesis: ( H is existential implies H = Ex ((bound_in H),(the_scope_of H)) )
assume A1: H is existential ; ::_thesis: H = Ex ((bound_in H),(the_scope_of H))
then ex x being Variable st H = Ex (x,(the_scope_of H)) by Th43;
hence H = Ex ((bound_in H),(the_scope_of H)) by A1, Th43; ::_thesis: verum
end;
definition
let H be ZF-formula;
assume A1: H is conditional ;
func the_antecedent_of H -> ZF-formula means :Def35: :: ZF_LANG:def 35
ex H1 being ZF-formula st H = it => H1;
existence
ex b1, H1 being ZF-formula st H = b1 => H1 by A1, Def21;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 => H1 & ex H1 being ZF-formula st H = b2 => H1 holds
b1 = b2 by Th32;
func the_consequent_of H -> ZF-formula means :Def36: :: ZF_LANG:def 36
ex H1 being ZF-formula st H = H1 => it;
existence
ex b1, H1 being ZF-formula st H = H1 => b1
proof
consider F, G being ZF-formula such that
A2: H = F => G by A1, Def21;
take G ; ::_thesis: ex H1 being ZF-formula st H = H1 => G
take F ; ::_thesis: H = F => G
thus H = F => G by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 => b1 & ex H1 being ZF-formula st H = H1 => b2 holds
b1 = b2 by Th32;
end;
:: deftheorem Def35 defines the_antecedent_of ZF_LANG:def_35_:_
for H being ZF-formula st H is conditional holds
for b2 being ZF-formula holds
( b2 = the_antecedent_of H iff ex H1 being ZF-formula st H = b2 => H1 );
:: deftheorem Def36 defines the_consequent_of ZF_LANG:def_36_:_
for H being ZF-formula st H is conditional holds
for b2 being ZF-formula holds
( b2 = the_consequent_of H iff ex H1 being ZF-formula st H = H1 => b2 );
theorem :: ZF_LANG:46
for H, F being ZF-formula st H is conditional holds
( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36;
theorem :: ZF_LANG:47
for H being ZF-formula st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
proof
let H be ZF-formula; ::_thesis: ( H is conditional implies H = (the_antecedent_of H) => (the_consequent_of H) )
assume A1: H is conditional ; ::_thesis: H = (the_antecedent_of H) => (the_consequent_of H)
then ex F being ZF-formula st H = (the_antecedent_of H) => F by Def35;
hence H = (the_antecedent_of H) => (the_consequent_of H) by A1, Def36; ::_thesis: verum
end;
definition
let H be ZF-formula;
assume A1: H is biconditional ;
func the_left_side_of H -> ZF-formula means :Def37: :: ZF_LANG:def 37
ex H1 being ZF-formula st H = it <=> H1;
existence
ex b1, H1 being ZF-formula st H = b1 <=> H1 by A1, Def22;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 <=> H1 & ex H1 being ZF-formula st H = b2 <=> H1 holds
b1 = b2 by Th33;
func the_right_side_of H -> ZF-formula means :Def38: :: ZF_LANG:def 38
ex H1 being ZF-formula st H = H1 <=> it;
existence
ex b1, H1 being ZF-formula st H = H1 <=> b1
proof
consider F, G being ZF-formula such that
A2: H = F <=> G by A1, Def22;
take G ; ::_thesis: ex H1 being ZF-formula st H = H1 <=> G
take F ; ::_thesis: H = F <=> G
thus H = F <=> G by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 <=> b1 & ex H1 being ZF-formula st H = H1 <=> b2 holds
b1 = b2 by Th33;
end;
:: deftheorem Def37 defines the_left_side_of ZF_LANG:def_37_:_
for H being ZF-formula st H is biconditional holds
for b2 being ZF-formula holds
( b2 = the_left_side_of H iff ex H1 being ZF-formula st H = b2 <=> H1 );
:: deftheorem Def38 defines the_right_side_of ZF_LANG:def_38_:_
for H being ZF-formula st H is biconditional holds
for b2 being ZF-formula holds
( b2 = the_right_side_of H iff ex H1 being ZF-formula st H = H1 <=> b2 );
theorem :: ZF_LANG:48
for H, F being ZF-formula st H is biconditional holds
( ( F = the_left_side_of H implies ex G being ZF-formula st H = F <=> G ) & ( ex G being ZF-formula st H = F <=> G implies F = the_left_side_of H ) & ( F = the_right_side_of H implies ex G being ZF-formula st H = G <=> F ) & ( ex G being ZF-formula st H = G <=> F implies F = the_right_side_of H ) ) by Def37, Def38;
theorem :: ZF_LANG:49
for H being ZF-formula st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)
proof
let H be ZF-formula; ::_thesis: ( H is biconditional implies H = (the_left_side_of H) <=> (the_right_side_of H) )
assume A1: H is biconditional ; ::_thesis: H = (the_left_side_of H) <=> (the_right_side_of H)
then ex F being ZF-formula st H = (the_left_side_of H) <=> F by Def37;
hence H = (the_left_side_of H) <=> (the_right_side_of H) by A1, Def38; ::_thesis: verum
end;
definition
let H, F be ZF-formula;
predH is_immediate_constituent_of F means :Def39: :: ZF_LANG:def 39
( F = 'not' H or ex H1 being ZF-formula st
( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) );
end;
:: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def_39_:_
for H, F being ZF-formula holds
( H is_immediate_constituent_of F iff ( F = 'not' H or ex H1 being ZF-formula st
( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ) );
theorem Th50: :: ZF_LANG:50
for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x '=' y
proof
let x, y be Variable; ::_thesis: for H being ZF-formula holds not H is_immediate_constituent_of x '=' y
let H be ZF-formula; ::_thesis: not H is_immediate_constituent_of x '=' y
assume H is_immediate_constituent_of x '=' y ; ::_thesis: contradiction
then A1: ( x '=' y = 'not' H or ex H1 being ZF-formula st
( x '=' y = H '&' H1 or x '=' y = H1 '&' H ) or ex z being Variable st x '=' y = All (z,H) ) by Def39;
(x '=' y) . 1 = 0 by Th15;
hence contradiction by A1, Th16, Th17, FINSEQ_1:41; ::_thesis: verum
end;
theorem Th51: :: ZF_LANG:51
for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y
proof
let x, y be Variable; ::_thesis: for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y
let H be ZF-formula; ::_thesis: not H is_immediate_constituent_of x 'in' y
assume H is_immediate_constituent_of x 'in' y ; ::_thesis: contradiction
then A1: ( x 'in' y = 'not' H or ex H1 being ZF-formula st
( x 'in' y = H '&' H1 or x 'in' y = H1 '&' H ) or ex z being Variable st x 'in' y = All (z,H) ) by Def39;
(x 'in' y) . 1 = 1 by Th15;
hence contradiction by A1, Th16, Th17, FINSEQ_1:41; ::_thesis: verum
end;
theorem Th52: :: ZF_LANG:52
for F, H being ZF-formula holds
( F is_immediate_constituent_of 'not' H iff F = H )
proof
let F, H be ZF-formula; ::_thesis: ( F is_immediate_constituent_of 'not' H iff F = H )
thus ( F is_immediate_constituent_of 'not' H implies F = H ) ::_thesis: ( F = H implies F is_immediate_constituent_of 'not' H )
proof
A1: now__::_thesis:_for_x_being_Variable_holds_not_'not'_H_=_All_(x,F)
given x being Variable such that A2: 'not' H = All (x,F) ; ::_thesis: contradiction
('not' H) . 1 = 2 by FINSEQ_1:41;
hence contradiction by A2, Th17; ::_thesis: verum
end;
A3: now__::_thesis:_for_H1_being_ZF-formula_holds_
(_not_'not'_H_=_F_'&'_H1_&_not_'not'_H_=_H1_'&'_F_)
given H1 being ZF-formula such that A4: ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) ; ::_thesis: contradiction
('not' H) . 1 = 2 by FINSEQ_1:41;
hence contradiction by A4, Th16; ::_thesis: verum
end;
assume F is_immediate_constituent_of 'not' H ; ::_thesis: F = H
then ( 'not' H = 'not' F or ex H1 being ZF-formula st
( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) or ex x being Variable st 'not' H = All (x,F) ) by Def39;
hence F = H by A3, A1, FINSEQ_1:33; ::_thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of 'not' H ) by Def39; ::_thesis: verum
end;
theorem Th53: :: ZF_LANG:53
for F, G, H being ZF-formula holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
proof
let F, G, H be ZF-formula; ::_thesis: ( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
thus ( not F is_immediate_constituent_of G '&' H or F = G or F = H ) ::_thesis: ( ( F = G or F = H ) implies F is_immediate_constituent_of G '&' H )
proof
A1: now__::_thesis:_for_x_being_Variable_holds_not_G_'&'_H_=_All_(x,F)
given x being Variable such that A2: G '&' H = All (x,F) ; ::_thesis: contradiction
(G '&' H) . 1 = 3 by Th16;
hence contradiction by A2, Th17; ::_thesis: verum
end;
A3: now__::_thesis:_not_G_'&'_H_=_'not'_F
assume A4: G '&' H = 'not' F ; ::_thesis: contradiction
(G '&' H) . 1 = 3 by Th16;
hence contradiction by A4, FINSEQ_1:41; ::_thesis: verum
end;
assume F is_immediate_constituent_of G '&' H ; ::_thesis: ( F = G or F = H )
then ex H1 being ZF-formula st
( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) by A3, A1, Def39;
hence ( F = G or F = H ) by Th30; ::_thesis: verum
end;
assume ( F = G or F = H ) ; ::_thesis: F is_immediate_constituent_of G '&' H
hence F is_immediate_constituent_of G '&' H by Def39; ::_thesis: verum
end;
theorem Th54: :: ZF_LANG:54
for x being Variable
for F, H being ZF-formula holds
( F is_immediate_constituent_of All (x,H) iff F = H )
proof
let x be Variable; ::_thesis: for F, H being ZF-formula holds
( F is_immediate_constituent_of All (x,H) iff F = H )
let F, H be ZF-formula; ::_thesis: ( F is_immediate_constituent_of All (x,H) iff F = H )
thus ( F is_immediate_constituent_of All (x,H) implies F = H ) ::_thesis: ( F = H implies F is_immediate_constituent_of All (x,H) )
proof
A1: now__::_thesis:_for_G_being_ZF-formula_holds_
(_not_All_(x,H)_=_F_'&'_G_&_not_All_(x,H)_=_G_'&'_F_)
given G being ZF-formula such that A2: ( All (x,H) = F '&' G or All (x,H) = G '&' F ) ; ::_thesis: contradiction
( (F '&' G) . 1 = 3 & (G '&' F) . 1 = 3 ) by Th16;
hence contradiction by A2, Th17; ::_thesis: verum
end;
A3: now__::_thesis:_not_All_(x,H)_=_'not'_F
assume A4: All (x,H) = 'not' F ; ::_thesis: contradiction
(All (x,H)) . 1 = 4 by Th17;
hence contradiction by A4, FINSEQ_1:41; ::_thesis: verum
end;
assume F is_immediate_constituent_of All (x,H) ; ::_thesis: F = H
then ex y being Variable st All (x,H) = All (y,F) by A3, A1, Def39;
hence F = H by Th3; ::_thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of All (x,H) ) by Def39; ::_thesis: verum
end;
theorem :: ZF_LANG:55
for H, F being ZF-formula st H is atomic holds
not F is_immediate_constituent_of H
proof
let H, F be ZF-formula; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H )
A1: now__::_thesis:_(_H_is_being_equality_&_H_is_atomic_implies_not_F_is_immediate_constituent_of_H_)
assume H is being_equality ; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H )
then H = (Var1 H) '=' (Var2 H) by Th36;
hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th50; ::_thesis: verum
end;
A2: now__::_thesis:_(_H_is_being_membership_&_H_is_atomic_implies_not_F_is_immediate_constituent_of_H_)
assume H is being_membership ; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H )
then H = (Var1 H) 'in' (Var2 H) by Th37;
hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th51; ::_thesis: verum
end;
assume H is atomic ; ::_thesis: not F is_immediate_constituent_of H
hence not F is_immediate_constituent_of H by A1, A2, Def15; ::_thesis: verum
end;
theorem Th56: :: ZF_LANG:56
for H, F being ZF-formula st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )
proof
let H, F be ZF-formula; ::_thesis: ( H is negative implies ( F is_immediate_constituent_of H iff F = the_argument_of H ) )
assume H is negative ; ::_thesis: ( F is_immediate_constituent_of H iff F = the_argument_of H )
then H = 'not' (the_argument_of H) by Def30;
hence ( F is_immediate_constituent_of H iff F = the_argument_of H ) by Th52; ::_thesis: verum
end;
theorem Th57: :: ZF_LANG:57
for H, F being ZF-formula st H is conjunctive holds
( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )
proof
let H, F be ZF-formula; ::_thesis: ( H is conjunctive implies ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) )
assume H is conjunctive ; ::_thesis: ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th40;
hence ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) by Th53; ::_thesis: verum
end;
theorem Th58: :: ZF_LANG:58
for H, F being ZF-formula st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )
proof
let H, F be ZF-formula; ::_thesis: ( H is universal implies ( F is_immediate_constituent_of H iff F = the_scope_of H ) )
assume H is universal ; ::_thesis: ( F is_immediate_constituent_of H iff F = the_scope_of H )
then H = All ((bound_in H),(the_scope_of H)) by Th44;
hence ( F is_immediate_constituent_of H iff F = the_scope_of H ) by Th54; ::_thesis: verum
end;
definition
let H, F be ZF-formula;
predH is_subformula_of F means :Def40: :: ZF_LANG:def 40
ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) );
end;
:: deftheorem Def40 defines is_subformula_of ZF_LANG:def_40_:_
for H, F being ZF-formula holds
( H is_subformula_of F iff ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );
theorem Th59: :: ZF_LANG:59
for H being ZF-formula holds H is_subformula_of H
proof
let H be ZF-formula; ::_thesis: H is_subformula_of H
take 1 ; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st
( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take <*H*> ; ::_thesis: ( 1 <= 1 & len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus 1 <= 1 ; ::_thesis: ( len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus len <*H*> = 1 by FINSEQ_1:40; ::_thesis: ( <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus ( <*H*> . 1 = H & <*H*> . 1 = H ) by FINSEQ_1:def_8; ::_thesis: for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
thus for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; ::_thesis: verum
end;
definition
let H, F be ZF-formula;
predH is_proper_subformula_of F means :Def41: :: ZF_LANG:def 41
( H is_subformula_of F & H <> F );
end;
:: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def_41_:_
for H, F being ZF-formula holds
( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );
theorem Th60: :: ZF_LANG:60
for H, F being ZF-formula st H is_immediate_constituent_of F holds
len H < len F
proof
let H, F be ZF-formula; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F )
A1: now__::_thesis:_(_F_=_'not'_H_&_H_is_immediate_constituent_of_F_implies_len_H_<_len_F_)
assume F = 'not' H ; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F )
then len F = (len <*2*>) + (len H) by FINSEQ_1:22
.= (len H) + 1 by FINSEQ_1:40 ;
hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; ::_thesis: verum
end;
A2: now__::_thesis:_(_ex_H1_being_ZF-formula_st_
(_F_=_H_'&'_H1_or_F_=_H1_'&'_H_)_&_H_is_immediate_constituent_of_F_implies_len_H_<_len_F_)
given H1 being ZF-formula such that A3: ( F = H '&' H1 or F = H1 '&' H ) ; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F )
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 ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; ::_thesis: verum
end;
A5: now__::_thesis:_(_ex_x_being_Variable_st_F_=_All_(x,H)_&_H_is_immediate_constituent_of_F_implies_len_H_<_len_F_)
given x being Variable such that A6: F = All (x,H) ; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F )
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 ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; ::_thesis: verum
end;
assume H is_immediate_constituent_of F ; ::_thesis: len H < len F
hence len H < len F by A1, A2, A5, Def39; ::_thesis: verum
end;
theorem Th61: :: ZF_LANG:61
for H, F being ZF-formula st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
proof
let H, F be ZF-formula; ::_thesis: ( H is_immediate_constituent_of F implies H is_proper_subformula_of F )
assume A1: H is_immediate_constituent_of F ; ::_thesis: H is_proper_subformula_of F
thus H is_subformula_of F :: according to ZF_LANG:def_41 ::_thesis: H <> F
proof
take n = 2; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take L = <*H,F*>; ::_thesis: ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus 1 <= n ; ::_thesis: ( len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus len L = n by FINSEQ_1:44; ::_thesis: ( L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus ( L . 1 = H & L . n = F ) by FINSEQ_1:44; ::_thesis: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n implies ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that
A2: 1 <= k and
A3: k < n ; ::_thesis: ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
take H ; ::_thesis: ex F1 being ZF-formula st
( L . k = H & L . (k + 1) = F1 & H is_immediate_constituent_of F1 )
take F ; ::_thesis: ( L . k = H & L . (k + 1) = F & H is_immediate_constituent_of 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; ::_thesis: H is_immediate_constituent_of F
thus H is_immediate_constituent_of F by A1; ::_thesis: verum
end;
assume H = F ; ::_thesis: contradiction
then len H = len F ;
hence contradiction by A1, Th60; ::_thesis: verum
end;
theorem Th62: :: ZF_LANG:62
for H, F being ZF-formula st H is_proper_subformula_of F holds
len H < len F
proof
let H, F be ZF-formula; ::_thesis: ( H is_proper_subformula_of F implies len H < len F )
assume H is_subformula_of F ; :: according to ZF_LANG:def_41 ::_thesis: ( not H <> F or len H < len F )
then consider n being Element of NAT , L being FinSequence such that
A1: 1 <= n and
len L = n and
A2: L . 1 = H and
A3: L . n = F and
A4: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def40;
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 < n implies for H1 being ZF-formula st L . ($1 + 1) = H1 holds
len H < len H1 );
A5: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
A6: ( 1 <= k & k < n implies for H1 being ZF-formula st L . (k + 1) = H1 holds
len H < len H1 ) and
A7: 1 <= k + 1 and
A8: k + 1 < n ; ::_thesis: for H1 being ZF-formula st L . ((k + 1) + 1) = H1 holds
len H < len H1
consider F1, G being ZF-formula 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 be ZF-formula; ::_thesis: ( L . ((k + 1) + 1) = H1 implies len H < len H1 )
assume A11: L . ((k + 1) + 1) = H1 ; ::_thesis: len H < len H1
A12: now__::_thesis:_(_ex_m_being_Nat_st_k_=_m_+_1_implies_len_H_<_len_H1_)
given m being Nat such that A13: k = m + 1 ; ::_thesis: len H < len H1
len H < len F1 by A6, A8, A9, A13, NAT_1:11, NAT_1:13;
hence len H < len H1 by A11, A10, Th60, XXREAL_0:2; ::_thesis: verum
end;
( k = 0 implies len H < len H1 ) by A2, A11, A9, A10, Th60;
hence len H < len H1 by A12, NAT_1:6; ::_thesis: verum
end;
assume H <> F ; ::_thesis: len H < len F
then 1 < n by A1, A2, A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A14: n = 2 + k by NAT_1:10;
A15: S1[ 0 ] ;
A16: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A5);
reconsider k = 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 len H < len F by A3, A16, A14, A17, NAT_1:11; ::_thesis: verum
end;
theorem Th63: :: ZF_LANG:63
for H, F being ZF-formula st H is_proper_subformula_of F holds
ex G being ZF-formula st G is_immediate_constituent_of F
proof
let H, F be ZF-formula; ::_thesis: ( H is_proper_subformula_of F implies ex G being ZF-formula st G is_immediate_constituent_of F )
assume H is_subformula_of F ; :: according to ZF_LANG:def_41 ::_thesis: ( not H <> F or ex G being ZF-formula st G is_immediate_constituent_of F )
then consider n being Element of NAT , L being FinSequence such that
A1: 1 <= n and
len L = n and
A2: L . 1 = H and
A3: L . n = F and
A4: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def40;
assume H <> F ; ::_thesis: ex G being ZF-formula st G is_immediate_constituent_of F
then 1 < n by A1, A2, A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A5: n = 2 + k by NAT_1:10;
reconsider k = 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 being ZF-formula 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 ; ::_thesis: H1 is_immediate_constituent_of F
thus H1 is_immediate_constituent_of F by A3, A5, A6; ::_thesis: verum
end;
theorem Th64: :: ZF_LANG:64
for F, G, H being ZF-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H
proof
let F, G, H be ZF-formula; ::_thesis: ( F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H )
assume that
A1: F is_subformula_of G and
A2: F <> G and
A3: G is_subformula_of H and
A4: G <> H ; :: according to ZF_LANG:def_41 ::_thesis: F is_proper_subformula_of H
consider m being Element of NAT , L9 being FinSequence such that
A5: 1 <= m and
A6: len L9 = m and
A7: L9 . 1 = G and
A8: L9 . m = H and
A9: for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L9 . k = H1 & L9 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A3, Def40;
consider n being Element of NAT , L being FinSequence such that
A10: 1 <= n and
A11: len L = n and
A12: L . 1 = F and
A13: L . n = G and
A14: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40;
1 < n by A2, A10, A12, A13, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A15: n = 2 + k by NAT_1:10;
reconsider k = 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 :: according to ZF_LANG:def_41 ::_thesis: F <> H
proof
take l = (1 + k) + m; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st
( 1 <= l & len L = l & L . 1 = F & L . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take K = L1 ^ L9; ::_thesis: ( 1 <= l & len K = l & K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex H1, F1 being ZF-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A16: ((1 + k) + m) - (1 + k) = m ;
m <= m + (1 + k) by NAT_1:11;
hence 1 <= l by A5, XXREAL_0:2; ::_thesis: ( len K = l & K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex H1, F1 being ZF-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
(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; ::_thesis: ( K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex H1, F1 being ZF-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A20: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_1_+_k_holds_
K_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= 1 + k implies K . j = L . j )
assume ( 1 <= j & j <= 1 + k ) ; ::_thesis: K . j = L . j
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; ::_thesis: verum
end;
1 <= 1 + k by NAT_1:11;
hence K . 1 = F by A12, A20; ::_thesis: ( K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex H1, F1 being ZF-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
(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; ::_thesis: for k being Element of NAT st 1 <= k & k < l holds
ex H1, F1 being ZF-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < l implies ex H1, F1 being ZF-formula st
( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that
A22: 1 <= j and
A23: j < l ; ::_thesis: ex H1, F1 being ZF-formula st
( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
j + 0 <= j + 1 by XREAL_1:7;
then A24: 1 <= j + 1 by A22, XXREAL_0:2;
A25: now__::_thesis:_(_j_<_1_+_k_implies_ex_F1,_G1_being_ZF-formula_st_
(_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_)
assume A26: j < 1 + k ; ::_thesis: ex F1, G1 being ZF-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
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 being ZF-formula such that
A28: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A14, A22;
take F1 = F1; ::_thesis: ex G1 being ZF-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
thus ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A20, A22, A24, A26, A27, A28; ::_thesis: verum
end;
A29: now__::_thesis:_(_1_+_k_<_j_implies_ex_F1,_G1_being_ZF-formula_st_
(_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_)
A30: j + 1 <= l by A23, NAT_1:13;
assume A31: 1 + k < j ; ::_thesis: ex F1, G1 being ZF-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then A32: 1 + k < j + 1 by NAT_1:13;
(1 + k) + 1 <= j by A31, NAT_1:13;
then consider j1 being Nat such that
A33: j = ((1 + k) + 1) + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def_12;
j - (1 + k) < l - (1 + k) by A23, XREAL_1:9;
then consider F1, G1 being ZF-formula 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 = F1; ::_thesis: ex G1 being ZF-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of 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; ::_thesis: verum
end;
now__::_thesis:_(_j_=_1_+_k_implies_ex_F1,_G1_being_ZF-formula_st_
(_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_)
A36: ( j + 1 <= l & (j + 1) - j = (j + 1) + (- j) ) by A23, NAT_1:13;
assume A37: j = 1 + k ; ::_thesis: ex F1, G1 being ZF-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then j < (1 + k) + 1 by NAT_1:13;
then consider F1, G1 being ZF-formula such that
A38: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A14, A15, A22;
take F1 = F1; ::_thesis: ex G1 being ZF-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of 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; ::_thesis: verum
end;
hence ex H1, F1 being ZF-formula st
( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A25, A29, XXREAL_0:1; ::_thesis: verum
end;
assume A39: F = H ; ::_thesis: contradiction
F is_proper_subformula_of G by A1, A2, Def41;
then A40: len F < len G by Th62;
G is_proper_subformula_of H by A3, A4, Def41;
hence contradiction by A39, A40, Th62; ::_thesis: verum
end;
theorem Th65: :: ZF_LANG:65
for F, G, H being ZF-formula st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H
proof
let F, G, H be ZF-formula; ::_thesis: ( F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H )
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H ; ::_thesis: F is_subformula_of H
now__::_thesis:_(_F_<>_G_implies_F_is_subformula_of_H_)
assume F <> G ; ::_thesis: F is_subformula_of H
then A3: F is_proper_subformula_of G by A1, Def41;
now__::_thesis:_(_G_<>_H_implies_F_is_subformula_of_H_)
assume G <> H ; ::_thesis: F is_subformula_of H
then G is_proper_subformula_of H by A2, Def41;
then F is_proper_subformula_of H by A3, Th64;
hence F is_subformula_of H by Def41; ::_thesis: verum
end;
hence F is_subformula_of H by A1; ::_thesis: verum
end;
hence F is_subformula_of H by A2; ::_thesis: verum
end;
theorem :: ZF_LANG:66
for G, H being ZF-formula st G is_subformula_of H & H is_subformula_of G holds
G = H
proof
let G, H be ZF-formula; ::_thesis: ( G is_subformula_of H & H is_subformula_of G implies G = H )
assume that
A1: G is_subformula_of H and
A2: H is_subformula_of G ; ::_thesis: G = H
assume A3: G <> H ; ::_thesis: contradiction
then G is_proper_subformula_of H by A1, Def41;
then A4: len G < len H by Th62;
H is_proper_subformula_of G by A2, A3, Def41;
hence contradiction by A4, Th62; ::_thesis: verum
end;
theorem Th67: :: ZF_LANG:67
for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x '=' y
proof
let x, y be Variable; ::_thesis: for F being ZF-formula holds not F is_proper_subformula_of x '=' y
let F be ZF-formula; ::_thesis: not F is_proper_subformula_of x '=' y
assume F is_proper_subformula_of x '=' y ; ::_thesis: contradiction
then ex G being ZF-formula st G is_immediate_constituent_of x '=' y by Th63;
hence contradiction by Th50; ::_thesis: verum
end;
theorem Th68: :: ZF_LANG:68
for x, y being Variable
for F being ZF-formula holds not F is_proper_subformula_of x 'in' y
proof
let x, y be Variable; ::_thesis: for F being ZF-formula holds not F is_proper_subformula_of x 'in' y
let F be ZF-formula; ::_thesis: not F is_proper_subformula_of x 'in' y
assume F is_proper_subformula_of x 'in' y ; ::_thesis: contradiction
then ex G being ZF-formula st G is_immediate_constituent_of x 'in' y by Th63;
hence contradiction by Th51; ::_thesis: verum
end;
theorem Th69: :: ZF_LANG:69
for F, H being ZF-formula st F is_proper_subformula_of 'not' H holds
F is_subformula_of H
proof
let F, H be ZF-formula; ::_thesis: ( F is_proper_subformula_of 'not' H implies F is_subformula_of H )
assume that
A1: F is_subformula_of 'not' H and
A2: F <> 'not' H ; :: according to ZF_LANG:def_41 ::_thesis: F is_subformula_of H
consider n being Element of NAT , L being FinSequence 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 being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40;
1 < n by A2, A3, A5, A6, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A8: n = 2 + k by NAT_1:10;
reconsider k = 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; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus A9: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A4, A8, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A10: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_
L1_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j
then j in { j1 where j1 is Element of 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; ::_thesis: verum
end;
hence L1 . 1 = F by A5, A9; ::_thesis: ( L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
m < m + 1 by NAT_1:13;
then consider F1, G1 being ZF-formula 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; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that
A13: 1 <= j and
A14: j < m ; ::_thesis: ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
m <= m + 1 by NAT_1:11;
then j < n by A8, A14, XXREAL_0:2;
then consider F1, G1 being ZF-formula such that
A15: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A13;
take F1 ; ::_thesis: ex F1 being ZF-formula st
( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 )
take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A13, A14, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A10, A13, A14, A15; ::_thesis: verum
end;
theorem Th70: :: ZF_LANG:70
for F, G, H being ZF-formula holds
( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )
proof
let F, G, H be ZF-formula; ::_thesis: ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )
assume that
A1: F is_subformula_of G '&' H and
A2: F <> G '&' H ; :: according to ZF_LANG:def_41 ::_thesis: ( F is_subformula_of G or F is_subformula_of H )
consider n being Element of NAT , L being FinSequence 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 being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40;
1 < n by A2, A3, A5, A6, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A8: n = 2 + k by NAT_1:10;
reconsider k = 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 being ZF-formula 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; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus A11: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A4, A8, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A12: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_
L1_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j
then j in { j1 where j1 is Element of 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; ::_thesis: verum
end;
hence L1 . 1 = F by A5, A11; ::_thesis: ( L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus L1 . m = H1 by A9, A11, A12; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that
A13: 1 <= j and
A14: j < m ; ::_thesis: ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
m <= m + 1 by NAT_1:11;
then j < n by A8, A14, XXREAL_0:2;
then consider F1, G1 being ZF-formula such that
A15: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A13;
take F1 ; ::_thesis: ex F1 being ZF-formula st
( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 )
take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A13, A14, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A12, A13, A14, A15; ::_thesis: verum
end;
hence ( F is_subformula_of G or F is_subformula_of H ) by A6, A8, A10, Th53; ::_thesis: verum
end;
theorem Th71: :: ZF_LANG:71
for x being Variable
for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds
F is_subformula_of H
proof
let x be Variable; ::_thesis: for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds
F is_subformula_of H
let F, H be ZF-formula; ::_thesis: ( F is_proper_subformula_of All (x,H) implies F is_subformula_of H )
assume that
A1: F is_subformula_of All (x,H) and
A2: F <> All (x,H) ; :: according to ZF_LANG:def_41 ::_thesis: F is_subformula_of H
consider n being Element of NAT , L being FinSequence 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 being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40;
1 < n by A2, A3, A5, A6, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A8: n = 2 + k by NAT_1:10;
reconsider k = 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; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus A9: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A4, A8, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A10: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_
L1_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j
then j in { j1 where j1 is Element of 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; ::_thesis: verum
end;
hence L1 . 1 = F by A5, A9; ::_thesis: ( L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
m < m + 1 by NAT_1:13;
then consider F1, G1 being ZF-formula 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; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that
A13: 1 <= j and
A14: j < m ; ::_thesis: ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
m <= m + 1 by NAT_1:11;
then j < n by A8, A14, XXREAL_0:2;
then consider F1, G1 being ZF-formula such that
A15: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A13;
take F1 ; ::_thesis: ex F1 being ZF-formula st
( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 )
take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A13, A14, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A10, A13, A14, A15; ::_thesis: verum
end;
theorem :: ZF_LANG:72
for H, F being ZF-formula st H is atomic holds
not F is_proper_subformula_of H
proof
let H, F be ZF-formula; ::_thesis: ( H is atomic implies not F is_proper_subformula_of H )
assume H is atomic ; ::_thesis: not F is_proper_subformula_of H
then ( H is being_equality or H is being_membership ) by Def15;
then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th36, Th37;
hence not F is_proper_subformula_of H by Th67, Th68; ::_thesis: verum
end;
theorem :: ZF_LANG:73
for H being ZF-formula st H is negative holds
the_argument_of H is_proper_subformula_of H
proof
let H be ZF-formula; ::_thesis: ( H is negative implies the_argument_of H is_proper_subformula_of H )
assume H is negative ; ::_thesis: the_argument_of H is_proper_subformula_of H
then the_argument_of H is_immediate_constituent_of H by Th56;
hence the_argument_of H is_proper_subformula_of H by Th61; ::_thesis: verum
end;
theorem :: ZF_LANG:74
for H being ZF-formula st H is conjunctive holds
( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive implies ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) )
assume H is conjunctive ; ::_thesis: ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )
then ( the_left_argument_of H is_immediate_constituent_of H & the_right_argument_of H is_immediate_constituent_of H ) by Th57;
hence ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) by Th61; ::_thesis: verum
end;
theorem :: ZF_LANG:75
for H being ZF-formula st H is universal holds
the_scope_of H is_proper_subformula_of H
proof
let H be ZF-formula; ::_thesis: ( H is universal implies the_scope_of H is_proper_subformula_of H )
assume H is universal ; ::_thesis: the_scope_of H is_proper_subformula_of H
then the_scope_of H is_immediate_constituent_of H by Th58;
hence the_scope_of H is_proper_subformula_of H by Th61; ::_thesis: verum
end;
theorem Th76: :: ZF_LANG:76
for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x '=' y iff H = x '=' y )
proof
let x, y be Variable; ::_thesis: for H being ZF-formula holds
( H is_subformula_of x '=' y iff H = x '=' y )
let H be ZF-formula; ::_thesis: ( H is_subformula_of x '=' y iff H = x '=' y )
thus ( H is_subformula_of x '=' y implies H = x '=' y ) ::_thesis: ( H = x '=' y implies H is_subformula_of x '=' y )
proof
assume A1: H is_subformula_of x '=' y ; ::_thesis: H = x '=' y
assume H <> x '=' y ; ::_thesis: contradiction
then H is_proper_subformula_of x '=' y by A1, Def41;
then ex F being ZF-formula st F is_immediate_constituent_of x '=' y by Th63;
hence contradiction by Th50; ::_thesis: verum
end;
thus ( H = x '=' y implies H is_subformula_of x '=' y ) by Th59; ::_thesis: verum
end;
theorem Th77: :: ZF_LANG:77
for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x 'in' y iff H = x 'in' y )
proof
let x, y be Variable; ::_thesis: for H being ZF-formula holds
( H is_subformula_of x 'in' y iff H = x 'in' y )
let H be ZF-formula; ::_thesis: ( H is_subformula_of x 'in' y iff H = x 'in' y )
thus ( H is_subformula_of x 'in' y implies H = x 'in' y ) ::_thesis: ( H = x 'in' y implies H is_subformula_of x 'in' y )
proof
assume A1: H is_subformula_of x 'in' y ; ::_thesis: H = x 'in' y
assume H <> x 'in' y ; ::_thesis: contradiction
then H is_proper_subformula_of x 'in' y by A1, Def41;
then ex F being ZF-formula st F is_immediate_constituent_of x 'in' y by Th63;
hence contradiction by Th51; ::_thesis: verum
end;
assume H = x 'in' y ; ::_thesis: H is_subformula_of x 'in' y
hence H is_subformula_of x 'in' y by Th59; ::_thesis: verum
end;
definition
let H be ZF-formula;
func Subformulae H -> set means :Def42: :: ZF_LANG:def 42
for a being set holds
( a in it iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) );
existence
ex b1 being set st
for a being set holds
( a in b1 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) )
proof
defpred S1[ set ] means ex F being ZF-formula st
( F = $1 & F is_subformula_of H );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in NAT * & S1[a] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for a being set holds
( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) )
let a be set ; ::_thesis: ( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) )
thus ( a in X implies ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) by A1; ::_thesis: ( ex F being ZF-formula st
( F = a & F is_subformula_of H ) implies a in X )
given F being ZF-formula such that A2: ( F = a & F is_subformula_of H ) ; ::_thesis: a in X
F in NAT * by FINSEQ_1:def_11;
hence a in X by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in b2 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) holds
b1 = b2
proof
let X, Y be set ; ::_thesis: ( ( for a being set holds
( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in Y iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) implies X = Y )
assume that
A3: for a being set holds
( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) and
A4: for a being set holds
( a in Y iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ; ::_thesis: X = Y
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_X_implies_a_in_Y_)_&_(_a_in_Y_implies_a_in_X_)_)
let a be set ; ::_thesis: ( ( a in X implies a in Y ) & ( a in Y implies a in X ) )
thus ( a in X implies a in Y ) ::_thesis: ( a in Y implies a in X )
proof
assume a in X ; ::_thesis: a in Y
then ex F being ZF-formula st
( F = a & F is_subformula_of H ) by A3;
hence a in Y by A4; ::_thesis: verum
end;
assume a in Y ; ::_thesis: a in X
then ex F being ZF-formula st
( F = a & F is_subformula_of H ) by A4;
hence a in X by A3; ::_thesis: verum
end;
hence X = Y by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def42 defines Subformulae ZF_LANG:def_42_:_
for H being ZF-formula
for b2 being set holds
( b2 = Subformulae H iff for a being set holds
( a in b2 iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) );
theorem Th78: :: ZF_LANG:78
for G, H being ZF-formula st G in Subformulae H holds
G is_subformula_of H
proof
let G, H be ZF-formula; ::_thesis: ( G in Subformulae H implies G is_subformula_of H )
assume G in Subformulae H ; ::_thesis: G is_subformula_of H
then ex F being ZF-formula st
( F = G & F is_subformula_of H ) by Def42;
hence G is_subformula_of H ; ::_thesis: verum
end;
theorem :: ZF_LANG:79
for F, H being ZF-formula st F is_subformula_of H holds
Subformulae F c= Subformulae H
proof
let F, H be ZF-formula; ::_thesis: ( F is_subformula_of H implies Subformulae F c= Subformulae H )
assume A1: F is_subformula_of H ; ::_thesis: Subformulae F c= Subformulae H
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae F or a in Subformulae H )
assume a in Subformulae F ; ::_thesis: a in Subformulae H
then consider F1 being ZF-formula such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def42;
F1 is_subformula_of H by A1, A3, Th65;
hence a in Subformulae H by A2, Def42; ::_thesis: verum
end;
theorem Th80: :: ZF_LANG:80
for x, y being Variable holds Subformulae (x '=' y) = {(x '=' y)}
proof
let x, y be Variable; ::_thesis: Subformulae (x '=' y) = {(x '=' y)}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Subformulae_(x_'='_y)_implies_a_in_{(x_'='_y)}_)_&_(_a_in_{(x_'='_y)}_implies_a_in_Subformulae_(x_'='_y)_)_)
let a be set ; ::_thesis: ( ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) & ( a in {(x '=' y)} implies a in Subformulae (x '=' y) ) )
thus ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) ::_thesis: ( a in {(x '=' y)} implies a in Subformulae (x '=' y) )
proof
assume a in Subformulae (x '=' y) ; ::_thesis: a in {(x '=' y)}
then consider F being ZF-formula such that
A1: F = a and
A2: F is_subformula_of x '=' y by Def42;
F = x '=' y by A2, Th76;
hence a in {(x '=' y)} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume a in {(x '=' y)} ; ::_thesis: a in Subformulae (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; ::_thesis: verum
end;
hence Subformulae (x '=' y) = {(x '=' y)} by TARSKI:1; ::_thesis: verum
end;
theorem Th81: :: ZF_LANG:81
for x, y being Variable holds Subformulae (x 'in' y) = {(x 'in' y)}
proof
let x, y be Variable; ::_thesis: Subformulae (x 'in' y) = {(x 'in' y)}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Subformulae_(x_'in'_y)_implies_a_in_{(x_'in'_y)}_)_&_(_a_in_{(x_'in'_y)}_implies_a_in_Subformulae_(x_'in'_y)_)_)
let a be set ; ::_thesis: ( ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) & ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) ) )
thus ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) ::_thesis: ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) )
proof
assume a in Subformulae (x 'in' y) ; ::_thesis: a in {(x 'in' y)}
then consider F being ZF-formula such that
A1: F = a and
A2: F is_subformula_of x 'in' y by Def42;
F = x 'in' y by A2, Th77;
hence a in {(x 'in' y)} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume a in {(x 'in' y)} ; ::_thesis: a in Subformulae (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; ::_thesis: verum
end;
hence Subformulae (x 'in' y) = {(x 'in' y)} by TARSKI:1; ::_thesis: verum
end;
theorem Th82: :: ZF_LANG:82
for H being ZF-formula holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
proof
let H be ZF-formula; ::_thesis: Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Subformulae_('not'_H)_implies_a_in_(Subformulae_H)_\/_{('not'_H)}_)_&_(_a_in_(Subformulae_H)_\/_{('not'_H)}_implies_a_in_Subformulae_('not'_H)_)_)
let a be set ; ::_thesis: ( ( a in Subformulae ('not' H) implies a in (Subformulae H) \/ {('not' H)} ) & ( a in (Subformulae H) \/ {('not' H)} implies a in Subformulae ('not' H) ) )
A1: now__::_thesis:_(_a_in_{('not'_H)}_implies_a_in_Subformulae_('not'_H)_)
assume a in {('not' H)} ; ::_thesis: a in Subformulae ('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; ::_thesis: verum
end;
thus ( a in Subformulae ('not' H) implies a in (Subformulae H) \/ {('not' H)} ) ::_thesis: ( a in (Subformulae H) \/ {('not' H)} implies a in Subformulae ('not' H) )
proof
assume a in Subformulae ('not' H) ; ::_thesis: a in (Subformulae H) \/ {('not' H)}
then consider F being ZF-formula such that
A3: F = a and
A4: F is_subformula_of 'not' H by Def42;
now__::_thesis:_(_F_<>_'not'_H_implies_a_in_Subformulae_H_)
assume F <> 'not' H ; ::_thesis: a in Subformulae H
then F is_proper_subformula_of 'not' H by A4, Def41;
then F is_subformula_of H by Th69;
hence a in Subformulae H by A3, Def42; ::_thesis: verum
end;
then ( a in Subformulae H or a in {('not' H)} ) by A3, TARSKI:def_1;
hence a in (Subformulae H) \/ {('not' H)} by XBOOLE_0:def_3; ::_thesis: verum
end;
A5: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_('not'_H)_)
assume a in Subformulae H ; ::_thesis: a in Subformulae ('not' H)
then consider F being ZF-formula such that
A6: F = a and
A7: F is_subformula_of H by Def42;
H is_immediate_constituent_of 'not' H by Th52;
then H is_proper_subformula_of 'not' H by Th61;
then H is_subformula_of 'not' H by Def41;
then F is_subformula_of 'not' H by A7, Th65;
hence a in Subformulae ('not' H) by A6, Def42; ::_thesis: verum
end;
assume a in (Subformulae H) \/ {('not' H)} ; ::_thesis: a in Subformulae ('not' H)
hence a in Subformulae ('not' H) by A5, A1, XBOOLE_0:def_3; ::_thesis: verum
end;
hence Subformulae ('not' H) = (Subformulae H) \/ {('not' H)} by TARSKI:1; ::_thesis: verum
end;
theorem Th83: :: ZF_LANG:83
for H, F being ZF-formula holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
proof
let H, F be ZF-formula; ::_thesis: Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Subformulae_(H_'&'_F)_implies_a_in_((Subformulae_H)_\/_(Subformulae_F))_\/_{(H_'&'_F)}_)_&_(_a_in_((Subformulae_H)_\/_(Subformulae_F))_\/_{(H_'&'_F)}_implies_a_in_Subformulae_(H_'&'_F)_)_)
let a be set ; ::_thesis: ( ( a in Subformulae (H '&' F) implies a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ) & ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) ) )
A1: ( not a in (Subformulae H) \/ (Subformulae F) or 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)} ) ::_thesis: ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) )
proof
assume a in Subformulae (H '&' F) ; ::_thesis: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
then consider G being ZF-formula such that
A2: G = a and
A3: G is_subformula_of H '&' F by Def42;
now__::_thesis:_(_G_<>_H_'&'_F_implies_a_in_(Subformulae_H)_\/_(Subformulae_F)_)
assume G <> H '&' F ; ::_thesis: a in (Subformulae H) \/ (Subformulae F)
then G is_proper_subformula_of H '&' F by A3, Def41;
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; ::_thesis: verum
end;
then ( a in (Subformulae H) \/ (Subformulae F) or a in {(H '&' F)} ) by A2, TARSKI:def_1;
hence a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by XBOOLE_0:def_3; ::_thesis: verum
end;
A4: now__::_thesis:_(_a_in_{(H_'&'_F)}_implies_a_in_Subformulae_(H_'&'_F)_)
assume a in {(H '&' F)} ; ::_thesis: a in Subformulae (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; ::_thesis: verum
end;
A6: now__::_thesis:_(_a_in_Subformulae_F_implies_a_in_Subformulae_(H_'&'_F)_)
assume a in Subformulae F ; ::_thesis: a in Subformulae (H '&' F)
then consider G being ZF-formula such that
A7: G = a and
A8: G is_subformula_of F by Def42;
F is_immediate_constituent_of H '&' F by Th53;
then F is_proper_subformula_of H '&' F by Th61;
then F is_subformula_of H '&' F by Def41;
then G is_subformula_of H '&' F by A8, Th65;
hence a in Subformulae (H '&' F) by A7, Def42; ::_thesis: verum
end;
A9: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_(H_'&'_F)_)
assume a in Subformulae H ; ::_thesis: a in Subformulae (H '&' F)
then consider G being ZF-formula such that
A10: G = a and
A11: G is_subformula_of H by Def42;
H is_immediate_constituent_of H '&' F by Th53;
then H is_proper_subformula_of H '&' F by Th61;
then H is_subformula_of H '&' F by Def41;
then G is_subformula_of H '&' F by A11, Th65;
hence a in Subformulae (H '&' F) by A10, Def42; ::_thesis: verum
end;
assume a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ; ::_thesis: a in Subformulae (H '&' F)
hence a in Subformulae (H '&' F) by A1, A9, A6, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
hence Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by TARSKI:1; ::_thesis: verum
end;
theorem Th84: :: ZF_LANG:84
for x being Variable
for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
proof
let x be Variable; ::_thesis: for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let H be ZF-formula; ::_thesis: Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_Subformulae_(All_(x,H))_implies_a_in_(Subformulae_H)_\/_{(All_(x,H))}_)_&_(_a_in_(Subformulae_H)_\/_{(All_(x,H))}_implies_a_in_Subformulae_(All_(x,H))_)_)
let a be set ; ::_thesis: ( ( a in Subformulae (All (x,H)) implies a in (Subformulae H) \/ {(All (x,H))} ) & ( a in (Subformulae H) \/ {(All (x,H))} implies a in Subformulae (All (x,H)) ) )
A1: now__::_thesis:_(_a_in_{(All_(x,H))}_implies_a_in_Subformulae_(All_(x,H))_)
assume a in {(All (x,H))} ; ::_thesis: a in Subformulae (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; ::_thesis: verum
end;
thus ( a in Subformulae (All (x,H)) implies a in (Subformulae H) \/ {(All (x,H))} ) ::_thesis: ( a in (Subformulae H) \/ {(All (x,H))} implies a in Subformulae (All (x,H)) )
proof
assume a in Subformulae (All (x,H)) ; ::_thesis: a in (Subformulae H) \/ {(All (x,H))}
then consider F being ZF-formula such that
A3: F = a and
A4: F is_subformula_of All (x,H) by Def42;
now__::_thesis:_(_F_<>_All_(x,H)_implies_a_in_Subformulae_H_)
assume F <> All (x,H) ; ::_thesis: a in Subformulae H
then F is_proper_subformula_of All (x,H) by A4, Def41;
then F is_subformula_of H by Th71;
hence a in Subformulae H by A3, Def42; ::_thesis: verum
end;
then ( a in Subformulae H or a in {(All (x,H))} ) by A3, TARSKI:def_1;
hence a in (Subformulae H) \/ {(All (x,H))} by XBOOLE_0:def_3; ::_thesis: verum
end;
A5: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_(All_(x,H))_)
assume a in Subformulae H ; ::_thesis: a in Subformulae (All (x,H))
then consider F being ZF-formula such that
A6: F = a and
A7: F is_subformula_of H by Def42;
H is_immediate_constituent_of All (x,H) by Th54;
then H is_proper_subformula_of All (x,H) by Th61;
then H is_subformula_of All (x,H) by Def41;
then F is_subformula_of All (x,H) by A7, Th65;
hence a in Subformulae (All (x,H)) by A6, Def42; ::_thesis: verum
end;
assume a in (Subformulae H) \/ {(All (x,H))} ; ::_thesis: a in Subformulae (All (x,H))
hence a in Subformulae (All (x,H)) by A5, A1, XBOOLE_0:def_3; ::_thesis: verum
end;
hence Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))} by TARSKI:1; ::_thesis: verum
end;
theorem :: ZF_LANG:85
for H being ZF-formula holds
( H is atomic iff Subformulae H = {H} )
proof
let H be ZF-formula; ::_thesis: ( H is atomic iff Subformulae H = {H} )
thus ( H is atomic implies Subformulae H = {H} ) ::_thesis: ( Subformulae H = {H} implies H is atomic )
proof
assume H is atomic ; ::_thesis: Subformulae H = {H}
then ( H is being_equality or H is being_membership ) by Def15;
then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th36, Th37;
hence Subformulae H = {H} by Th80, Th81; ::_thesis: verum
end;
assume A1: Subformulae H = {H} ; ::_thesis: H is atomic
A2: now__::_thesis:_not_H_=_'not'_(the_argument_of_H)
assume H = 'not' (the_argument_of H) ; ::_thesis: contradiction
then A3: the_argument_of H is_immediate_constituent_of H by Th52;
then the_argument_of H is_proper_subformula_of H by Th61;
then the_argument_of H is_subformula_of H by Def41;
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; ::_thesis: verum
end;
A5: now__::_thesis:_not_H_=_(the_left_argument_of_H)_'&'_(the_right_argument_of_H)
assume H = (the_left_argument_of H) '&' (the_right_argument_of H) ; ::_thesis: contradiction
then A6: the_left_argument_of H is_immediate_constituent_of H by Th53;
then the_left_argument_of H is_proper_subformula_of H by Th61;
then the_left_argument_of H is_subformula_of H by Def41;
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; ::_thesis: verum
end;
assume not H is atomic ; ::_thesis: contradiction
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, Th54;
then the_scope_of H is_proper_subformula_of H by Th61;
then the_scope_of H is_subformula_of H by Def41;
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; ::_thesis: verum
end;
theorem :: ZF_LANG:86
for H being ZF-formula st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
proof
let H be ZF-formula; ::_thesis: ( H is negative implies Subformulae H = (Subformulae (the_argument_of H)) \/ {H} )
assume H is negative ; ::_thesis: Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
then H = 'not' (the_argument_of H) by Def30;
hence Subformulae H = (Subformulae (the_argument_of H)) \/ {H} by Th82; ::_thesis: verum
end;
theorem :: ZF_LANG:87
for H being ZF-formula st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive implies Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )
assume H is conjunctive ; ::_thesis: Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th40;
hence Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by Th83; ::_thesis: verum
end;
theorem :: ZF_LANG:88
for H being ZF-formula st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
proof
let H be ZF-formula; ::_thesis: ( H is universal implies Subformulae H = (Subformulae (the_scope_of H)) \/ {H} )
assume H is universal ; ::_thesis: Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
then H = All ((bound_in H),(the_scope_of H)) by Th44;
hence Subformulae H = (Subformulae (the_scope_of H)) \/ {H} by Th84; ::_thesis: verum
end;
theorem :: ZF_LANG:89
for H, G, F being ZF-formula st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds
H in Subformulae F
proof
let H, G, F be ZF-formula; ::_thesis: ( ( 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 )
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 ; ::_thesis: H 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 by Def41;
G is_subformula_of F by A2, Th78;
then H is_subformula_of F by A3, Th65;
hence H in Subformulae F by Def42; ::_thesis: verum
end;
scheme :: ZF_LANG:sch 1
ZFInd{ P1[ ZF-formula] } :
for H being ZF-formula holds P1[H]
provided
A1: for H being ZF-formula st H is atomic holds
P1[H] and
A2: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds
P1[H] and
A3: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds
P1[H] and
A4: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds
P1[H]
proof
defpred S1[ Nat] means for H being ZF-formula st len H = $1 holds
P1[H];
A5: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A6: for k being Nat st k < n holds
for H being ZF-formula st len H = k holds
P1[H] ; ::_thesis: S1[n]
let H be ZF-formula; ::_thesis: ( len H = n implies P1[H] )
assume A7: len H = n ; ::_thesis: P1[H]
A8: now__::_thesis:_(_H_is_conjunctive_implies_P1[H]_)
assume A9: H is conjunctive ; ::_thesis: P1[H]
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 by Th53;
then len (the_right_argument_of H) < len H by Th60;
then A11: P1[ the_right_argument_of H] by A6, A7;
the_left_argument_of H is_immediate_constituent_of H by A10, Th53;
then len (the_left_argument_of H) < len H by Th60;
then P1[ the_left_argument_of H] by A6, A7;
hence P1[H] by A3, A9, A11; ::_thesis: verum
end;
A12: now__::_thesis:_(_H_is_universal_implies_P1[H]_)
assume A13: H is universal ; ::_thesis: P1[H]
then H = All ((bound_in H),(the_scope_of H)) by Th44;
then the_scope_of H is_immediate_constituent_of H by Th54;
then len (the_scope_of H) < len H by Th60;
hence P1[H] by A4, A6, A7, A13; ::_thesis: verum
end;
now__::_thesis:_(_H_is_negative_implies_P1[H]_)
assume A14: H is negative ; ::_thesis: P1[H]
then H = 'not' (the_argument_of H) by Def30;
then the_argument_of H is_immediate_constituent_of H by Th52;
then len (the_argument_of H) < len H by Th60;
hence P1[H] by A2, A6, A7, A14; ::_thesis: verum
end;
hence P1[H] by A1, A8, A12, Th10; ::_thesis: verum
end;
A15: for n being Nat holds S1[n] from NAT_1:sch_4(A5);
let H be ZF-formula; ::_thesis: P1[H]
len H = len H ;
hence P1[H] by A15; ::_thesis: verum
end;
scheme :: ZF_LANG:sch 2
ZFCompInd{ P1[ ZF-formula] } :
for H being ZF-formula holds P1[H]
provided
A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds
P1[F] ) holds
P1[H]
proof
defpred S1[ Nat] means for H being ZF-formula st len H = $1 holds
P1[H];
A2: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A3: for k being Nat st k < n holds
for H being ZF-formula st len H = k holds
P1[H] ; ::_thesis: S1[n]
let H be ZF-formula; ::_thesis: ( len H = n implies P1[H] )
assume A4: len H = n ; ::_thesis: P1[H]
now__::_thesis:_for_F_being_ZF-formula_st_F_is_proper_subformula_of_H_holds_
P1[F]
let F be ZF-formula; ::_thesis: ( F is_proper_subformula_of H implies P1[F] )
assume F is_proper_subformula_of H ; ::_thesis: P1[F]
then len F < len H by Th62;
hence P1[F] by A3, A4; ::_thesis: verum
end;
hence P1[H] by A1; ::_thesis: verum
end;
A5: for n being Nat holds S1[n] from NAT_1:sch_4(A2);
let H be ZF-formula; ::_thesis: P1[H]
len H = len H ;
hence P1[H] by A5; ::_thesis: verum
end;