Theorem oncard

Description: A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	oncard	$$⊢\exists xA=\mathrm{card}\left(x\right)\leftrightarrow A=\mathrm{card}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A=\mathrm{card}\left(x\right)\to A=\mathrm{card}\left(x\right)$$
2		fveq2	$$⊢A=\mathrm{card}\left(x\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\mathrm{card}\left(x\right)\right)$$
3		cardidm	$$⊢\mathrm{card}\left(\mathrm{card}\left(x\right)\right)=\mathrm{card}\left(x\right)$$
4	2 3	eqtrdi	$$⊢A=\mathrm{card}\left(x\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(x\right)$$
5	1 4	eqtr4d	$$⊢A=\mathrm{card}\left(x\right)\to A=\mathrm{card}\left(A\right)$$
6	5	exlimiv	$$⊢\exists xA=\mathrm{card}\left(x\right)\to A=\mathrm{card}\left(A\right)$$
7		fvex	$$⊢\mathrm{card}\left(A\right)\in \mathrm{V}$$
8		eleq1	$$⊢A=\mathrm{card}\left(A\right)\to \left(A\in \mathrm{V}\leftrightarrow \mathrm{card}\left(A\right)\in \mathrm{V}\right)$$
9	7 8	mpbiri	$$⊢A=\mathrm{card}\left(A\right)\to A\in \mathrm{V}$$
10		fveq2	$$⊢x=A\to \mathrm{card}\left(x\right)=\mathrm{card}\left(A\right)$$
11	10	eqeq2d	$$⊢x=A\to \left(A=\mathrm{card}\left(x\right)\leftrightarrow A=\mathrm{card}\left(A\right)\right)$$
12	11	spcegv	$$⊢A\in \mathrm{V}\to \left(A=\mathrm{card}\left(A\right)\to \exists xA=\mathrm{card}\left(x\right)\right)$$
13	9 12	mpcom	$$⊢A=\mathrm{card}\left(A\right)\to \exists xA=\mathrm{card}\left(x\right)$$
14	6 13	impbii	$$⊢\exists xA=\mathrm{card}\left(x\right)\leftrightarrow A=\mathrm{card}\left(A\right)$$