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 ( 𝐻 ‘ 𝐾 ) ) )