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

Definition df-cnf 9606
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 ๐‘ฅ โ†‘o ๐‘ฆ. The content of the original Cantor Normal Form theorem is that for ๐‘ฅ = ฯ‰ this function is a bijection onto ฯ‰ โ†‘o ๐‘ฆ 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 9639 of this function in terms of df-oi 9454. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
Assertion
Ref Expression
df-cnf CNF = (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ (๐‘“ โˆˆ {๐‘” โˆˆ (๐‘ฅ โ†‘m ๐‘ฆ) โˆฃ ๐‘” finSupp โˆ…} โ†ฆ โฆ‹OrdIso( E , (๐‘“ supp โˆ…)) / โ„ŽโฆŒ(seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom โ„Ž)))
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘“,๐‘”,โ„Ž,๐‘˜,๐‘ง

Detailed syntax breakdown of Definition df-cnf
StepHypRef Expression
1 ccnf 9605 . 2 class CNF
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 con0 6321 . . 3 class On
5 vf . . . 4 setvar ๐‘“
6 vg . . . . . . 7 setvar ๐‘”
76cv 1541 . . . . . 6 class ๐‘”
8 c0 4286 . . . . . 6 class โˆ…
9 cfsupp 9311 . . . . . 6 class finSupp
107, 8, 9wbr 5109 . . . . 5 wff ๐‘” finSupp โˆ…
112cv 1541 . . . . . 6 class ๐‘ฅ
123cv 1541 . . . . . 6 class ๐‘ฆ
13 cmap 8771 . . . . . 6 class โ†‘m
1411, 12, 13co 7361 . . . . 5 class (๐‘ฅ โ†‘m ๐‘ฆ)
1510, 6, 14crab 3406 . . . 4 class {๐‘” โˆˆ (๐‘ฅ โ†‘m ๐‘ฆ) โˆฃ ๐‘” finSupp โˆ…}
16 vh . . . . 5 setvar โ„Ž
175cv 1541 . . . . . . 7 class ๐‘“
18 csupp 8096 . . . . . . 7 class supp
1917, 8, 18co 7361 . . . . . 6 class (๐‘“ supp โˆ…)
20 cep 5540 . . . . . 6 class E
2119, 20coi 9453 . . . . 5 class OrdIso( E , (๐‘“ supp โˆ…))
2216cv 1541 . . . . . . 7 class โ„Ž
2322cdm 5637 . . . . . 6 class dom โ„Ž
24 vk . . . . . . . 8 setvar ๐‘˜
25 vz . . . . . . . 8 setvar ๐‘ง
26 cvv 3447 . . . . . . . 8 class V
2724cv 1541 . . . . . . . . . . . 12 class ๐‘˜
2827, 22cfv 6500 . . . . . . . . . . 11 class (โ„Žโ€˜๐‘˜)
29 coe 8415 . . . . . . . . . . 11 class โ†‘o
3011, 28, 29co 7361 . . . . . . . . . 10 class (๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜))
3128, 17cfv 6500 . . . . . . . . . 10 class (๐‘“โ€˜(โ„Žโ€˜๐‘˜))
32 comu 8414 . . . . . . . . . 10 class ยทo
3330, 31, 32co 7361 . . . . . . . . 9 class ((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜)))
3425cv 1541 . . . . . . . . 9 class ๐‘ง
35 coa 8413 . . . . . . . . 9 class +o
3633, 34, 35co 7361 . . . . . . . 8 class (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)
3724, 25, 26, 26, 36cmpo 7363 . . . . . . 7 class (๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง))
3837, 8cseqom 8397 . . . . . 6 class seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
3923, 38cfv 6500 . . . . 5 class (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom โ„Ž)
4016, 21, 39csb 3859 . . . 4 class โฆ‹OrdIso( E , (๐‘“ supp โˆ…)) / โ„ŽโฆŒ(seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom โ„Ž)
415, 15, 40cmpt 5192 . . 3 class (๐‘“ โˆˆ {๐‘” โˆˆ (๐‘ฅ โ†‘m ๐‘ฆ) โˆฃ ๐‘” finSupp โˆ…} โ†ฆ โฆ‹OrdIso( E , (๐‘“ supp โˆ…)) / โ„ŽโฆŒ(seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom โ„Ž))
422, 3, 4, 4, 41cmpo 7363 . 2 class (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ (๐‘“ โˆˆ {๐‘” โˆˆ (๐‘ฅ โ†‘m ๐‘ฆ) โˆฃ ๐‘” finSupp โˆ…} โ†ฆ โฆ‹OrdIso( E , (๐‘“ supp โˆ…)) / โ„ŽโฆŒ(seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom โ„Ž)))
431, 42wceq 1542 1 wff CNF = (๐‘ฅ โˆˆ On, ๐‘ฆ โˆˆ On โ†ฆ (๐‘“ โˆˆ {๐‘” โˆˆ (๐‘ฅ โ†‘m ๐‘ฆ) โˆฃ ๐‘” finSupp โˆ…} โ†ฆ โฆ‹OrdIso( E , (๐‘“ supp โˆ…)) / โ„ŽโฆŒ(seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐‘ฅ โ†‘o (โ„Žโ€˜๐‘˜)) ยทo (๐‘“โ€˜(โ„Žโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom โ„Ž)))
Colors of variables: wff setvar class
This definition is referenced by:  cantnffval  9607
  Copyright terms: Public domain W3C validator