# Metamath Proof Explorer

## Theorem cardid2

Description: Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

Ref Expression
Assertion cardid2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\approx {A}$

### Proof

Step Hyp Ref Expression
1 cardval3 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}$
2 ssrab2 ${⊢}\left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\subseteq \mathrm{On}$
3 fvex ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{V}$
4 1 3 eqeltrrdi ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \bigcap \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\in \mathrm{V}$
5 intex ${⊢}\left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\ne \varnothing ↔\bigcap \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\in \mathrm{V}$
6 4 5 sylibr ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\ne \varnothing$
7 onint ${⊢}\left(\left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\subseteq \mathrm{On}\wedge \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\ne \varnothing \right)\to \bigcap \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\in \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}$
8 2 6 7 sylancr ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \bigcap \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\in \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}$
9 1 8 eqeltrd ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\in \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}$
10 breq1 ${⊢}{y}=\mathrm{card}\left({A}\right)\to \left({y}\approx {A}↔\mathrm{card}\left({A}\right)\approx {A}\right)$
11 10 elrab ${⊢}\mathrm{card}\left({A}\right)\in \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}↔\left(\mathrm{card}\left({A}\right)\in \mathrm{On}\wedge \mathrm{card}\left({A}\right)\approx {A}\right)$
12 11 simprbi ${⊢}\mathrm{card}\left({A}\right)\in \left\{{y}\in \mathrm{On}|{y}\approx {A}\right\}\to \mathrm{card}\left({A}\right)\approx {A}$
13 9 12 syl ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\approx {A}$