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	|- Limits C_ On

Proof

Step	Hyp	Ref	Expression
1		df-limits	|- Limits = ( ( On i^i Fix Bigcup ) \ { (/) } )
2		difss	|- ( ( On i^i Fix Bigcup ) \ { (/) } ) C_ ( On i^i Fix Bigcup )
3		inss1	|- ( On i^i Fix Bigcup ) C_ On
4	2 3	sstri	|- ( ( On i^i Fix Bigcup ) \ { (/) } ) C_ On
5	1 4	eqsstri	|- Limits C_ On