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

Theorem cantnfval 7961
Description: 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
cantnfs.a
cantnfs.b
cantnfcl.g
cantnfcl.f
cantnfval.h
Assertion
Ref Expression
cantnfval
Distinct variable groups:   , ,   , ,   , ,   S, ,   , ,   , ,

Proof of Theorem cantnfval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2450 . . . 4
2 cantnfs.a . . . 4
3 cantnfs.b . . . 4
41, 2, 3cantnffval 7954 . . 3
54fveq1d 5775 . 2
6 cantnfcl.f . . . 4
7 cantnfs.s . . . . 5
81, 2, 3cantnfdm 7955 . . . . 5
97, 8syl5eq 2502 . . . 4
106, 9eleqtrd 2538 . . 3
11 ovex 6199 . . . . . 6
12 eqid 2450 . . . . . . 7
1312oiexg 7834 . . . . . 6
1411, 13mp1i 12 . . . . 5
15 simpr 461 . . . . . . . . . . . . . . 15
16 oveq1 6181 . . . . . . . . . . . . . . . . 17
1716adantr 465 . . . . . . . . . . . . . . . 16
18 oieq2 7812 . . . . . . . . . . . . . . . 16
1917, 18syl 16 . . . . . . . . . . . . . . 15
2015, 19eqtrd 2490 . . . . . . . . . . . . . 14
21 cantnfcl.g . . . . . . . . . . . . . 14
2220, 21syl6eqr 2508 . . . . . . . . . . . . 13
2322fveq1d 5775 . . . . . . . . . . . 12
2423oveq2d 6190 . . . . . . . . . . 11
25 simpl 457 . . . . . . . . . . . 12
2625, 23fveq12d 5779 . . . . . . . . . . 11
2724, 26oveq12d 6192 . . . . . . . . . 10
2827oveq1d 6189 . . . . . . . . 9
2928mpt2eq3dv 6235 . . . . . . . 8
30 eqid 2450 . . . . . . . 8
31 seqomeq12 6993 . . . . . . . 8
3229, 30, 31sylancl 662 . . . . . . 7
33 cantnfval.h . . . . . . 7
3432, 33syl6eqr 2508 . . . . . 6
3522dmeqd 5124 . . . . . 6
3634, 35fveq12d 5779 . . . . 5
3714, 36csbied 3396 . . . 4
38 eqid 2450 . . . 4
39 fvex 5783 . . . 4
4037, 38, 39fvmpt 5857 . . 3
4110, 40syl 16 . 2
425, 41eqtrd 2490 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1370  e.wcel 1757  {crab 2796   cvv 3052  [_csb 3370   c0 3719   class class class wbr 4374  e.cmpt 4432   cep 4712   con0 4801  domcdm 4922  `cfv 5500  (class class class)co 6174  e.cmpt2 6176   csupp 6774  seqomcseqom 6986   coa 7001   comu 7002   coe 7003   cmap 7298   cfsupp 7705  OrdIsocoi 7808   ccnf 7952
This theorem is referenced by:  cantnfval2  7962  cantnfle  7964  cantnflt2  7966  cantnff  7967  cantnf0  7968  cantnfp1lem3  7973  cantnflem1  7982  cantnf  7986  cnfcom2  8020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-se 4762  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-isom 5509  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-recs 6916  df-rdg 6950  df-seqom 6987  df-oi 7809  df-cnf 7953
  Copyright terms: Public domain W3C validator