Theorem cantnfval

Description: 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	cantnfval	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( 𝐻 ‘ 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		eqid	⊢ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ }
8	7 2 3	cantnffval	⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )
9	8	fveq1d	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) ‘ 𝐹 ) )
10	7 2 3	cantnfdm	⊢ ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
11	1 10	eqtrid	⊢ ( 𝜑 → 𝑆 = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
12	5 11	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
13		ovex	⊢ ( 𝑓 supp ∅ ) ∈ V
14		eqid	⊢ OrdIso ( E , ( 𝑓 supp ∅ ) ) = OrdIso ( E , ( 𝑓 supp ∅ ) )
15	14	oiexg	⊢ ( ( 𝑓 supp ∅ ) ∈ V → OrdIso ( E , ( 𝑓 supp ∅ ) ) ∈ V )
16	13 15	mp1i	⊢ ( 𝑓 = 𝐹 → OrdIso ( E , ( 𝑓 supp ∅ ) ) ∈ V )
17		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) )
18		oveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 supp ∅ ) = ( 𝐹 supp ∅ ) )
19	18	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( 𝑓 supp ∅ ) = ( 𝐹 supp ∅ ) )
20		oieq2	⊢ ( ( 𝑓 supp ∅ ) = ( 𝐹 supp ∅ ) → OrdIso ( E , ( 𝑓 supp ∅ ) ) = OrdIso ( E , ( 𝐹 supp ∅ ) ) )
21	19 20	syl	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → OrdIso ( E , ( 𝑓 supp ∅ ) ) = OrdIso ( E , ( 𝐹 supp ∅ ) ) )
22	17 21	eqtrd	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ℎ = OrdIso ( E , ( 𝐹 supp ∅ ) ) )
23	22 4	eqtr4di	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ℎ = 𝐺 )
24	23	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( ℎ ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
25	24	oveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) = ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) )
26		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → 𝑓 = 𝐹 )
27	26 24	fveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
28	25 27	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) = ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
29	28	oveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) = ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
30	29	mpoeq3dv	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) )
31		eqid	⊢ ∅ = ∅
32		seqomeq12	⊢ ( ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ∧ ∅ = ∅ ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
33	30 31 32	sylancl	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
34	33 6	eqtr4di	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = 𝐻 )
35	23	dmeqd	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → dom ℎ = dom 𝐺 )
36	34 35	fveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ ℎ = OrdIso ( E , ( 𝑓 supp ∅ ) ) ) → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) = ( 𝐻 ‘ dom 𝐺 ) )
37	16 36	csbied	⊢ ( 𝑓 = 𝐹 → ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) = ( 𝐻 ‘ dom 𝐺 ) )
38		eqid	⊢ ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) )
39		fvex	⊢ ( 𝐻 ‘ dom 𝐺 ) ∈ V
40	37 38 39	fvmpt	⊢ ( 𝐹 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } → ( ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
41	12 40	syl	⊢ ( 𝜑 → ( ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
42	9 41	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )