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		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
2	1	oneli	$$⊢x\in \mathrm{card}\left(A\right)\to x\in \mathrm{On}$$
3	2	pm4.71ri	$$⊢x\in \mathrm{card}\left(A\right)\leftrightarrow \left(x\in \mathrm{On}\wedge x\in \mathrm{card}\left(A\right)\right)$$
4		cardsdomel	$$⊢\left(x\in \mathrm{On}\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \left(x\prec A\leftrightarrow x\in \mathrm{card}\left(A\right)\right)$$
5	4	ancoms	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge x\in \mathrm{On}\right)\to \left(x\prec A\leftrightarrow x\in \mathrm{card}\left(A\right)\right)$$
6	5	pm5.32da	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\left(x\in \mathrm{On}\wedge x\prec A\right)\leftrightarrow \left(x\in \mathrm{On}\wedge x\in \mathrm{card}\left(A\right)\right)\right)$$
7	3 6	bitr4id	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(x\in \mathrm{card}\left(A\right)\leftrightarrow \left(x\in \mathrm{On}\wedge x\prec A\right)\right)$$
8	7	eqabdv	$$⊢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\}$$