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 ) )