Theorem iscard4

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

	Ref	Expression
Assertion	iscard4	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow A\in \mathrm{ran}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow A=\mathrm{card}\left(A\right)$$
2		mptrel	$$⊢\mathrm{Rel}\left(x\in \mathrm{V}⟼\bigcap \left\{y\in \mathrm{On}|y\approx x\right\}\right)$$
3		df-card	$$⊢\mathrm{card}=\left(x\in \mathrm{V}⟼\bigcap \left\{y\in \mathrm{On}|y\approx x\right\}\right)$$
4	3	releqi	$$⊢\mathrm{Rel}\mathrm{card}\leftrightarrow \mathrm{Rel}\left(x\in \mathrm{V}⟼\bigcap \left\{y\in \mathrm{On}|y\approx x\right\}\right)$$
5	2 4	mpbir	$$⊢\mathrm{Rel}\mathrm{card}$$
6		relelrnb	$$⊢\mathrm{Rel}\mathrm{card}\to \left(A\in \mathrm{ran}\mathrm{card}\leftrightarrow \exists xx\mathrm{card}A\right)$$
7	5 6	ax-mp	$$⊢A\in \mathrm{ran}\mathrm{card}\leftrightarrow \exists xx\mathrm{card}A$$
8	3	funmpt2	$$⊢\mathrm{Fun}\mathrm{card}$$
9		funbrfv	$$⊢\mathrm{Fun}\mathrm{card}\to \left(x\mathrm{card}A\to \mathrm{card}\left(x\right)=A\right)$$
10	8 9	ax-mp	$$⊢x\mathrm{card}A\to \mathrm{card}\left(x\right)=A$$
11	10	eqcomd	$$⊢x\mathrm{card}A\to A=\mathrm{card}\left(x\right)$$
12	11	eximi	$$⊢\exists xx\mathrm{card}A\to \exists xA=\mathrm{card}\left(x\right)$$
13		cardidm	$$⊢\mathrm{card}\left(\mathrm{card}\left(x\right)\right)=\mathrm{card}\left(x\right)$$
14		fveq2	$$⊢A=\mathrm{card}\left(x\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\mathrm{card}\left(x\right)\right)$$
15		id	$$⊢A=\mathrm{card}\left(x\right)\to A=\mathrm{card}\left(x\right)$$
16	13 14 15	3eqtr4a	$$⊢A=\mathrm{card}\left(x\right)\to \mathrm{card}\left(A\right)=A$$
17	16	exlimiv	$$⊢\exists xA=\mathrm{card}\left(x\right)\to \mathrm{card}\left(A\right)=A$$
18	1	biimpi	$$⊢\mathrm{card}\left(A\right)=A\to A=\mathrm{card}\left(A\right)$$
19		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
20	18 19	eqeltrdi	$$⊢\mathrm{card}\left(A\right)=A\to A\in \mathrm{On}$$
21		onenon	$$⊢A\in \mathrm{On}\to A\in \mathrm{dom}\mathrm{card}$$
22	20 21	syl	$$⊢\mathrm{card}\left(A\right)=A\to A\in \mathrm{dom}\mathrm{card}$$
23		funfvbrb	$$⊢\mathrm{Fun}\mathrm{card}\to \left(A\in \mathrm{dom}\mathrm{card}\leftrightarrow A\mathrm{card}\mathrm{card}\left(A\right)\right)$$
24	23	biimpd	$$⊢\mathrm{Fun}\mathrm{card}\to \left(A\in \mathrm{dom}\mathrm{card}\to A\mathrm{card}\mathrm{card}\left(A\right)\right)$$
25	8 22 24	mpsyl	$$⊢\mathrm{card}\left(A\right)=A\to A\mathrm{card}\mathrm{card}\left(A\right)$$
26		id	$$⊢\mathrm{card}\left(A\right)=A\to \mathrm{card}\left(A\right)=A$$
27	25 26	breqtrd	$$⊢\mathrm{card}\left(A\right)=A\to A\mathrm{card}A$$
28		id	$$⊢A=\mathrm{card}\left(A\right)\to A=\mathrm{card}\left(A\right)$$
29	28 19	eqeltrdi	$$⊢A=\mathrm{card}\left(A\right)\to A\in \mathrm{On}$$
30	29	eqcoms	$$⊢\mathrm{card}\left(A\right)=A\to A\in \mathrm{On}$$
31		sbcbr1g	$$⊢A\in \mathrm{On}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\mathrm{card}A\leftrightarrow ⦋A/x⦌x\mathrm{card}A\right)$$
32		csbvarg	$$⊢A\in \mathrm{On}\to ⦋A/x⦌x=A$$
33	32	breq1d	$$⊢A\in \mathrm{On}\to \left(⦋A/x⦌x\mathrm{card}A\leftrightarrow A\mathrm{card}A\right)$$
34	31 33	bitrd	$$⊢A\in \mathrm{On}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\mathrm{card}A\leftrightarrow A\mathrm{card}A\right)$$
35	30 34	syl	$$⊢\mathrm{card}\left(A\right)=A\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\mathrm{card}A\leftrightarrow A\mathrm{card}A\right)$$
36	27 35	mpbird	$$⊢\mathrm{card}\left(A\right)=A\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\mathrm{card}A$$
37	36	spesbcd	$$⊢\mathrm{card}\left(A\right)=A\to \exists xx\mathrm{card}A$$
38	17 37	syl	$$⊢\exists xA=\mathrm{card}\left(x\right)\to \exists xx\mathrm{card}A$$
39	12 38	impbii	$$⊢\exists xx\mathrm{card}A\leftrightarrow \exists xA=\mathrm{card}\left(x\right)$$
40		oncard	$$⊢\exists xA=\mathrm{card}\left(x\right)\leftrightarrow A=\mathrm{card}\left(A\right)$$
41	7 39 40	3bitrri	$$⊢A=\mathrm{card}\left(A\right)\leftrightarrow A\in \mathrm{ran}\mathrm{card}$$
42	1 41	bitri	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow A\in \mathrm{ran}\mathrm{card}$$