Metamath Proof Explorer


Theorem cantnfval2

Description: Alternate expression for the value of the Cantor normal form function. (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 cantnfval2 ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) )

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 1 2 3 4 5 6 cantnfval ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
8 ssid dom 𝐺 ⊆ dom 𝐺
9 1 2 3 4 5 cantnfcl ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )
10 9 simprd ( 𝜑 → dom 𝐺 ∈ ω )
11 sseq1 ( 𝑢 = ∅ → ( 𝑢 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺 ) )
12 fveq2 ( 𝑢 = ∅ → ( 𝐻𝑢 ) = ( 𝐻 ‘ ∅ ) )
13 0ex ∅ ∈ V
14 6 seqom0g ( ∅ ∈ V → ( 𝐻 ‘ ∅ ) = ∅ )
15 13 14 ax-mp ( 𝐻 ‘ ∅ ) = ∅
16 12 15 eqtrdi ( 𝑢 = ∅ → ( 𝐻𝑢 ) = ∅ )
17 fveq2 ( 𝑢 = ∅ → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) )
18 eqid seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
19 18 seqom0g ( ∅ ∈ V → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ )
20 13 19 ax-mp ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅
21 17 20 eqtrdi ( 𝑢 = ∅ → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) = ∅ )
22 16 21 eqeq12d ( 𝑢 = ∅ → ( ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ↔ ∅ = ∅ ) )
23 11 22 imbi12d ( 𝑢 = ∅ → ( ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ↔ ( ∅ ⊆ dom 𝐺 → ∅ = ∅ ) ) )
24 23 imbi2d ( 𝑢 = ∅ → ( ( 𝜑 → ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ dom 𝐺 → ∅ = ∅ ) ) ) )
25 sseq1 ( 𝑢 = 𝑣 → ( 𝑢 ⊆ dom 𝐺𝑣 ⊆ dom 𝐺 ) )
26 fveq2 ( 𝑢 = 𝑣 → ( 𝐻𝑢 ) = ( 𝐻𝑣 ) )
27 fveq2 ( 𝑢 = 𝑣 → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) )
28 26 27 eqeq12d ( 𝑢 = 𝑣 → ( ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ↔ ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
29 25 28 imbi12d ( 𝑢 = 𝑣 → ( ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ↔ ( 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) ) )
30 29 imbi2d ( 𝑢 = 𝑣 → ( ( 𝜑 → ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ) ↔ ( 𝜑 → ( 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) ) ) )
31 sseq1 ( 𝑢 = suc 𝑣 → ( 𝑢 ⊆ dom 𝐺 ↔ suc 𝑣 ⊆ dom 𝐺 ) )
32 fveq2 ( 𝑢 = suc 𝑣 → ( 𝐻𝑢 ) = ( 𝐻 ‘ suc 𝑣 ) )
33 fveq2 ( 𝑢 = suc 𝑣 → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) )
34 32 33 eqeq12d ( 𝑢 = suc 𝑣 → ( ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ↔ ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) )
35 31 34 imbi12d ( 𝑢 = suc 𝑣 → ( ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ↔ ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) )
36 35 imbi2d ( 𝑢 = suc 𝑣 → ( ( 𝜑 → ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ) ↔ ( 𝜑 → ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) ) )
37 sseq1 ( 𝑢 = dom 𝐺 → ( 𝑢 ⊆ dom 𝐺 ↔ dom 𝐺 ⊆ dom 𝐺 ) )
38 fveq2 ( 𝑢 = dom 𝐺 → ( 𝐻𝑢 ) = ( 𝐻 ‘ dom 𝐺 ) )
39 fveq2 ( 𝑢 = dom 𝐺 → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) )
40 38 39 eqeq12d ( 𝑢 = dom 𝐺 → ( ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ↔ ( 𝐻 ‘ dom 𝐺 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) ) )
41 37 40 imbi12d ( 𝑢 = dom 𝐺 → ( ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ↔ ( dom 𝐺 ⊆ dom 𝐺 → ( 𝐻 ‘ dom 𝐺 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) ) ) )
42 41 imbi2d ( 𝑢 = dom 𝐺 → ( ( 𝜑 → ( 𝑢 ⊆ dom 𝐺 → ( 𝐻𝑢 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑢 ) ) ) ↔ ( 𝜑 → ( dom 𝐺 ⊆ dom 𝐺 → ( 𝐻 ‘ dom 𝐺 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) ) ) ) )
43 eqid ∅ = ∅
44 43 2a1i ( 𝜑 → ( ∅ ⊆ dom 𝐺 → ∅ = ∅ ) )
45 sssucid 𝑣 ⊆ suc 𝑣
46 sstr ( ( 𝑣 ⊆ suc 𝑣 ∧ suc 𝑣 ⊆ dom 𝐺 ) → 𝑣 ⊆ dom 𝐺 )
47 45 46 mpan ( suc 𝑣 ⊆ dom 𝐺𝑣 ⊆ dom 𝐺 )
48 47 imim1i ( ( 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) → ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
49 oveq2 ( ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) → ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻𝑣 ) ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
50 6 seqomsuc ( 𝑣 ∈ ω → ( 𝐻 ‘ suc 𝑣 ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻𝑣 ) ) )
51 50 ad2antrl ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( 𝐻 ‘ suc 𝑣 ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻𝑣 ) ) )
52 18 seqomsuc ( 𝑣 ∈ ω → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) = ( 𝑣 ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
53 52 ad2antrl ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) = ( 𝑣 ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
54 ssv dom 𝐺 ⊆ V
55 ssv On ⊆ V
56 resmpo ( ( dom 𝐺 ⊆ V ∧ On ⊆ V ) → ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ↾ ( dom 𝐺 × On ) ) = ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) )
57 54 55 56 mp2an ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ↾ ( dom 𝐺 × On ) ) = ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) )
58 57 oveqi ( 𝑣 ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ↾ ( dom 𝐺 × On ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) = ( 𝑣 ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) )
59 simprr ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → suc 𝑣 ⊆ dom 𝐺 )
60 vex 𝑣 ∈ V
61 60 sucid 𝑣 ∈ suc 𝑣
62 61 a1i ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → 𝑣 ∈ suc 𝑣 )
63 59 62 sseldd ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → 𝑣 ∈ dom 𝐺 )
64 18 cantnfvalf seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) : ω ⟶ On
65 64 ffvelrni ( 𝑣 ∈ ω → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ∈ On )
66 65 ad2antrl ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ∈ On )
67 ovres ( ( 𝑣 ∈ dom 𝐺 ∧ ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ∈ On ) → ( 𝑣 ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ↾ ( dom 𝐺 × On ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
68 63 66 67 syl2anc ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( 𝑣 ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ↾ ( dom 𝐺 × On ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
69 58 68 eqtr3id ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( 𝑣 ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
70 53 69 eqtrd ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) )
71 51 70 eqeq12d ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ↔ ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( 𝐻𝑣 ) ) = ( 𝑣 ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) ) )
72 49 71 syl5ibr ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺 ) ) → ( ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) )
73 72 expr ( ( 𝜑𝑣 ∈ ω ) → ( suc 𝑣 ⊆ dom 𝐺 → ( ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) )
74 73 a2d ( ( 𝜑𝑣 ∈ ω ) → ( ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) → ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) )
75 48 74 syl5 ( ( 𝜑𝑣 ∈ ω ) → ( ( 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) → ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) )
76 75 expcom ( 𝑣 ∈ ω → ( 𝜑 → ( ( 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) → ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) ) )
77 76 a2d ( 𝑣 ∈ ω → ( ( 𝜑 → ( 𝑣 ⊆ dom 𝐺 → ( 𝐻𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ 𝑣 ) ) ) → ( 𝜑 → ( suc 𝑣 ⊆ dom 𝐺 → ( 𝐻 ‘ suc 𝑣 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ suc 𝑣 ) ) ) ) )
78 24 30 36 42 44 77 finds ( dom 𝐺 ∈ ω → ( 𝜑 → ( dom 𝐺 ⊆ dom 𝐺 → ( 𝐻 ‘ dom 𝐺 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) ) ) )
79 10 78 mpcom ( 𝜑 → ( dom 𝐺 ⊆ dom 𝐺 → ( 𝐻 ‘ dom 𝐺 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) ) )
80 8 79 mpi ( 𝜑 → ( 𝐻 ‘ dom 𝐺 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) )
81 7 80 eqtrd ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( seqω ( ( 𝑘 ∈ dom 𝐺 , 𝑧 ∈ On ↦ ( ( ( 𝐴o ( 𝐺𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom 𝐺 ) )