Theorem omsson

Description: Omega is a subset of On . (Contributed by NM, 13-Jun-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	omsson	⊢ ω ⊆ On

Proof

Step	Hyp	Ref	Expression
1		dfom2	⊢ ω = { 𝑥 ∈ On ∣ suc 𝑥 ⊆ { 𝑦 ∈ On ∣ ¬ Lim 𝑦 } }
2	1	ssrab3	⊢ ω ⊆ On