Metamath Proof Explorer


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 𝖫𝗂𝗆𝗂𝗍𝗌 On

Proof

Step Hyp Ref Expression
1 df-limits 𝖫𝗂𝗆𝗂𝗍𝗌 = On 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉
2 difss On 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 On 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉
3 inss1 On 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 On
4 2 3 sstri On 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 On
5 1 4 eqsstri 𝖫𝗂𝗆𝗂𝗍𝗌 On