Metamath Proof Explorer


Theorem cantnffval

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 cantnffval.s 𝑆 = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ }
cantnffval.a ( 𝜑𝐴 ∈ On )
cantnffval.b ( 𝜑𝐵 ∈ On )
Assertion cantnffval ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ( 𝑓𝑆 OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) )

Proof

Step Hyp Ref Expression
1 cantnffval.s 𝑆 = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ }
2 cantnffval.a ( 𝜑𝐴 ∈ On )
3 cantnffval.b ( 𝜑𝐵 ∈ On )
4 oveq12 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑥m 𝑦 ) = ( 𝐴m 𝐵 ) )
5 4 rabeqdv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → { 𝑔 ∈ ( 𝑥m 𝑦 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
6 5 1 eqtr4di ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → { 𝑔 ∈ ( 𝑥m 𝑦 ) ∣ 𝑔 finSupp ∅ } = 𝑆 )
7 simp1l ( ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∧ 𝑘 ∈ V ∧ 𝑧 ∈ V ) → 𝑥 = 𝐴 )
8 7 oveq1d ( ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∧ 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥o ( 𝑘 ) ) = ( 𝐴o ( 𝑘 ) ) )
9 8 oveq1d ( ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∧ 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) = ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) )
10 9 oveq1d ( ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∧ 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) = ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) )
11 10 mpoeq3dva ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) )
12 eqid ∅ = ∅
13 seqomeq12 ( ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) ∧ ∅ = ∅ ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
14 11 12 13 sylancl ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
15 14 fveq1d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) )
16 15 csbeq2dv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) = OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) )
17 6 16 mpteq12dv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) = ( 𝑓𝑆 OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) )
18 df-cnf CNF = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( 𝑓 ∈ { 𝑔 ∈ ( 𝑥m 𝑦 ) ∣ 𝑔 finSupp ∅ } ↦ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝑥o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) )
19 ovex ( 𝐴m 𝐵 ) ∈ V
20 1 19 rabex2 𝑆 ∈ V
21 20 mptex ( 𝑓𝑆 OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) ∈ V
22 17 18 21 ovmpoa ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 CNF 𝐵 ) = ( 𝑓𝑆 OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) )
23 2 3 22 syl2anc ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ( 𝑓𝑆 OrdIso ( E , ( 𝑓 supp ∅ ) ) / ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴o ( 𝑘 ) ) ·o ( 𝑓 ‘ ( 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ) ) )