Theorem nnsdomg

Description: Omega strictly dominates a natural number. Example 3 of Enderton p. 146. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 15-Jun-1998)

	Ref	Expression
Assertion	nnsdomg	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → 𝐴 ≺ ω )

Proof

Step	Hyp	Ref	Expression
1		ssdomg	⊢ ( ω ∈ V → ( 𝐴 ⊆ ω → 𝐴 ≼ ω ) )
2		ordom	⊢ Ord ω
3		ordelss	⊢ ( ( Ord ω ∧ 𝐴 ∈ ω ) → 𝐴 ⊆ ω )
4	2 3	mpan	⊢ ( 𝐴 ∈ ω → 𝐴 ⊆ ω )
5	1 4	impel	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → 𝐴 ≼ ω )
6		ominf	⊢ ¬ ω ∈ Fin
7		ensym	⊢ ( 𝐴 ≈ ω → ω ≈ 𝐴 )
8		breq2	⊢ ( 𝑥 = 𝐴 → ( ω ≈ 𝑥 ↔ ω ≈ 𝐴 ) )
9	8	rspcev	⊢ ( ( 𝐴 ∈ ω ∧ ω ≈ 𝐴 ) → ∃ 𝑥 ∈ ω ω ≈ 𝑥 )
10		isfi	⊢ ( ω ∈ Fin ↔ ∃ 𝑥 ∈ ω ω ≈ 𝑥 )
11	9 10	sylibr	⊢ ( ( 𝐴 ∈ ω ∧ ω ≈ 𝐴 ) → ω ∈ Fin )
12	11	ex	⊢ ( 𝐴 ∈ ω → ( ω ≈ 𝐴 → ω ∈ Fin ) )
13	7 12	syl5	⊢ ( 𝐴 ∈ ω → ( 𝐴 ≈ ω → ω ∈ Fin ) )
14	6 13	mtoi	⊢ ( 𝐴 ∈ ω → ¬ 𝐴 ≈ ω )
15	14	adantl	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → ¬ 𝐴 ≈ ω )
16		brsdom	⊢ ( 𝐴 ≺ ω ↔ ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≈ ω ) )
17	5 15 16	sylanbrc	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → 𝐴 ≺ ω )