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

Metamath Proof Explorer

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	imbitrrid	\|- ( ( 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	biimtrdi	\|- ( ( 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 )