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

Theorem carddom2 7798
Description: Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 8363, 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 7791 . 2  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  C_  ( card `  B )  ->  A  ~<_  B ) )
2 brdom2 7074 . . 3  |-  ( A  ~<_  B  <->  ( A  ~<  B  \/  A  ~~  B
) )
3 cardon 7765 . . . . . . . 8  |-  ( card `  A )  e.  On
43onelssi 4631 . . . . . . 7  |-  ( (
card `  B )  e.  ( card `  A
)  ->  ( card `  B )  C_  ( card `  A ) )
5 carddomi2 7791 . . . . . . . 8  |-  ( ( B  e.  dom  card  /\  A  e.  dom  card )  ->  ( ( card `  B )  C_  ( card `  A )  ->  B  ~<_  A ) )
65ancoms 440 . . . . . . 7  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  B )  C_  ( card `  A )  ->  B  ~<_  A ) )
7 domnsym 7170 . . . . . . 7  |-  ( B  ~<_  A  ->  -.  A  ~<  B )
84, 6, 7syl56 32 . . . . . 6  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  B )  e.  (
card `  A )  ->  -.  A  ~<  B ) )
98con2d 109 . . . . 5  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~<  B  ->  -.  ( card `  B )  e.  (
card `  A )
) )
10 cardon 7765 . . . . . 6  |-  ( card `  B )  e.  On
11 ontri1 4557 . . . . . 6  |-  ( ( ( card `  A
)  e.  On  /\  ( card `  B )  e.  On )  ->  (
( card `  A )  C_  ( card `  B
)  <->  -.  ( card `  B )  e.  (
card `  A )
) )
123, 10, 11mp2an 654 . . . . 5  |-  ( (
card `  A )  C_  ( card `  B
)  <->  -.  ( card `  B )  e.  (
card `  A )
)
139, 12syl6ibr 219 . . . 4  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~<  B  ->  ( card `  A
)  C_  ( card `  B ) ) )
14 carden2b 7788 . . . . . 6  |-  ( A 
~~  B  ->  ( card `  A )  =  ( card `  B
) )
15 eqimss 3344 . . . . . 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 370 . . 3  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( A 
~<  B  \/  A  ~~  B )  ->  ( card `  A )  C_  ( card `  B )
) )
192, 18syl5bi 209 . 2  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( A  ~<_  B  ->  ( card `  A
)  C_  ( card `  B ) ) )
201, 19impbid 184 1  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  C_  ( card `  B )  <->  A  ~<_  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717    C_ wss 3264   class class class wbr 4154   Oncon0 4523   dom cdm 4819   ` cfv 5395    ~~ cen 7043    ~<_ cdom 7044    ~< csdm 7045   cardccrd 7756
This theorem is referenced by:  carduni  7802  carden2  7808  cardsdom2  7809  domtri2  7810  infxpidm2  7832  cardaleph  7904  infenaleph  7906  alephinit  7910  ficardun2  8017  ackbij2  8057  cfflb  8073  fin1a2lem9  8222  carddom  8363  pwfseqlem5  8472  hashdom  11581
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-int 3994  df-br 4155  df-opab 4209  df-mpt 4210  df-tr 4245  df-eprel 4436  df-id 4440  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-er 6842  df-en 7047  df-dom 7048  df-sdom 7049  df-card 7760
  Copyright terms: Public domain W3C validator