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	$⊢ (ω \in V \land A \in ω) \to A ≺ ω$

Proof

Step	Hyp	Ref	Expression
1		ordom	$⊢ Ord ω$
2		ordelss	$⊢ (Ord ω \land A \in ω) \to A \subseteq ω$
3	1 2	mpan	$⊢ A \in ω \to A \subseteq ω$
4	3	adantr	$⊢ (A \in ω \land ω \in V) \to A \subseteq ω$
5		nnfi	$⊢ A \in ω \to A \in Fin$
6		ssdomfi2	$⊢ (A \in Fin \land ω \in V \land A \subseteq ω) \to A ≼ ω$
7	5 6	syl3an1	$⊢ (A \in ω \land ω \in V \land A \subseteq ω) \to A ≼ ω$
8	4 7	mpd3an3	$⊢ (A \in ω \land ω \in V) \to A ≼ ω$
9	8	ancoms	$⊢ (ω \in V \land A \in ω) \to A ≼ ω$
10		ominf	$⊢ \neg ω \in Fin$
11		ensymfib	$⊢ A \in Fin \to (A \approx ω \leftrightarrow ω \approx A)$
12	5 11	syl	$⊢ A \in ω \to (A \approx ω \leftrightarrow ω \approx A)$
13		breq2	$⊢ x = A \to (ω \approx x \leftrightarrow ω \approx A)$
14	13	rspcev	$⊢ (A \in ω \land ω \approx A) \to \exists x \in ω ω \approx x$
15		isfi	$⊢ ω \in Fin \leftrightarrow \exists x \in ω ω \approx x$
16	14 15	sylibr	$⊢ (A \in ω \land ω \approx A) \to ω \in Fin$
17	16	ex	$⊢ A \in ω \to (ω \approx A \to ω \in Fin)$
18	12 17	sylbid	$⊢ A \in ω \to (A \approx ω \to ω \in Fin)$
19	10 18	mtoi	$⊢ A \in ω \to \neg A \approx ω$
20	19	adantl	$⊢ (ω \in V \land A \in ω) \to \neg A \approx ω$
21		brsdom	$⊢ A ≺ ω \leftrightarrow (A ≼ ω \land \neg A \approx ω)$
22	9 20 21	sylanbrc	$⊢ (ω \in V \land A \in ω) \to A ≺ ω$

Metamath Proof Explorer

Theorem nnsdomg

Proof