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

Theorem carden2b 7859
 Description: If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 7858 are meant to replace carden 8431 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 7857 . . . . 5
2 ennum 7839 . . . . . . . 8
32biimpa 472 . . . . . . 7
4 cardid2 7845 . . . . . . 7
53, 4syl 16 . . . . . 6
6 ensym 7159 . . . . . . 7
76adantr 453 . . . . . 6
8 entr 7162 . . . . . 6
95, 7, 8syl2anc 644 . . . . 5
101, 9nsyl3 114 . . . 4
11 cardon 7836 . . . . 5
12 cardon 7836 . . . . 5
13 ontri1 4618 . . . . 5
1411, 12, 13mp2an 655 . . . 4
1510, 14sylibr 205 . . 3
16 cardne 7857 . . . . 5
17 cardid2 7845 . . . . . 6
18 id 21 . . . . . 6
19 entr 7162 . . . . . 6
2017, 18, 19syl2anr 466 . . . . 5
2116, 20nsyl3 114 . . . 4
22 ontri1 4618 . . . . 5
2312, 11, 22mp2an 655 . . . 4
2421, 23sylibr 205 . . 3
2515, 24eqssd 3367 . 2
26 ndmfv 5758 . . . 4