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

Theorem cantnfval2 8121
 Description: Alternate expression for the value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.)
Hypotheses
Ref Expression
cantnfs.s CNF
cantnfs.a
cantnfs.b
cantnfcl.g OrdIso supp
cantnfcl.f
cantnfval.h seq𝜔
Assertion
Ref Expression
cantnfval2 CNF seq𝜔
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem cantnfval2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . 3 CNF
2 cantnfs.a . . 3
3 cantnfs.b . . 3
4 cantnfcl.g . . 3 OrdIso supp
5 cantnfcl.f . . 3
6 cantnfval.h . . 3 seq𝜔
71, 2, 3, 4, 5, 6cantnfval 8120 . 2 CNF
8 ssid 3421 . . 3
91, 2, 3, 4, 5cantnfcl 8119 . . . . 5 supp
109simprd 464 . . . 4
11 sseq1 3423 . . . . . . 7
12 fveq2 5820 . . . . . . . . 9
13 0ex 4494 . . . . . . . . . 10
146seqom0g 7123 . . . . . . . . . 10
1513, 14ax-mp 5 . . . . . . . . 9
1612, 15syl6eq 2473 . . . . . . . 8
17 fveq2 5820 . . . . . . . . 9 seq𝜔 seq𝜔
18 eqid 2423 . . . . . . . . . . 11 seq𝜔 seq𝜔
1918seqom0g 7123 . . . . . . . . . 10 seq𝜔
2013, 19ax-mp 5 . . . . . . . . 9 seq𝜔
2117, 20syl6eq 2473 . . . . . . . 8 seq𝜔
2216, 21eqeq12d 2438 . . . . . . 7 seq𝜔
2311, 22imbi12d 321 . . . . . 6 seq𝜔
2423imbi2d 317 . . . . 5 seq𝜔
25 sseq1 3423 . . . . . . 7
26 fveq2 5820 . . . . . . . 8
27 fveq2 5820 . . . . . . . 8 seq𝜔 seq𝜔
2826, 27eqeq12d 2438 . . . . . . 7 seq𝜔 seq𝜔
2925, 28imbi12d 321 . . . . . 6 seq𝜔 seq𝜔
3029imbi2d 317 . . . . 5 seq𝜔 seq𝜔
31 sseq1 3423 . . . . . . 7
32 fveq2 5820 . . . . . . . 8
33 fveq2 5820 . . . . . . . 8 seq𝜔 seq𝜔
3432, 33eqeq12d 2438 . . . . . . 7 seq𝜔 seq𝜔
3531, 34imbi12d 321 . . . . . 6 seq𝜔 seq𝜔
3635imbi2d 317 . . . . 5 seq𝜔 seq𝜔
37 sseq1 3423 . . . . . . 7
38 fveq2 5820 . . . . . . . 8
39 fveq2 5820 . . . . . . . 8 seq𝜔 seq𝜔
4038, 39eqeq12d 2438 . . . . . . 7 seq𝜔 seq𝜔
4137, 40imbi12d 321 . . . . . 6 seq𝜔 seq𝜔
4241imbi2d 317 . . . . 5 seq𝜔 seq𝜔
43 eqid 2423 . . . . . 6
44432a1i 12 . . . . 5
45 sssucid 5457 . . . . . . . . . 10
46 sstr 3410 . . . . . . . . . 10
4745, 46mpan 674 . . . . . . . . 9
4847imim1i 60 . . . . . . . 8 seq𝜔 seq𝜔
49 oveq2 6252 . . . . . . . . . . 11 seq𝜔 seq𝜔
506seqomsuc 7124 . . . . . . . . . . . . 13
5150ad2antrl 732 . . . . . . . . . . . 12
5218seqomsuc 7124 . . . . . . . . . . . . . 14 seq𝜔 seq𝜔
5352ad2antrl 732 . . . . . . . . . . . . 13 seq𝜔 seq𝜔
54 ssv 3422 . . . . . . . . . . . . . . . 16
55 ssv 3422 . . . . . . . . . . . . . . . 16
56 resmpt2 6347 . . . . . . . . . . . . . . . 16
5754, 55, 56mp2an 676 . . . . . . . . . . . . . . 15
5857oveqi 6257 . . . . . . . . . . . . . 14 seq𝜔 seq𝜔
59 simprr 764 . . . . . . . . . . . . . . . 16
60 vex 3020 . . . . . . . . . . . . . . . . . 18
6160sucid 5459 . . . . . . . . . . . . . . . . 17
6261a1i 11 . . . . . . . . . . . . . . . 16
6359, 62sseldd 3403 . . . . . . . . . . . . . . 15
6418cantnfvalf 8117 . . . . . . . . . . . . . . . . 17 seq𝜔
6564ffvelrni 5975 . . . . . . . . . . . . . . . 16 seq𝜔
6665ad2antrl 732 . . . . . . . . . . . . . . 15 seq𝜔
67 ovres 6389 . . . . . . . . . . . . . . 15 seq𝜔 seq𝜔 seq𝜔
6863, 66, 67syl2anc 665 . . . . . . . . . . . . . 14 seq𝜔 seq𝜔
6958, 68syl5eqr 2471 . . . . . . . . . . . . 13 seq𝜔 seq𝜔
7053, 69eqtrd 2457 . . . . . . . . . . . 12 seq𝜔 seq𝜔
7151, 70eqeq12d 2438 . . . . . . . . . . 11 seq𝜔 seq𝜔
7249, 71syl5ibr 224 . . . . . . . . . 10 seq𝜔 seq𝜔
7372expr 618 . . . . . . . . 9 seq𝜔 seq𝜔
7473a2d 29 . . . . . . . 8 seq𝜔 seq𝜔
7548, 74syl5 33 . . . . . . 7 seq𝜔 seq𝜔
7675expcom 436 . . . . . 6 seq𝜔 seq𝜔
7776a2d 29 . . . . 5 seq𝜔 seq𝜔
7824, 30, 36, 42, 44, 77finds 6672 . . . 4 seq𝜔
7910, 78mpcom 37 . . 3 seq𝜔
808, 79mpi 20 . 2 seq𝜔
817, 80eqtrd 2457 1 CNF seq𝜔
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1872  cvv 3017   wss 3374  c0 3699   cep 4700   wwe 4749   cxp 4789   cdm 4791   cres 4793  con0 5380   csuc 5382  cfv 5539  (class class class)co 6244   cmpt2 6246  com 6645   supp csupp 6864  seq𝜔cseqom 7114   coa 7129   comu 7130   coe 7131  OrdIsocoi 7972   CNF ccnf 8113 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-supp 6865  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-seqom 7115  df-oadd 7136  df-er 7313  df-map 7424  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-fsupp 7832  df-oi 7973  df-cnf 8114 This theorem is referenced by:  cantnfres  8129
 Copyright terms: Public domain W3C validator