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

Metamath Proof Explorer

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 𝐺 ) )