Theorem nnsdom

Description: A natural number is strictly dominated by the set of natural numbers. Example 3 of Enderton p. 146. (Contributed by NM, 28-Oct-2003)

	Ref	Expression
Assertion	nnsdom	⊢ ( 𝐴 ∈ ω → 𝐴 ≺ ω )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		nnsdomg	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → 𝐴 ≺ ω )
3	1 2	mpan	⊢ ( 𝐴 ∈ ω → 𝐴 ≺ ω )