Theorem carden2a

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

	Ref	Expression
Assertion	carden2a	|- ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> A ~~ B )

Proof

Step	Hyp	Ref	Expression
1		df-ne	|- ( ( card ` A ) =/= (/) <-> -. ( card ` A ) = (/) )
2		ndmfv	|- ( -. B e. dom card -> ( card ` B ) = (/) )
3		eqeq1	|- ( ( card ` A ) = ( card ` B ) -> ( ( card ` A ) = (/) <-> ( card ` B ) = (/) ) )
4	2 3	syl5ibr	|- ( ( card ` A ) = ( card ` B ) -> ( -. B e. dom card -> ( card ` A ) = (/) ) )
5	4	con1d	|- ( ( card ` A ) = ( card ` B ) -> ( -. ( card ` A ) = (/) -> B e. dom card ) )
6	5	imp	|- ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> B e. dom card )
7		cardid2	|- ( B e. dom card -> ( card ` B ) ~~ B )
8	6 7	syl	|- ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> ( card ` B ) ~~ B )
9		breq2	|- ( ( card ` A ) = ( card ` B ) -> ( A ~~ ( card ` A ) <-> A ~~ ( card ` B ) ) )
10		entr	|- ( ( A ~~ ( card ` B ) /\ ( card ` B ) ~~ B ) -> A ~~ B )
11	10	ex	|- ( A ~~ ( card ` B ) -> ( ( card ` B ) ~~ B -> A ~~ B ) )
12	9 11	syl6bi	|- ( ( card ` A ) = ( card ` B ) -> ( A ~~ ( card ` A ) -> ( ( card ` B ) ~~ B -> A ~~ B ) ) )
13		cardid2	|- ( A e. dom card -> ( card ` A ) ~~ A )
14		ndmfv	|- ( -. A e. dom card -> ( card ` A ) = (/) )
15	13 14	nsyl4	|- ( -. ( card ` A ) = (/) -> ( card ` A ) ~~ A )
16	15	ensymd	|- ( -. ( card ` A ) = (/) -> A ~~ ( card ` A ) )
17	12 16	impel	|- ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> ( ( card ` B ) ~~ B -> A ~~ B ) )
18	8 17	mpd	|- ( ( ( card ` A ) = ( card ` B ) /\ -. ( card ` A ) = (/) ) -> A ~~ B )
19	1 18	sylan2b	|- ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> A ~~ B )