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	syl6eq	⊢ ( 𝑢 = ∅ → ( 𝐻 ‘ 𝑢 ) = ∅ )
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	syl6eq	⊢ ( 𝑢 = ∅ → ( 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	syl5eqr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ 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 𝐺 ) )