Theorem elnn

Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998)

	Ref	Expression
Assertion	elnn	$$⊢\left(A\in B\wedge B\in \mathrm{\omega }\right)\to A\in \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
2		ordtr	$$⊢\mathrm{Ord}\mathrm{\omega }\to \mathrm{Tr}\mathrm{\omega }$$
3		trel	$$⊢\mathrm{Tr}\mathrm{\omega }\to \left(\left(A\in B\wedge B\in \mathrm{\omega }\right)\to A\in \mathrm{\omega }\right)$$
4	1 2 3	mp2b	$$⊢\left(A\in B\wedge B\in \mathrm{\omega }\right)\to A\in \mathrm{\omega }$$