Theorem iscard5

Description: Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023)

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

Proof

Step	Hyp	Ref	Expression
1		iscard	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\in Ax\prec A\right)$$
2		sdomnen	$$⊢x\prec A\to \neg x\approx A$$
3		onelss	$$⊢A\in \mathrm{On}\to \left(x\in A\to x\subseteq A\right)$$
4		ssdomg	$$⊢A\in \mathrm{On}\to \left(x\subseteq A\to x\preccurlyeq A\right)$$
5	3 4	syld	$$⊢A\in \mathrm{On}\to \left(x\in A\to x\preccurlyeq A\right)$$
6	5	imp	$$⊢\left(A\in \mathrm{On}\wedge x\in A\right)\to x\preccurlyeq A$$
7		brsdom	$$⊢x\prec A\leftrightarrow \left(x\preccurlyeq A\wedge \neg x\approx A\right)$$
8	7	biimpri	$$⊢\left(x\preccurlyeq A\wedge \neg x\approx A\right)\to x\prec A$$
9	8	a1i	$$⊢\left(A\in \mathrm{On}\wedge x\in A\right)\to \left(\left(x\preccurlyeq A\wedge \neg x\approx A\right)\to x\prec A\right)$$
10	6 9	mpand	$$⊢\left(A\in \mathrm{On}\wedge x\in A\right)\to \left(\neg x\approx A\to x\prec A\right)$$
11	2 10	impbid2	$$⊢\left(A\in \mathrm{On}\wedge x\in A\right)\to \left(x\prec A\leftrightarrow \neg x\approx A\right)$$
12	11	ralbidva	$$⊢A\in \mathrm{On}\to \left(\forall x\in Ax\prec A\leftrightarrow \forall x\in A\neg x\approx A\right)$$
13	12	pm5.32i	$$⊢\left(A\in \mathrm{On}\wedge \forall x\in Ax\prec A\right)\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\in A\neg x\approx A\right)$$
14	1 13	bitri	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\in A\neg x\approx A\right)$$