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

### Proof

Step Hyp Ref Expression
1 df-ne ${⊢}\mathrm{card}\left({A}\right)\ne \varnothing ↔¬\mathrm{card}\left({A}\right)=\varnothing$
2 ndmfv ${⊢}¬{B}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({B}\right)=\varnothing$
3 eqeq1 ${⊢}\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left(\mathrm{card}\left({A}\right)=\varnothing ↔\mathrm{card}\left({B}\right)=\varnothing \right)$
4 2 3 syl5ibr ${⊢}\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left(¬{B}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\varnothing \right)$
5 4 con1d ${⊢}\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left(¬\mathrm{card}\left({A}\right)=\varnothing \to {B}\in \mathrm{dom}\mathrm{card}\right)$
6 5 imp ${⊢}\left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\wedge ¬\mathrm{card}\left({A}\right)=\varnothing \right)\to {B}\in \mathrm{dom}\mathrm{card}$
7 cardid2 ${⊢}{B}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({B}\right)\approx {B}$
8 6 7 syl ${⊢}\left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\wedge ¬\mathrm{card}\left({A}\right)=\varnothing \right)\to \mathrm{card}\left({B}\right)\approx {B}$
9 breq2 ${⊢}\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left({A}\approx \mathrm{card}\left({A}\right)↔{A}\approx \mathrm{card}\left({B}\right)\right)$
10 entr ${⊢}\left({A}\approx \mathrm{card}\left({B}\right)\wedge \mathrm{card}\left({B}\right)\approx {B}\right)\to {A}\approx {B}$
11 10 ex ${⊢}{A}\approx \mathrm{card}\left({B}\right)\to \left(\mathrm{card}\left({B}\right)\approx {B}\to {A}\approx {B}\right)$
12 9 11 syl6bi ${⊢}\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left({A}\approx \mathrm{card}\left({A}\right)\to \left(\mathrm{card}\left({B}\right)\approx {B}\to {A}\approx {B}\right)\right)$
13 cardid2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\approx {A}$
14 ndmfv ${⊢}¬{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\varnothing$
15 13 14 nsyl4 ${⊢}¬\mathrm{card}\left({A}\right)=\varnothing \to \mathrm{card}\left({A}\right)\approx {A}$
16 15 ensymd ${⊢}¬\mathrm{card}\left({A}\right)=\varnothing \to {A}\approx \mathrm{card}\left({A}\right)$
17 12 16 impel ${⊢}\left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\wedge ¬\mathrm{card}\left({A}\right)=\varnothing \right)\to \left(\mathrm{card}\left({B}\right)\approx {B}\to {A}\approx {B}\right)$
18 8 17 mpd ${⊢}\left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\wedge ¬\mathrm{card}\left({A}\right)=\varnothing \right)\to {A}\approx {B}$
19 1 18 sylan2b ${⊢}\left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\wedge \mathrm{card}\left({A}\right)\ne \varnothing \right)\to {A}\approx {B}$