# Metamath Proof Explorer

## Theorem cardval3

Description: An alternate definition of the value of ( cardA ) that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion cardval3 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to {A}\in \mathrm{V}$
2 isnum2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{x}\approx {A}$
3 rabn0 ${⊢}\left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}\ne \varnothing ↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{x}\approx {A}$
4 intex ${⊢}\left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}\ne \varnothing ↔\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}\in \mathrm{V}$
5 2 3 4 3bitr2i ${⊢}{A}\in \mathrm{dom}\mathrm{card}↔\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}\in \mathrm{V}$
6 5 biimpi ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}\in \mathrm{V}$
7 breq2 ${⊢}{y}={A}\to \left({x}\approx {y}↔{x}\approx {A}\right)$
8 7 rabbidv ${⊢}{y}={A}\to \left\{{x}\in \mathrm{On}|{x}\approx {y}\right\}=\left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}$
9 8 inteqd ${⊢}{y}={A}\to \bigcap \left\{{x}\in \mathrm{On}|{x}\approx {y}\right\}=\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}$
10 df-card ${⊢}\mathrm{card}=\left({y}\in \mathrm{V}⟼\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {y}\right\}\right)$
11 9 10 fvmptg ${⊢}\left({A}\in \mathrm{V}\wedge \bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}\in \mathrm{V}\right)\to \mathrm{card}\left({A}\right)=\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}$
12 1 6 11 syl2anc ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\bigcap \left\{{x}\in \mathrm{On}|{x}\approx {A}\right\}$