# Metamath Proof Explorer

## Theorem cardval2

Description: An alternate version of the value of the cardinal number of a set. Compare cardval . This theorem could be used to give a simpler definition of card in place of df-card . It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003)

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

### Proof

Step Hyp Ref Expression
1 cardsdomel ${⊢}\left({x}\in \mathrm{On}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \left({x}\prec {A}↔{x}\in \mathrm{card}\left({A}\right)\right)$
2 1 ancoms ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {x}\in \mathrm{On}\right)\to \left({x}\prec {A}↔{x}\in \mathrm{card}\left({A}\right)\right)$
3 2 pm5.32da ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left(\left({x}\in \mathrm{On}\wedge {x}\prec {A}\right)↔\left({x}\in \mathrm{On}\wedge {x}\in \mathrm{card}\left({A}\right)\right)\right)$
4 cardon ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{On}$
5 4 oneli ${⊢}{x}\in \mathrm{card}\left({A}\right)\to {x}\in \mathrm{On}$
6 5 pm4.71ri ${⊢}{x}\in \mathrm{card}\left({A}\right)↔\left({x}\in \mathrm{On}\wedge {x}\in \mathrm{card}\left({A}\right)\right)$
7 3 6 syl6rbbr ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left({x}\in \mathrm{card}\left({A}\right)↔\left({x}\in \mathrm{On}\wedge {x}\prec {A}\right)\right)$
8 7 abbi2dv ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\left\{{x}|\left({x}\in \mathrm{On}\wedge {x}\prec {A}\right)\right\}$
9 df-rab ${⊢}\left\{{x}\in \mathrm{On}|{x}\prec {A}\right\}=\left\{{x}|\left({x}\in \mathrm{On}\wedge {x}\prec {A}\right)\right\}$
10 8 9 eqtr4di ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)=\left\{{x}\in \mathrm{On}|{x}\prec {A}\right\}$