Metamath Proof Explorer

Theorem cantnfsuc

Description: The value of the recursive function H at a successor. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnfs.s ⊢S=dom⁡ACNFB
cantnfs.a ⊢φ→A∈On
cantnfs.b ⊢φ→B∈On
cantnfcl.g ⊢G=OrdIsoEFsupp∅
cantnfcl.f ⊢φ→F∈S
cantnfval.h ⊢H=seqωk∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜z∅
Assertion cantnfsuc ⊢φ∧K∈ω→H⁡suc⁡K=A↑𝑜G⁡K⋅𝑜F⁡G⁡K+𝑜H⁡K

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢S=dom⁡ACNFB
2 cantnfs.a ⊢φ→A∈On
3 cantnfs.b ⊢φ→B∈On
4 cantnfcl.g ⊢G=OrdIsoEFsupp∅
5 cantnfcl.f ⊢φ→F∈S
6 cantnfval.h ⊢H=seqωk∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜z∅
7 6 seqomsuc ⊢K∈ω→H⁡suc⁡K=Kk∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜zH⁡K
8 7 adantl ⊢φ∧K∈ω→H⁡suc⁡K=Kk∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜zH⁡K
9 elex ⊢K∈ω→K∈V
10 9 adantl ⊢φ∧K∈ω→K∈V
11 fvex ⊢H⁡K∈V
12 simpl ⊢u=K∧v=H⁡K→u=K
13 12 fveq2d ⊢u=K∧v=H⁡K→G⁡u=G⁡K
14 13 oveq2d ⊢u=K∧v=H⁡K→A↑𝑜G⁡u=A↑𝑜G⁡K
15 13 fveq2d ⊢u=K∧v=H⁡K→F⁡G⁡u=F⁡G⁡K
16 14 15 oveq12d ⊢u=K∧v=H⁡K→A↑𝑜G⁡u⋅𝑜F⁡G⁡u=A↑𝑜G⁡K⋅𝑜F⁡G⁡K
17 simpr ⊢u=K∧v=H⁡K→v=H⁡K
18 16 17 oveq12d ⊢u=K∧v=H⁡K→A↑𝑜G⁡u⋅𝑜F⁡G⁡u+𝑜v=A↑𝑜G⁡K⋅𝑜F⁡G⁡K+𝑜H⁡K
19 fveq2 ⊢k=u→G⁡k=G⁡u
20 19 oveq2d ⊢k=u→A↑𝑜G⁡k=A↑𝑜G⁡u
21 19 fveq2d ⊢k=u→F⁡G⁡k=F⁡G⁡u
22 20 21 oveq12d ⊢k=u→A↑𝑜G⁡k⋅𝑜F⁡G⁡k=A↑𝑜G⁡u⋅𝑜F⁡G⁡u
23 22 oveq1d ⊢k=u→A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜z=A↑𝑜G⁡u⋅𝑜F⁡G⁡u+𝑜z
24 oveq2 ⊢z=v→A↑𝑜G⁡u⋅𝑜F⁡G⁡u+𝑜z=A↑𝑜G⁡u⋅𝑜F⁡G⁡u+𝑜v
25 23 24 cbvmpov ⊢k∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜z=u∈V,v∈V⟼A↑𝑜G⁡u⋅𝑜F⁡G⁡u+𝑜v
26 ovex ⊢A↑𝑜G⁡K⋅𝑜F⁡G⁡K+𝑜H⁡K∈V
27 18 25 26 ovmpoa ⊢K∈V∧H⁡K∈V→Kk∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜zH⁡K=A↑𝑜G⁡K⋅𝑜F⁡G⁡K+𝑜H⁡K
28 10 11 27 sylancl ⊢φ∧K∈ω→Kk∈V,z∈V⟼A↑𝑜G⁡k⋅𝑜F⁡G⁡k+𝑜zH⁡K=A↑𝑜G⁡K⋅𝑜F⁡G⁡K+𝑜H⁡K
29 8 28 eqtrd ⊢φ∧K∈ω→H⁡suc⁡K=A↑𝑜G⁡K⋅𝑜F⁡G⁡K+𝑜H⁡K