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

Theorem cantnflem3 8110
 Description: Lemma for cantnf 8112. Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than has a normal form, we can use oeeu 7251 to factor into the form where and (and a fortiori ). Then since , has a normal form, and by appending the term using cantnfp1 8100 we get a normal form for . (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.s CNF
cantnfs.a
cantnfs.b
oemapval.t
cantnf.c
cantnf.s CNF
cantnf.e
cantnf.x
cantnf.p
cantnf.y
cantnf.z
cantnf.g
cantnf.v CNF
cantnf.f
Assertion
Ref Expression
cantnflem3 CNF
Distinct variable groups:   ,,,,,,   ,,,,,,,,   ,,,,,,,,,   ,,   ,,,,   ,,,,,   ,,,,   ,,,,,,   ,,,,   ,,,,,   ,,,,,,,,
Allowed substitution hints:   (,,,,)   (,,)   ()   (,,,,,,,,)   (,,,)   (,,,,,,)   (,,,,)   (,,)   ()   (,,,)   (,,,,)

Proof of Theorem cantnflem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . . . 5 CNF
2 cantnfs.a . . . . 5
3 cantnfs.b . . . . 5
4 cantnf.g . . . . 5
5 oemapval.t . . . . . . . . . . . . . 14
6 cantnf.c . . . . . . . . . . . . . 14
7 cantnf.s . . . . . . . . . . . . . 14 CNF
8 cantnf.e . . . . . . . . . . . . . 14
91, 2, 3, 5, 6, 7, 8cantnflem2 8109 . . . . . . . . . . . . 13
10 eqid 2441 . . . . . . . . . . . . . . 15
11 eqid 2441 . . . . . . . . . . . . . . 15
12 eqid 2441 . . . . . . . . . . . . . . 15
1310, 11, 123pm3.2i 1173 . . . . . . . . . . . . . 14
14 cantnf.x . . . . . . . . . . . . . . 15
15 cantnf.p . . . . . . . . . . . . . . 15
16 cantnf.y . . . . . . . . . . . . . . 15
17 cantnf.z . . . . . . . . . . . . . . 15
1814, 15, 16, 17oeeui 7250 . . . . . . . . . . . . . 14
1913, 18mpbiri 233 . . . . . . . . . . . . 13
209, 19syl 16 . . . . . . . . . . . 12
2120simpld 459 . . . . . . . . . . 11
2221simp1d 1007 . . . . . . . . . 10
23 oecl 7186 . . . . . . . . . 10
242, 22, 23syl2anc 661 . . . . . . . . 9
2521simp2d 1008 . . . . . . . . . . 11
2625eldifad 3471 . . . . . . . . . 10
27 onelon 4890 . . . . . . . . . 10
282, 26, 27syl2anc 661 . . . . . . . . 9
29 dif1o 7149 . . . . . . . . . . . 12
3029simprbi 464 . . . . . . . . . . 11
3125, 30syl 16 . . . . . . . . . 10
32 on0eln0 4920 . . . . . . . . . . 11
3328, 32syl 16 . . . . . . . . . 10
3431, 33mpbird 232 . . . . . . . . 9
35 omword1 7221 . . . . . . . . 9
3624, 28, 34, 35syl21anc 1226 . . . . . . . 8
37 omcl 7185 . . . . . . . . . . 11
3824, 28, 37syl2anc 661 . . . . . . . . . 10
3921simp3d 1009 . . . . . . . . . . 11
40 onelon 4890 . . . . . . . . . . 11
4124, 39, 40syl2anc 661 . . . . . . . . . 10
42 oaword1 7200 . . . . . . . . . 10
4338, 41, 42syl2anc 661 . . . . . . . . 9
4420simprd 463 . . . . . . . . 9
4543, 44sseqtrd 3523 . . . . . . . 8
4636, 45sstrd 3497 . . . . . . 7
47 oecl 7186 . . . . . . . . 9
482, 3, 47syl2anc 661 . . . . . . . 8
49 ontr2 4912 . . . . . . . 8
5024, 48, 49syl2anc 661 . . . . . . 7
5146, 6, 50mp2and 679 . . . . . 6
529simpld 459 . . . . . . 7
53 oeord 7236 . . . . . . 7
5422, 3, 52, 53syl3anc 1227 . . . . . 6
5551, 54mpbird 232 . . . . 5
562adantr 465 . . . . . . . . . . . 12 supp
573adantr 465 . . . . . . . . . . . . 13 supp
58 suppssdm 6913 . . . . . . . . . . . . . . 15 supp
591, 2, 3cantnfs 8085 . . . . . . . . . . . . . . . . . 18 finSupp
604, 59mpbid 210 . . . . . . . . . . . . . . . . 17 finSupp
6160simpld 459 . . . . . . . . . . . . . . . 16
62 fdm 5722 . . . . . . . . . . . . . . . 16
6361, 62syl 16 . . . . . . . . . . . . . . 15
6458, 63syl5sseq 3535 . . . . . . . . . . . . . 14 supp
6564sselda 3487 . . . . . . . . . . . . 13 supp
66 onelon 4890 . . . . . . . . . . . . 13
6757, 65, 66syl2anc 661 . . . . . . . . . . . 12 supp
68 oecl 7186 . . . . . . . . . . . 12
6956, 67, 68syl2anc 661 . . . . . . . . . . 11 supp
7061adantr 465 . . . . . . . . . . . . 13 supp
7170, 65ffvelrnd 6014 . . . . . . . . . . . 12 supp
72 onelon 4890 . . . . . . . . . . . 12
7356, 71, 72syl2anc 661 . . . . . . . . . . 11 supp
74 ffn 5718 . . . . . . . . . . . . . . 15
7561, 74syl 16 . . . . . . . . . . . . . 14
76 0ex 4564 . . . . . . . . . . . . . . 15
7776a1i 11 . . . . . . . . . . . . . 14
78 elsuppfn 6908 . . . . . . . . . . . . . 14 supp
7975, 3, 77, 78syl3anc 1227 . . . . . . . . . . . . 13 supp
8079simplbda 624 . . . . . . . . . . . 12 supp
81 on0eln0 4920 . . . . . . . . . . . . 13
8273, 81syl 16 . . . . . . . . . . . 12 supp
8380, 82mpbird 232 . . . . . . . . . . 11 supp
84 omword1 7221 . . . . . . . . . . 11
8569, 73, 83, 84syl21anc 1226 . . . . . . . . . 10 supp
86 eqid 2441 . . . . . . . . . . . 12 OrdIso supp OrdIso supp
874adantr 465 . . . . . . . . . . . 12 supp
88 eqid 2441 . . . . . . . . . . . 12 seq𝜔 OrdIso supp OrdIso supp seq𝜔 OrdIso supp OrdIso supp
891, 56, 57, 86, 87, 88, 65cantnfle 8090 . . . . . . . . . . 11 supp CNF
90 cantnf.v . . . . . . . . . . . 12 CNF
9190adantr 465 . . . . . . . . . . 11 supp CNF
9289, 91sseqtrd 3523 . . . . . . . . . 10 supp
9385, 92sstrd 3497 . . . . . . . . 9 supp
9439adantr 465 . . . . . . . . 9 supp
9524adantr 465 . . . . . . . . . 10 supp
96 ontr2 4912 . . . . . . . . . 10
9769, 95, 96syl2anc 661 . . . . . . . . 9 supp
9893, 94, 97mp2and 679 . . . . . . . 8 supp
9922adantr 465 . . . . . . . . 9 supp
10052adantr 465 . . . . . . . . 9 supp
101 oeord 7236 . . . . . . . . 9
10267, 99, 100, 101syl3anc 1227 . . . . . . . 8 supp
10398, 102mpbird 232 . . . . . . 7 supp
104103ex 434 . . . . . 6 supp
105104ssrdv 3493 . . . . 5 supp
106 cantnf.f . . . . 5
1071, 2, 3, 4, 55, 26, 105, 106cantnfp1 8100 . . . 4 CNF CNF
108107simprd 463 . . 3 CNF CNF
10990oveq2d 6294 . . 3 CNF
110108, 109, 443eqtrd 2486 . 2 CNF
1111, 2, 3cantnff 8093 . . . 4 CNF
112 ffn 5718 . . . 4 CNF CNF
113111, 112syl 16 . . 3 CNF
114107simpld 459 . . 3
115 fnfvelrn 6010 . . 3 CNF CNF CNF
116113, 114, 115syl2anc 661 . 2 CNF CNF
117110, 116eqeltrrd 2530 1 CNF
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 972   wceq 1381   wcel 1802   wne 2636  wral 2791  wrex 2792  crab 2795  cvv 3093   cdif 3456   wss 3459  c0 3768  cif 3923  cop 4017  cuni 4231  cint 4268   class class class wbr 4434  copab 4491   cmpt 4492   cep 4776  con0 4865   cdm 4986   crn 4987  cio 5536   wfn 5570  wf 5571  cfv 5575  (class class class)co 6278   cmpt2 6280  c1st 6780  c2nd 6781   supp csupp 6900  seq𝜔cseqom 7111  c1o 7122  c2o 7123   coa 7126   comu 7127   coe 7128   finSupp cfsupp 7828  OrdIsocoi 7934   CNF ccnf 8078 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4545  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-uni 4232  df-int 4269  df-iun 4314  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-se 4826  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-isom 5584  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6683  df-1st 6782  df-2nd 6783  df-supp 6901  df-recs 7041  df-rdg 7075  df-seqom 7112  df-1o 7129  df-2o 7130  df-oadd 7133  df-omul 7134  df-oexp 7135  df-er 7310  df-map 7421  df-en 7516  df-dom 7517  df-sdom 7518  df-fin 7519  df-fsupp 7829  df-oi 7935  df-cnf 8079 This theorem is referenced by:  cantnflem4  8111
 Copyright terms: Public domain W3C validator