Metamath Proof Explorer

Theorem carden2b

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

Ref Expression
Assertion carden2b ⊢A≈B→card⁡A=card⁡B

Proof

Step Hyp Ref Expression
1 cardne ⊢card⁡B∈card⁡A→¬card⁡B≈A
2 ennum ⊢A≈B→A∈dom⁡card↔B∈dom⁡card
3 2 biimpa ⊢A≈B∧A∈dom⁡card→B∈dom⁡card
4 cardid2 ⊢B∈dom⁡card→card⁡B≈B
5 3 4 syl ⊢A≈B∧A∈dom⁡card→card⁡B≈B
6 ensym ⊢A≈B→B≈A
7 6 adantr ⊢A≈B∧A∈dom⁡card→B≈A
8 entr ⊢card⁡B≈B∧B≈A→card⁡B≈A
9 5 7 8 syl2anc ⊢A≈B∧A∈dom⁡card→card⁡B≈A
10 1 9 nsyl3 ⊢A≈B∧A∈dom⁡card→¬card⁡B∈card⁡A
11 cardon ⊢card⁡A∈On
12 cardon ⊢card⁡B∈On
13 ontri1 ⊢card⁡A∈On∧card⁡B∈On→card⁡A⊆card⁡B↔¬card⁡B∈card⁡A
14 11 12 13 mp2an ⊢card⁡A⊆card⁡B↔¬card⁡B∈card⁡A
15 10 14 sylibr ⊢A≈B∧A∈dom⁡card→card⁡A⊆card⁡B
16 cardne ⊢card⁡A∈card⁡B→¬card⁡A≈B
17 cardid2 ⊢A∈dom⁡card→card⁡A≈A
18 id ⊢A≈B→A≈B
19 entr ⊢card⁡A≈A∧A≈B→card⁡A≈B
20 17 18 19 syl2anr ⊢A≈B∧A∈dom⁡card→card⁡A≈B
21 16 20 nsyl3 ⊢A≈B∧A∈dom⁡card→¬card⁡A∈card⁡B
22 ontri1 ⊢card⁡B∈On∧card⁡A∈On→card⁡B⊆card⁡A↔¬card⁡A∈card⁡B
23 12 11 22 mp2an ⊢card⁡B⊆card⁡A↔¬card⁡A∈card⁡B
24 21 23 sylibr ⊢A≈B∧A∈dom⁡card→card⁡B⊆card⁡A
25 15 24 eqssd ⊢A≈B∧A∈dom⁡card→card⁡A=card⁡B
26 ndmfv ⊢¬A∈dom⁡card→card⁡A=∅
27 26 adantl ⊢A≈B∧¬A∈dom⁡card→card⁡A=∅
28 2 notbid ⊢A≈B→¬A∈dom⁡card↔¬B∈dom⁡card
29 28 biimpa ⊢A≈B∧¬A∈dom⁡card→¬B∈dom⁡card
30 ndmfv ⊢¬B∈dom⁡card→card⁡B=∅
31 29 30 syl ⊢A≈B∧¬A∈dom⁡card→card⁡B=∅
32 27 31 eqtr4d ⊢A≈B∧¬A∈dom⁡card→card⁡A=card⁡B
33 25 32 pm2.61dan ⊢A≈B→card⁡A=card⁡B