Theorem onelon

Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of BellMachover p. 469. (Contributed by NM, 26-Oct-2003)

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

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ordelon	$$⊢\left(\mathrm{Ord}A\wedge B\in A\right)\to B\in \mathrm{On}$$
3	1 2	sylan	$$⊢\left(A\in \mathrm{On}\wedge B\in A\right)\to B\in \mathrm{On}$$