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 part of the antecedent. See nnsdom for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998) Avoid ax-pow . (Revised by BTernaryTau, 7-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ordom	⊢ Ord ω
2		ordelss	⊢ ( ( Ord ω ∧ 𝐴 ∈ ω ) → 𝐴 ⊆ ω )
3	1 2	mpan	⊢ ( 𝐴 ∈ ω → 𝐴 ⊆ ω )
4	3	adantr	⊢ ( ( 𝐴 ∈ ω ∧ ω ∈ V ) → 𝐴 ⊆ ω )
5		nnfi	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
6		ssdomfi2	⊢ ( ( 𝐴 ∈ Fin ∧ ω ∈ V ∧ 𝐴 ⊆ ω ) → 𝐴 ≼ ω )
7	5 6	syl3an1	⊢ ( ( 𝐴 ∈ ω ∧ ω ∈ V ∧ 𝐴 ⊆ ω ) → 𝐴 ≼ ω )
8	4 7	mpd3an3	⊢ ( ( 𝐴 ∈ ω ∧ ω ∈ V ) → 𝐴 ≼ ω )
9	8	ancoms	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → 𝐴 ≼ ω )
10		ominf	⊢ ¬ ω ∈ Fin
11		ensymfib	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ ω ↔ ω ≈ 𝐴 ) )
12	5 11	syl	⊢ ( 𝐴 ∈ ω → ( 𝐴 ≈ ω ↔ ω ≈ 𝐴 ) )
13		breq2	⊢ ( 𝑥 = 𝐴 → ( ω ≈ 𝑥 ↔ ω ≈ 𝐴 ) )
14	13	rspcev	⊢ ( ( 𝐴 ∈ ω ∧ ω ≈ 𝐴 ) → ∃ 𝑥 ∈ ω ω ≈ 𝑥 )
15		isfi	⊢ ( ω ∈ Fin ↔ ∃ 𝑥 ∈ ω ω ≈ 𝑥 )
16	14 15	sylibr	⊢ ( ( 𝐴 ∈ ω ∧ ω ≈ 𝐴 ) → ω ∈ Fin )
17	16	ex	⊢ ( 𝐴 ∈ ω → ( ω ≈ 𝐴 → ω ∈ Fin ) )
18	12 17	sylbid	⊢ ( 𝐴 ∈ ω → ( 𝐴 ≈ ω → ω ∈ Fin ) )
19	10 18	mtoi	⊢ ( 𝐴 ∈ ω → ¬ 𝐴 ≈ ω )
20	19	adantl	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → ¬ 𝐴 ≈ ω )
21		brsdom	⊢ ( 𝐴 ≺ ω ↔ ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≈ ω ) )
22	9 20 21	sylanbrc	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ ω ) → 𝐴 ≺ ω )