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

Theorem fin67 8649
Description: Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
fin67

Proof of Theorem fin67
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 isfin6 8554 . 2
2 2onn 7163 . . . . . 6
3 ssid 3457 . . . . . 6
4 ssnnfi 7617 . . . . . 6
52, 3, 4mp2an 672 . . . . 5
6 sdomdom 7421 . . . . 5
7 domfi 7619 . . . . 5
85, 6, 7sylancr 663 . . . 4
9 fin17 8648 . . . 4
108, 9syl 16 . . 3
11 sdomnen 7422 . . . . 5
12 eldifi 3560 . . . . . . . . 9
13 ensym 7442 . . . . . . . . 9
14 isnumi 8201 . . . . . . . . 9
1512, 13, 14syl2an 477 . . . . . . . 8
16 vex 3055 . . . . . . . . . . 11
17 eldif 3420 . . . . . . . . . . . 12
18 ordom 6569 . . . . . . . . . . . . . 14
19 eloni 4811 . . . . . . . . . . . . . 14
20 ordtri1 4834 . . . . . . . . . . . . . 14
2118, 19, 20sylancr 663 . . . . . . . . . . . . 13
2221biimpar 485 . . . . . . . . . . . 12
2317, 22sylbi 195 . . . . . . . . . . 11
24 ssdomg 7439 . . . . . . . . . . 11
2516, 23, 24mpsyl 63 . . . . . . . . . 10
26 domen2 7538 . . . . . . . . . 10
2725, 26syl5ibr 221 . . . . . . . . 9
2827impcom 430 . . . . . . . 8
29 infxpidm2 8268 . . . . . . . 8
3015, 28, 29syl2anc 661 . . . . . . 7
31 ensym 7442 . . . . . . 7
3230, 31syl 16 . . . . . 6
3332rexlimiva 2916 . . . . 5
3411, 33nsyl 121 . . . 4
35 relsdom 7401 . . . . . 6
3635brrelexi 4961 . . . . 5
37 isfin7 8555 . . . . 5
3836, 37syl 16 . . . 4
3934, 38mpbird 232 . . 3
4010, 39jaoi 379 . 2
411, 40sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  e.wcel 1757  E.wrex 2793   cvv 3052  \cdif 3407  C_wss 3410   class class class wbr 4374  Ordword 4800   con0 4801  X.cxp 4920  domcdm 4922   com 6560   c2o 6998   cen 7391   cdom 7392   csdm 7393   cfn 7394   ccrd 8190   cfin6 8537   cfin7 8538
This theorem is referenced by:  fin2so  28538
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  ax-inf2 7932
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  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-int 4211  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-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-1o 7004  df-2o 7005  df-oadd 7008  df-er 7185  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-oi 7809  df-card 8194  df-fin6 8544  df-fin7 8545
  Copyright terms: Public domain W3C validator