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 ⊆ On

Proof

Step	Hyp	Ref	Expression
1		df-limits	⊢ Limits = ( ( On ∩ Fix Bigcup ) ∖ { ∅ } )
2		difss	⊢ ( ( On ∩ Fix Bigcup ) ∖ { ∅ } ) ⊆ ( On ∩ Fix Bigcup )
3		inss1	⊢ ( On ∩ Fix Bigcup ) ⊆ On
4	2 3	sstri	⊢ ( ( On ∩ Fix Bigcup ) ∖ { ∅ } ) ⊆ On
5	1 4	eqsstri	⊢ Limits ⊆ On