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

Theorem carddom2 8271
Description: Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 8842, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
carddom2  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  C_  ( card `  B )  <->  A  ~<_  B ) )

Proof of Theorem carddom2
StepHypRef Expression
1 carddomi2 8264 . 2  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  C_  ( card `  B )  ->  A  ~<_  B ) )
2 brdom2 7464 . . 3  |-  ( A  ~<_  B  <->  ( A  ~<  B  \/  A  ~~  B
) )
3 cardon 8238 . . . . . . . 8  |-  ( card `  A )  e.  On
43onelssi 4900 . . . . . . 7  |-  ( (
card `  B )  e.  ( card `  A
)  ->  ( card `  B )  C_  ( card `  A ) )
5 carddomi2 8264 . . . . . . . 8  |-  ( ( B  e.  dom  card  /\  A  e.  dom  card )  ->  ( ( card `  B )  C_  ( card `  A )  ->  B  ~<_  A ) )
65ancoms 451 . . . . . . 7  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  B )  C_  ( card `  A )  ->  B  ~<_  A ) )
7 domnsym 7562 . . . . . . 7  |-  ( B  ~<_  A  ->  -.  A  ~<  B )
84, 6, 7syl56 34 . . . . . 6  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  B )  e.  (
card `  A )  ->  -.  A  ~<  B ) )
98con2d 115 . . . . 5  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~<  B  ->  -.  ( card `  B )  e.  (
card `  A )
) )
10 cardon 8238 . . . . . 6  |-  ( card `  B )  e.  On
11 ontri1 4826 . . . . . 6  |-  ( ( ( card `  A
)  e.  On  /\  ( card `  B )  e.  On )  ->  (
( card `  A )  C_  ( card `  B
)  <->  -.  ( card `  B )  e.  (
card `  A )
) )
123, 10, 11mp2an 670 . . . . 5  |-  ( (
card `  A )  C_  ( card `  B
)  <->  -.  ( card `  B )  e.  (
card `  A )
)
139, 12syl6ibr 227 . . . 4  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~<  B  ->  ( card `  A
)  C_  ( card `  B ) ) )
14 carden2b 8261 . . . . . 6  |-  ( A 
~~  B  ->  ( card `  A )  =  ( card `  B
) )
15 eqimss 3469 . . . . . 6  |-  ( (
card `  A )  =  ( card `  B
)  ->  ( card `  A )  C_  ( card `  B ) )
1614, 15syl 16 . . . . 5  |-  ( A 
~~  B  ->  ( card `  A )  C_  ( card `  B )
)
1716a1i 11 . . . 4  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~~  B  ->  ( card `  A
)  C_  ( card `  B ) ) )
1813, 17jaod 378 . . 3  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( A 
~<  B  \/  A  ~~  B )  ->  ( card `  A )  C_  ( card `  B )
) )
192, 18syl5bi 217 . 2  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~<_  B  ->  ( card `  A
)  C_  ( card `  B ) ) )
201, 19impbid 191 1  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  C_  ( card `  B )  <->  A  ~<_  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    = wceq 1399    e. wcel 1826    C_ wss 3389   class class class wbr 4367   Oncon0 4792   dom cdm 4913   ` cfv 5496    ~~ cen 7432    ~<_ cdom 7433    ~< csdm 7434   cardccrd 8229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-card 8233
This theorem is referenced by:  carduni  8275  carden2  8281  cardsdom2  8282  domtri2  8283  infxpidm2  8307  cardaleph  8383  infenaleph  8385  alephinit  8389  ficardun2  8496  ackbij2  8536  cfflb  8552  fin1a2lem9  8701  carddom  8842  pwfseqlem5  8952  hashdom  12350
  Copyright terms: Public domain W3C validator