Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  carden2b Structured version   Visualization version   Unicode version

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

Proof of Theorem carden2b
StepHypRef Expression
1 cardne 8417 . . . . 5
2 ennum 8399 . . . . . . . 8
32biimpa 492 . . . . . . 7
4 cardid2 8405 . . . . . . 7
53, 4syl 17 . . . . . 6
6 ensym 7636 . . . . . . 7
76adantr 472 . . . . . 6
8 entr 7639 . . . . . 6
95, 7, 8syl2anc 673 . . . . 5
101, 9nsyl3 123 . . . 4
11 cardon 8396 . . . . 5
12 cardon 8396 . . . . 5
13 ontri1 5464 . . . . 5
1411, 12, 13mp2an 686 . . . 4
1510, 14sylibr 217 . . 3
16 cardne 8417 . . . . 5
17 cardid2 8405 . . . . . 6
18 id 22 . . . . . 6
19 entr 7639 . . . . . 6
2017, 18, 19syl2anr 486 . . . . 5
2116, 20nsyl3 123 . . . 4
22 ontri1 5464 . . . . 5
2312, 11, 22mp2an 686 . . . 4
2421, 23sylibr 217 . . 3
2515, 24eqssd 3435 . 2
26 ndmfv 5903 . . . 4