Theorem iscard3

Description: Two ways to express the property of being a cardinal number. (Contributed by NM, 9-Nov-2003)

	Ref	Expression
Assertion	iscard3	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow A\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)$$

Proof

Step	Hyp	Ref	Expression
1		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
2		eleq1	$$⊢\mathrm{card}\left(A\right)=A\to \left(\mathrm{card}\left(A\right)\in \mathrm{On}\leftrightarrow A\in \mathrm{On}\right)$$
3	1 2	mpbii	$$⊢\mathrm{card}\left(A\right)=A\to A\in \mathrm{On}$$
4		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
5	3 4	syl	$$⊢\mathrm{card}\left(A\right)=A\to \mathrm{Ord}A$$
6		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
7		ordtri2or	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}\mathrm{\omega }\right)\to \left(A\in \mathrm{\omega }\vee \mathrm{\omega }\subseteq A\right)$$
8	5 6 7	sylancl	$$⊢\mathrm{card}\left(A\right)=A\to \left(A\in \mathrm{\omega }\vee \mathrm{\omega }\subseteq A\right)$$
9	8	ord	$$⊢\mathrm{card}\left(A\right)=A\to \left(\neg A\in \mathrm{\omega }\to \mathrm{\omega }\subseteq A\right)$$
10		isinfcard	$$⊢\left(\mathrm{\omega }\subseteq A\wedge \mathrm{card}\left(A\right)=A\right)\leftrightarrow A\in \mathrm{ran}\aleph$$
11	10	biimpi	$$⊢\left(\mathrm{\omega }\subseteq A\wedge \mathrm{card}\left(A\right)=A\right)\to A\in \mathrm{ran}\aleph$$
12	11	expcom	$$⊢\mathrm{card}\left(A\right)=A\to \left(\mathrm{\omega }\subseteq A\to A\in \mathrm{ran}\aleph \right)$$
13	9 12	syld	$$⊢\mathrm{card}\left(A\right)=A\to \left(\neg A\in \mathrm{\omega }\to A\in \mathrm{ran}\aleph \right)$$
14	13	orrd	$$⊢\mathrm{card}\left(A\right)=A\to \left(A\in \mathrm{\omega }\vee A\in \mathrm{ran}\aleph \right)$$
15		cardnn	$$⊢A\in \mathrm{\omega }\to \mathrm{card}\left(A\right)=A$$
16	10	bicomi	$$⊢A\in \mathrm{ran}\aleph \leftrightarrow \left(\mathrm{\omega }\subseteq A\wedge \mathrm{card}\left(A\right)=A\right)$$
17	16	simprbi	$$⊢A\in \mathrm{ran}\aleph \to \mathrm{card}\left(A\right)=A$$
18	15 17	jaoi	$$⊢\left(A\in \mathrm{\omega }\vee A\in \mathrm{ran}\aleph \right)\to \mathrm{card}\left(A\right)=A$$
19	14 18	impbii	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow \left(A\in \mathrm{\omega }\vee A\in \mathrm{ran}\aleph \right)$$
20		elun	$$⊢A\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)\leftrightarrow \left(A\in \mathrm{\omega }\vee A\in \mathrm{ran}\aleph \right)$$
21	19 20	bitr4i	$$⊢\mathrm{card}\left(A\right)=A\leftrightarrow A\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)$$