This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmi ⊢ ( 𝑣 ∈ ω → ( 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 imbitrrid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ 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 𝐺 ) )