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 dom card card B =
3 eqeq1 card A = card B card A = card B =
4 2 3 syl5ibr card A = card B ¬ B dom card card A =
5 4 con1d card A = card B ¬ card A = B dom card
6 5 imp card A = card B ¬ card A = B dom card
7 cardid2 B 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 dom card card A A
14 ndmfv ¬ A 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