Theorem elrncard

Description: Let us define a cardinal number to be an element A e. On such that A is not equipotent with any x e. A . (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	elrncard	$$⊢A\in \mathrm{ran}\mathrm{card}\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\in A\neg x\approx A\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscard4	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow A\in \mathrm{ran}\mathrm{card}$$
2		iscard5	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\in A\neg x\approx A\right)$$
3	1 2	bitr3i	$$⊢A\in \mathrm{ran}\mathrm{card}\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\in A\neg x\approx A\right)$$