# 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}\approx {B}\to \mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 cardne ${⊢}\mathrm{card}\left({B}\right)\in \mathrm{card}\left({A}\right)\to ¬\mathrm{card}\left({B}\right)\approx {A}$
2 ennum ${⊢}{A}\approx {B}\to \left({A}\in \mathrm{dom}\mathrm{card}↔{B}\in \mathrm{dom}\mathrm{card}\right)$
3 2 biimpa ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to {B}\in \mathrm{dom}\mathrm{card}$
4 cardid2 ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({B}\right)\approx {B}$
5 3 4 syl ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({B}\right)\approx {B}$
6 ensym ${⊢}{A}\approx {B}\to {B}\approx {A}$
7 6 adantr ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to {B}\approx {A}$
8 entr ${⊢}\left(\mathrm{card}\left({B}\right)\approx {B}\wedge {B}\approx {A}\right)\to \mathrm{card}\left({B}\right)\approx {A}$
9 5 7 8 syl2anc ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({B}\right)\approx {A}$
10 1 9 nsyl3 ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to ¬\mathrm{card}\left({B}\right)\in \mathrm{card}\left({A}\right)$
11 cardon ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{On}$
12 cardon ${⊢}\mathrm{card}\left({B}\right)\in \mathrm{On}$
13 ontri1 ${⊢}\left(\mathrm{card}\left({A}\right)\in \mathrm{On}\wedge \mathrm{card}\left({B}\right)\in \mathrm{On}\right)\to \left(\mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left({B}\right)↔¬\mathrm{card}\left({B}\right)\in \mathrm{card}\left({A}\right)\right)$
14 11 12 13 mp2an ${⊢}\mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left({B}\right)↔¬\mathrm{card}\left({B}\right)\in \mathrm{card}\left({A}\right)$
15 10 14 sylibr ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left({B}\right)$
16 cardne ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{card}\left({B}\right)\to ¬\mathrm{card}\left({A}\right)\approx {B}$
17 cardid2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\approx {A}$
18 id ${⊢}{A}\approx {B}\to {A}\approx {B}$
19 entr ${⊢}\left(\mathrm{card}\left({A}\right)\approx {A}\wedge {A}\approx {B}\right)\to \mathrm{card}\left({A}\right)\approx {B}$
20 17 18 19 syl2anr ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({A}\right)\approx {B}$
21 16 20 nsyl3 ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to ¬\mathrm{card}\left({A}\right)\in \mathrm{card}\left({B}\right)$
22 ontri1 ${⊢}\left(\mathrm{card}\left({B}\right)\in \mathrm{On}\wedge \mathrm{card}\left({A}\right)\in \mathrm{On}\right)\to \left(\mathrm{card}\left({B}\right)\subseteq \mathrm{card}\left({A}\right)↔¬\mathrm{card}\left({A}\right)\in \mathrm{card}\left({B}\right)\right)$
23 12 11 22 mp2an ${⊢}\mathrm{card}\left({B}\right)\subseteq \mathrm{card}\left({A}\right)↔¬\mathrm{card}\left({A}\right)\in \mathrm{card}\left({B}\right)$
24 21 23 sylibr ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({B}\right)\subseteq \mathrm{card}\left({A}\right)$
25 15 24 eqssd ${⊢}\left({A}\approx {B}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)$
26 ndmfv ${⊢}¬{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\varnothing$
27 26 adantl ${⊢}\left({A}\approx {B}\wedge ¬{A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({A}\right)=\varnothing$
28 2 notbid ${⊢}{A}\approx {B}\to \left(¬{A}\in \mathrm{dom}\mathrm{card}↔¬{B}\in \mathrm{dom}\mathrm{card}\right)$
29 28 biimpa ${⊢}\left({A}\approx {B}\wedge ¬{A}\in \mathrm{dom}\mathrm{card}\right)\to ¬{B}\in \mathrm{dom}\mathrm{card}$
30 ndmfv ${⊢}¬{B}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({B}\right)=\varnothing$
31 29 30 syl ${⊢}\left({A}\approx {B}\wedge ¬{A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({B}\right)=\varnothing$
32 27 31 eqtr4d ${⊢}\left({A}\approx {B}\wedge ¬{A}\in \mathrm{dom}\mathrm{card}\right)\to \mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)$
33 25 32 pm2.61dan ${⊢}{A}\approx {B}\to \mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)$