Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfcom2 Unicode version

Theorem cnfcom2 7615
 Description: Any nonzero ordinal is equinumerous to the leading term of its Cantor normal form. (Contributed by Mario Carneiro, 30-May-2015.)
Hypotheses
Ref Expression
cnfcom.s CNF
cnfcom.a
cnfcom.b
cnfcom.f CNF
cnfcom.g OrdIso
cnfcom.h seq𝜔
cnfcom.t seq𝜔
cnfcom.m
cnfcom.k
cnfcom.w
cnfcom2.1
Assertion
Ref Expression
cnfcom2
Distinct variable groups:   ,,,   ,   ,,,,   ,   ,   ,,,,   ,,   ,,   ,,,
Allowed substitution hints:   ()   ()   (,,,)   (,)   (,,)   (,)   (,,,)   (,,)   (,,)

Proof of Theorem cnfcom2
StepHypRef Expression
1 cnfcom.s . . . . 5 CNF
2 cnfcom.a . . . . 5
3 cnfcom.b . . . . 5
4 cnfcom.f . . . . 5 CNF
5 cnfcom.g . . . . 5 OrdIso
6 cnfcom.h . . . . 5 seq𝜔
7 cnfcom.t . . . . 5 seq𝜔
8 cnfcom.m . . . . 5
9 cnfcom.k . . . . 5
10 fvex 5701 . . . . . . . . . . . 12 CNF
114, 10eqeltri 2474 . . . . . . . . . . 11
1211cnvex 5365 . . . . . . . . . 10
13 imaexg 5176 . . . . . . . . . 10
145oion 7461 . . . . . . . . . 10
1512, 13, 14mp2b 10 . . . . . . . . 9
1615elexi 2925 . . . . . . . 8
1716uniex 4664 . . . . . . 7
1817sucid 4620 . . . . . 6
19 cnfcom.w . . . . . . 7
20 cnfcom2.1 . . . . . . 7
211, 2, 3, 4, 5, 6, 7, 8, 9, 19, 20cnfcom2lem 7614 . . . . . 6
2218, 21syl5eleqr 2491 . . . . 5
231, 2, 3, 4, 5, 6, 7, 8, 9, 22cnfcom 7613 . . . 4
2419oveq2i 6051 . . . . . 6
2519fveq2i 5690 . . . . . 6
2624, 25oveq12i 6052 . . . . 5
27 f1oeq3 5626 . . . . 5
2826, 27ax-mp 8 . . . 4
2923, 28sylibr 204 . . 3
3021fveq2d 5691 . . . 4
31 f1oeq1 5624 . . . 4
3230, 31syl 16 . . 3
3329, 32mpbird 224 . 2
344fveq2i 5690 . . . . 5 CNF CNF CNF
35 omelon 7557 . . . . . . 7
3635a1i 11 . . . . . 6
371, 36, 2cantnff1o 7608 . . . . . . . . 9 CNF
38 f1ocnv 5646 . . . . . . . . 9 CNF CNF
39 f1of 5633 . . . . . . . . 9 CNF CNF
4037, 38, 393syl 19 . . . . . . . 8 CNF
4140, 3ffvelrnd 5830 . . . . . . 7 CNF
424, 41syl5eqel 2488 . . . . . 6
438oveq1i 6050 . . . . . . . . . 10
4443a1i 11 . . . . . . . . 9
4544mpt2eq3ia 6098 . . . . . . . 8
46 eqid 2404 . . . . . . . 8
47 seqomeq12 6670 . . . . . . . 8 seq𝜔 seq𝜔
4845, 46, 47mp2an 654 . . . . . . 7 seq𝜔 seq𝜔
496, 48eqtri 2424 . . . . . 6 seq𝜔
501, 36, 2, 5, 42, 49cantnfval 7579 . . . . 5 CNF
5134, 50syl5reqr 2451 . . . 4 CNF CNF
5221fveq2d 5691 . . . 4
53 f1ocnvfv2 5974 . . . . 5 CNF CNF CNF
5437, 3, 53syl2anc 643 . . . 4 CNF CNF
5551, 52, 543eqtr3d 2444 . . 3
56 f1oeq2 5625 . . 3
5755, 56syl 16 . 2
5833, 57mpbid 202 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1649   wcel 1721  cvv 2916   cdif 3277   cun 3278  c0 3588  cuni 3975   cmpt 4226   cep 4452  con0 4541   csuc 4543  com 4804  ccnv 4836   cdm 4837  cima 4840  wf 5409  wf1o 5412  cfv 5413  (class class class)co 6040   cmpt2 6042  seq𝜔cseqom 6663  c1o 6676   coa 6680   comu 6681   coe 6682  OrdIsocoi 7434   CNF ccnf 7572 This theorem is referenced by:  cnfcom3  7617 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-seqom 6664  df-1o 6683  df-2o 6684  df-oadd 6687  df-omul 6688  df-oexp 6689  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-cnf 7573
 Copyright terms: Public domain W3C validator