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 ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnfcl.g ⊢ G = OrdIso E F supp ∅
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 ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 cantnfcl.g ⊢ G = OrdIso E F supp ∅
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 = K k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z H ⁡ K
8 7 adantl ⊢ φ ∧ K ∈ ω → H ⁡ suc ⁡ K = K k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z H ⁡ 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 → K k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z H ⁡ K = A ↑ 𝑜 G ⁡ K ⋅ 𝑜 F ⁡ G ⁡ K + 𝑜 H ⁡ K
28 10 11 27 sylancl ⊢ φ ∧ K ∈ ω → K k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z H ⁡ 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