Theorem nndomo

Description: Cardinal ordering agrees with natural number ordering. Example 3 of Enderton p. 146. (Contributed by NM, 17-Jun-1998)

	Ref	Expression
Assertion	nndomo	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A\preccurlyeq B\leftrightarrow A\subseteq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnon	$$⊢B\in \mathrm{\omega }\to B\in \mathrm{On}$$
2		nndomog	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{On}\right)\to \left(A\preccurlyeq B\leftrightarrow A\subseteq B\right)$$
3	1 2	sylan2	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A\preccurlyeq B\leftrightarrow A\subseteq B\right)$$