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

Metamath Proof Explorer

Theorem carden2b

Description: If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a are meant to replace carden in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion carden2b 
|- ( A ~~ B -> ( card ` A ) = ( card ` B ) )

Proof

Step Hyp Ref Expression
1 cardne 
 |-  ( ( card ` B ) e. ( card ` A ) -> -. ( card ` B ) ~~ A )
2 ennum 
 |-  ( A ~~ B -> ( A e. dom card <-> B e. dom card ) )
3 2 biimpa 
 |-  ( ( A ~~ B /\ A e. dom card ) -> B e. dom card )
4 cardid2 
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
5 3 4 syl 
 |-  ( ( A ~~ B /\ A e. dom card ) -> ( card ` B ) ~~ B )
6 ensym 
 |-  ( A ~~ B -> B ~~ A )
7 6 adantr 
 |-  ( ( A ~~ B /\ A e. dom card ) -> B ~~ A )
8 entr 
 |-  ( ( ( card ` B ) ~~ B /\ B ~~ A ) -> ( card ` B ) ~~ A )
9 5 7 8 syl2anc 
 |-  ( ( A ~~ B /\ A e. dom card ) -> ( card ` B ) ~~ A )
10 1 9 nsyl3 
 |-  ( ( A ~~ B /\ A e. dom card ) -> -. ( card ` B ) e. ( card ` A ) )
11 cardon 
 |-  ( card ` A ) e. On
12 cardon 
 |-  ( card ` B ) e. On
13 ontri1 
 |-  ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) )
14 11 12 13 mp2an 
 |-  ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) )
15 10 14 sylibr 
 |-  ( ( A ~~ B /\ A e. dom card ) -> ( card ` A ) C_ ( card ` B ) )
16 cardne 
 |-  ( ( card ` A ) e. ( card ` B ) -> -. ( card ` A ) ~~ B )
17 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
18 id 
 |-  ( A ~~ B -> A ~~ B )
19 entr 
 |-  ( ( ( card ` A ) ~~ A /\ A ~~ B ) -> ( card ` A ) ~~ B )
20 17 18 19 syl2anr 
 |-  ( ( A ~~ B /\ A e. dom card ) -> ( card ` A ) ~~ B )
21 16 20 nsyl3 
 |-  ( ( A ~~ B /\ A e. dom card ) -> -. ( card ` A ) e. ( card ` B ) )
22 ontri1 
 |-  ( ( ( card ` B ) e. On /\ ( card ` A ) e. On ) -> ( ( card ` B ) C_ ( card ` A ) <-> -. ( card ` A ) e. ( card ` B ) ) )
23 12 11 22 mp2an 
 |-  ( ( card ` B ) C_ ( card ` A ) <-> -. ( card ` A ) e. ( card ` B ) )
24 21 23 sylibr 
 |-  ( ( A ~~ B /\ A e. dom card ) -> ( card ` B ) C_ ( card ` A ) )
25 15 24 eqssd 
 |-  ( ( A ~~ B /\ A e. dom card ) -> ( card ` A ) = ( card ` B ) )
26 ndmfv 
 |-  ( -. A e. dom card -> ( card ` A ) = (/) )
27 26 adantl 
 |-  ( ( A ~~ B /\ -. A e. dom card ) -> ( card ` A ) = (/) )
28 2 notbid 
 |-  ( A ~~ B -> ( -. A e. dom card <-> -. B e. dom card ) )
29 28 biimpa 
 |-  ( ( A ~~ B /\ -. A e. dom card ) -> -. B e. dom card )
30 ndmfv 
 |-  ( -. B e. dom card -> ( card ` B ) = (/) )
31 29 30 syl 
 |-  ( ( A ~~ B /\ -. A e. dom card ) -> ( card ` B ) = (/) )
32 27 31 eqtr4d 
 |-  ( ( A ~~ B /\ -. A e. dom card ) -> ( card ` A ) = ( card ` B ) )
33 25 32 pm2.61dan 
 |-  ( A ~~ B -> ( card ` A ) = ( card ` B ) )