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 A1:
( F is_subformula_of G & F <> G & G is_subformula_of H & G <> H )
; :: according to ZF_LANG:def 41 :: thesis: F is_proper_subformula_of H
then consider n being Element of NAT , L being FinSequence such that
A2:
( 1 <= n & len L = n & L . 1 = F & L . n = G )
and
A3:
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;
1 < n
by A1, A2, XXREAL_0:1;
then A4:
1 + 1 <= n
by NAT_1:13;
consider m being Element of NAT , L' being FinSequence such that
A5:
( 1 <= m & len L' = m & L' . 1 = G & L' . m = H )
and
A6:
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 )
by A1, Def40;
consider k being Nat such that
A7:
n = 2 + k
by A4, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:19;
thus
F is_subformula_of H
:: according to ZF_LANG:def 41 :: thesis: F <> Hproof
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 ^ L';
:: 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 ) ) )
(
m <= m + (1 + k) &
m + (1 + k) = (1 + k) + m )
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 A8:
1
+ k <= n
by A7, NAT_1:11;
then A9:
len L1 = 1
+ k
by A2, FINSEQ_1:21;
hence A10:
len K = l
by A5, FINSEQ_1:35;
:: 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 ) ) )
( 1
<= 1
+ k & 1
<= 1 )
by NAT_1:11;
hence
K . 1
= F
by A2, A11;
:: 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:9;
then
(
len L1 < l &
l <= l )
by A9, NAT_1:13;
then A13:
K . l = L' . (l - (len L1))
by A10, FINSEQ_1:37;
((1 + k) + m) - (1 + k) = m
;
hence
K . l = H
by A2, A5, A8, A13, FINSEQ_1:21;
:: 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 A14:
( 1
<= j &
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 &
j + 0 = j )
by XREAL_1:9;
then A15:
1
<= j + 1
by A14, XXREAL_0:2;
A19:
now assume A20:
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 A21:
( 1
+ k < j + 1 &
j + 1
<= l )
by A14, NAT_1:13;
A22:
(
j + 1
= 1
+ j &
(j + 1) - j = (j + 1) + (- j) &
(1 + j) + (- j) = 1
+ (j + (- j)) &
j + (- j) = 0 )
;
(
K . j = L . j &
j < (1 + k) + 1 )
by A11, A14, A20, NAT_1:13;
then consider F1,
G1 being
ZF-formula such that A23:
(
L . j = F1 &
L . (j + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A3, A7, A14;
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 A2, A5, A7, A9, A10, A11, A14, A20, A21, A22, A23, FINSEQ_1:37;
:: thesis: verum end;
now assume A24:
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 A25:
( 1
+ k < j + 1 &
j <= l &
j + 1
<= l )
by A14, NAT_1:13;
(1 + k) + 1
<= j
by A24, NAT_1:13;
then consider j1 being
Nat such that A26:
j = ((1 + k) + 1) + j1
by NAT_1:10;
reconsider j1 =
j1 as
Element of
NAT by ORDINAL1:def 13;
A27:
(
((1 + k) + 1) + j1 = (1 + k) + (1 + j1) &
(1 + k) + (1 + j1) = (1 + j1) + (1 + k) &
((1 + j1) + (1 + k)) - (1 + k) = ((1 + j1) + (1 + k)) + (- (1 + k)) &
((1 + j1) + (1 + k)) + (- (1 + k)) = (1 + j1) + ((1 + k) + (- (1 + k))) &
(1 + k) + (- (1 + k)) = 0 &
(1 + j1) + 0 = 1
+ j1 )
;
A28:
(j + 1) - (len L1) =
1
+ (j + (- (len L1)))
.=
(1 + j1) + 1
by A2, A8, A26, A27, FINSEQ_1:21
;
( 1
<= 1
+ j1 &
j - (1 + k) < l - (1 + k) )
by A14, NAT_1:11, XREAL_1:11;
then consider F1,
G1 being
ZF-formula such that A29:
(
L' . (1 + j1) = F1 &
L' . ((1 + j1) + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A6, A26;
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 A9, A10, A24, A25, A27, A28, A29, FINSEQ_1:37;
:: 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 A16, A19, XXREAL_0:1;
:: thesis: verum
end;
assume A30:
F = H
; :: thesis: contradiction
( F is_proper_subformula_of G & G is_proper_subformula_of H )
by A1, Def41;
then
( len F < len G & len G < len H )
by Th83;
hence
contradiction
by A30; :: thesis: verum