Theorem limitssson

Description: The class of all limit ordinals is a subclass of the class of all ordinals. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	limitssson	$$⊢\mathrm{𝖫𝗂𝗆𝗂𝗍𝗌}\subseteq \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		df-limits	$$⊢\mathrm{𝖫𝗂𝗆𝗂𝗍𝗌}=\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)\setminus \left\{\varnothing \right\}$$
2		difss	$$⊢\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)\setminus \left\{\varnothing \right\}\subseteq \mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}$$
3		inss1	$$⊢\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\subseteq \mathrm{On}$$
4	2 3	sstri	$$⊢\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)\setminus \left\{\varnothing \right\}\subseteq \mathrm{On}$$
5	1 4	eqsstri	$$⊢\mathrm{𝖫𝗂𝗆𝗂𝗍𝗌}\subseteq \mathrm{On}$$