Definition df-limits

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

	Ref	Expression
Assertion	df-limits	$$⊢\mathrm{𝖫𝗂𝗆𝗂𝗍𝗌}=\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)\setminus \left\{\varnothing \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		climits	$$class\mathrm{𝖫𝗂𝗆𝗂𝗍𝗌}$$
1		con0	$$class\mathrm{On}$$
2		cbigcup	$$class\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}$$
3	2	cfix	$$class\mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}$$
4	1 3	cin	$$class\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)$$
5		c0	$$class\varnothing$$
6	5	csn	$$class\left\{\varnothing \right\}$$
7	4 6	cdif	$$class\left(\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)\setminus \left\{\varnothing \right\}\right)$$
8	0 7	wceq	$$wff\mathrm{𝖫𝗂𝗆𝗂𝗍𝗌}=\left(\mathrm{On}\cap \mathrm{𝖥𝗂𝗑}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\right)\setminus \left\{\varnothing \right\}$$