Metamath Proof Explorer

Theorem carddom2

Description: Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom , which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion carddom2 
|- ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) )

Proof

Step Hyp Ref Expression
1 carddomi2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) -> A ~<_ B ) )
2 brdom2 
 |-  ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )
3 cardon 
 |-  ( card ` A ) e. On
4 3 onelssi 
 |-  ( ( card ` B ) e. ( card ` A ) -> ( card ` B ) C_ ( card ` A ) )
5 carddomi2 
 |-  ( ( B e. dom card /\ A e. dom card ) -> ( ( card ` B ) C_ ( card ` A ) -> B ~<_ A ) )
6 5 ancoms 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` B ) C_ ( card ` A ) -> B ~<_ A ) )
7 domnsym 
 |-  ( B ~<_ A -> -. A ~< B )
8 4 6 7 syl56 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` B ) e. ( card ` A ) -> -. A ~< B ) )
9 8 con2d 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A ~< B -> -. ( card ` B ) e. ( card ` A ) ) )
10 cardon 
 |-  ( card ` B ) e. On
11 ontri1 
 |-  ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) )
12 3 10 11 mp2an 
 |-  ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) )
13 9 12 imbitrrdi 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A ~< B -> ( card ` A ) C_ ( card ` B ) ) )
14 carden2b 
 |-  ( A ~~ B -> ( card ` A ) = ( card ` B ) )
15 eqimss 
 |-  ( ( card ` A ) = ( card ` B ) -> ( card ` A ) C_ ( card ` B ) )
16 14 15 syl 
 |-  ( A ~~ B -> ( card ` A ) C_ ( card ` B ) )
17 16 a1i 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A ~~ B -> ( card ` A ) C_ ( card ` B ) ) )
18 13 17 jaod 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( A ~< B \/ A ~~ B ) -> ( card ` A ) C_ ( card ` B ) ) )
19 2 18 biimtrid 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B -> ( card ` A ) C_ ( card ` B ) ) )
20 1 19 impbid 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) )