Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		ssdomg	$⊢ ω \in V \to (A \subseteq ω \to A ≼ ω)$
2		ordom	$⊢ Ord ω$
3		ordelss	$⊢ (Ord ω \land A \in ω) \to A \subseteq ω$
4	2 3	mpan	$⊢ A \in ω \to A \subseteq ω$
5	1 4	impel	$⊢ (ω \in V \land A \in ω) \to A ≼ ω$
6		ominf	$⊢ \neg ω \in Fin$
7		ensym	$⊢ A \approx ω \to ω \approx A$
8		breq2	$⊢ x = A \to (ω \approx x \leftrightarrow ω \approx A)$
9	8	rspcev	$⊢ (A \in ω \land ω \approx A) \to \exists x \in ω ω \approx x$
10		isfi	$⊢ ω \in Fin \leftrightarrow \exists x \in ω ω \approx x$
11	9 10	sylibr	$⊢ (A \in ω \land ω \approx A) \to ω \in Fin$
12	11	ex	$⊢ A \in ω \to (ω \approx A \to ω \in Fin)$
13	7 12	syl5	$⊢ A \in ω \to (A \approx ω \to ω \in Fin)$
14	6 13	mtoi	$⊢ A \in ω \to \neg A \approx ω$
15	14	adantl	$⊢ (ω \in V \land A \in ω) \to \neg A \approx ω$
16		brsdom	$⊢ A ≺ ω \leftrightarrow (A ≼ ω \land \neg A \approx ω)$
17	5 15 16	sylanbrc	$⊢ (ω \in V \land A \in ω) \to A ≺ ω$