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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnfcl.g ⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
cantnfcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
cantnfval.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
Assertion cantnfsuc ( ( 𝜑 ∧ 𝐾 ∈ ω ) → ( 𝐻 ‘ suc 𝐾 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) +o ( 𝐻 ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 cantnfcl.g ⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
5 cantnfcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6 cantnfval.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
7 6 seqomsuc ⊢ ( 𝐾 ∈ ω → ( 𝐻 ‘ suc 𝐾 ) = ( 𝐾 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻 ‘ 𝐾 ) ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ω ) → ( 𝐻 ‘ suc 𝐾 ) = ( 𝐾 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻 ‘ 𝐾 ) ) )
9 elex ⊢ ( 𝐾 ∈ ω → 𝐾 ∈ V )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ω ) → 𝐾 ∈ V )
11 fvex ⊢ ( 𝐻 ‘ 𝐾 ) ∈ V
12 simpl ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → 𝑢 = 𝐾 )
13 12 fveq2d ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝐾 ) )
14 13 oveq2d ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) = ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) )
15 13 fveq2d ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) )
16 14 15 oveq12d ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) = ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) )
17 simpr ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → 𝑣 = ( 𝐻 ‘ 𝐾 ) )
18 16 17 oveq12d ⊢ ( ( 𝑢 = 𝐾 ∧ 𝑣 = ( 𝐻 ‘ 𝐾 ) ) → ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑣 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) +o ( 𝐻 ‘ 𝐾 ) ) )
19 fveq2 ⊢ ( 𝑘 = 𝑢 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑢 ) )
20 19 oveq2d ⊢ ( 𝑘 = 𝑢 → ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) )
21 19 fveq2d ⊢ ( 𝑘 = 𝑢 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) )
22 20 21 oveq12d ⊢ ( 𝑘 = 𝑢 → ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) )
23 22 oveq1d ⊢ ( 𝑘 = 𝑢 → ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑧 ) )
24 oveq2 ⊢ ( 𝑧 = 𝑣 → ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑧 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑣 ) )
25 23 24 cbvmpov ⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑢 ) ) ) +o 𝑣 ) )
26 ovex ⊢ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) +o ( 𝐻 ‘ 𝐾 ) ) ∈ V
27 18 25 26 ovmpoa ⊢ ( ( 𝐾 ∈ V ∧ ( 𝐻 ‘ 𝐾 ) ∈ V ) → ( 𝐾 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻 ‘ 𝐾 ) ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) +o ( 𝐻 ‘ 𝐾 ) ) )
28 10 11 27 sylancl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ω ) → ( 𝐾 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻 ‘ 𝐾 ) ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) +o ( 𝐻 ‘ 𝐾 ) ) )
29 8 28 eqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ω ) → ( 𝐻 ‘ suc 𝐾 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝐾 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝐾 ) ) ) +o ( 𝐻 ‘ 𝐾 ) ) )