This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem carddomi2

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

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

Proof

Step Hyp Ref Expression
1 cardnueq0 
 |-  ( A e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) )
2 1 adantr 
 |-  ( ( A e. dom card /\ B e. V ) -> ( ( card ` A ) = (/) <-> A = (/) ) )
3 2 biimpa 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( card ` A ) = (/) ) -> A = (/) )
4 0domg 
 |-  ( B e. V -> (/) ~<_ B )
5 4 ad2antlr 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( card ` A ) = (/) ) -> (/) ~<_ B )
6 3 5 eqbrtrd 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( card ` A ) = (/) ) -> A ~<_ B )
7 6 a1d 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( card ` A ) = (/) ) -> ( ( card ` A ) C_ ( card ` B ) -> A ~<_ B ) )
8 fvex 
 |-  ( card ` B ) e. _V
9 simprr 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( card ` A ) C_ ( card ` B ) )
10 ssdomg 
 |-  ( ( card ` B ) e. _V -> ( ( card ` A ) C_ ( card ` B ) -> ( card ` A ) ~<_ ( card ` B ) ) )
11 8 9 10 mpsyl 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( card ` A ) ~<_ ( card ` B ) )
12 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
13 12 ad2antrr 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( card ` A ) ~~ A )
14 simprl 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( card ` A ) =/= (/) )
15 ssn0 
 |-  ( ( ( card ` A ) C_ ( card ` B ) /\ ( card ` A ) =/= (/) ) -> ( card ` B ) =/= (/) )
16 9 14 15 syl2anc 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( card ` B ) =/= (/) )
17 ndmfv 
 |-  ( -. B e. dom card -> ( card ` B ) = (/) )
18 17 necon1ai 
 |-  ( ( card ` B ) =/= (/) -> B e. dom card )
19 cardid2 
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
20 16 18 19 3syl 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( card ` B ) ~~ B )
21 domen1 
 |-  ( ( card ` A ) ~~ A -> ( ( card ` A ) ~<_ ( card ` B ) <-> A ~<_ ( card ` B ) ) )
22 domen2 
 |-  ( ( card ` B ) ~~ B -> ( A ~<_ ( card ` B ) <-> A ~<_ B ) )
23 21 22 sylan9bb 
 |-  ( ( ( card ` A ) ~~ A /\ ( card ` B ) ~~ B ) -> ( ( card ` A ) ~<_ ( card ` B ) <-> A ~<_ B ) )
24 13 20 23 syl2anc 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> ( ( card ` A ) ~<_ ( card ` B ) <-> A ~<_ B ) )
25 11 24 mpbid 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( ( card ` A ) =/= (/) /\ ( card ` A ) C_ ( card ` B ) ) ) -> A ~<_ B )
26 25 expr 
 |-  ( ( ( A e. dom card /\ B e. V ) /\ ( card ` A ) =/= (/) ) -> ( ( card ` A ) C_ ( card ` B ) -> A ~<_ B ) )
27 7 26 pm2.61dane 
 |-  ( ( A e. dom card /\ B e. V ) -> ( ( card ` A ) C_ ( card ` B ) -> A ~<_ B ) )