let x be Variable; 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; ( 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)
; ZF_LANG:def 41 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;
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; ZF_LANG:def 40 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
; ( 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; ( 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; ( 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 for j being Nat st 1 <= j & j <= m holds
L1 . j = L . jend;
hence
L1 . 1 = F
by A5, A9; ( 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; 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 ; ( 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
; 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
; ex F1 being ZF-formula st
( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 )
take
G1
; ( 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; verum