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