Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnf Structured version   Visualization version   GIF version

Definition df-cnf 8442
 Description: Define the Cantor normal form function, which takes as input a finitely supported function from 𝑦 to 𝑥 and outputs the corresponding member of the ordinal exponential 𝑥 ↑𝑜 𝑦. The content of the original Cantor Normal Form theorem is that for 𝑥 = ω this function is a bijection onto ω ↑𝑜 𝑦 for any ordinal 𝑦 (or, since the function restricts naturally to different ordinals, the statement that the composite function is a bijection to On). More can be said about the function, however, and in particular it is an order isomorphism for a certain easily defined well-ordering of the finitely supported functions, which gives an alternate definition cantnffval2 8475 of this function in terms of df-oi 8298. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
Assertion
Ref Expression
df-cnf CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ OrdIso( E , (𝑓 supp ∅)) / (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)‘dom )))
Distinct variable group:   𝑥,𝑦,𝑓,𝑔,,𝑘,𝑧

Detailed syntax breakdown of Definition df-cnf
StepHypRef Expression
1 ccnf 8441 . 2 class CNF
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 con0 5640 . . 3 class On
5 vf . . . 4 setvar 𝑓
6 vg . . . . . . 7 setvar 𝑔
76cv 1474 . . . . . 6 class 𝑔
8 c0 3874 . . . . . 6 class
9 cfsupp 8158 . . . . . 6 class finSupp
107, 8, 9wbr 4583 . . . . 5 wff 𝑔 finSupp ∅
112cv 1474 . . . . . 6 class 𝑥
123cv 1474 . . . . . 6 class 𝑦
13 cmap 7744 . . . . . 6 class 𝑚
1411, 12, 13co 6549 . . . . 5 class (𝑥𝑚 𝑦)
1510, 6, 14crab 2900 . . . 4 class {𝑔 ∈ (𝑥𝑚 𝑦) ∣ 𝑔 finSupp ∅}
16 vh . . . . 5 setvar
175cv 1474 . . . . . . 7 class 𝑓
18 csupp 7182 . . . . . . 7 class supp
1917, 8, 18co 6549 . . . . . 6 class (𝑓 supp ∅)
20 cep 4947 . . . . . 6 class E
2119, 20coi 8297 . . . . 5 class OrdIso( E , (𝑓 supp ∅))
2216cv 1474 . . . . . . 7 class
2322cdm 5038 . . . . . 6 class dom
24 vk . . . . . . . 8 setvar 𝑘
25 vz . . . . . . . 8 setvar 𝑧
26 cvv 3173 . . . . . . . 8 class V
2724cv 1474 . . . . . . . . . . . 12 class 𝑘
2827, 22cfv 5804 . . . . . . . . . . 11 class (𝑘)
29 coe 7446 . . . . . . . . . . 11 class 𝑜
3011, 28, 29co 6549 . . . . . . . . . 10 class (𝑥𝑜 (𝑘))
3128, 17cfv 5804 . . . . . . . . . 10 class (𝑓‘(𝑘))
32 comu 7445 . . . . . . . . . 10 class ·𝑜
3330, 31, 32co 6549 . . . . . . . . 9 class ((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘)))
3425cv 1474 . . . . . . . . 9 class 𝑧
35 coa 7444 . . . . . . . . 9 class +𝑜
3633, 34, 35co 6549 . . . . . . . 8 class (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)
3724, 25, 26, 26, 36cmpt2 6551 . . . . . . 7 class (𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧))
3837, 8cseqom 7429 . . . . . 6 class seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)
3923, 38cfv 5804 . . . . 5 class (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)‘dom )
4016, 21, 39csb 3499 . . . 4 class OrdIso( E , (𝑓 supp ∅)) / (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)‘dom )
415, 15, 40cmpt 4643 . . 3 class (𝑓 ∈ {𝑔 ∈ (𝑥𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ OrdIso( E , (𝑓 supp ∅)) / (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)‘dom ))
422, 3, 4, 4, 41cmpt2 6551 . 2 class (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ OrdIso( E , (𝑓 supp ∅)) / (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)‘dom )))
431, 42wceq 1475 1 wff CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ OrdIso( E , (𝑓 supp ∅)) / (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥𝑜 (𝑘)) ·𝑜 (𝑓‘(𝑘))) +𝑜 𝑧)), ∅)‘dom )))
 Colors of variables: wff setvar class This definition is referenced by:  cantnffval  8443
 Copyright terms: Public domain W3C validator