Metamath Proof Explorer

Theorem infsdomnn

Description: An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004) (Revised by Mario Carneiro, 27-Apr-2015)

		Ref	Expression
	Assertion	infsdomnn	$⊢ (ω ≼ A \land B \in ω) \to B ≺ A$

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex1i	$⊢ ω ≼ A \to ω \in V$
3		nnsdomg	$⊢ (ω \in V \land B \in ω) \to B ≺ ω$
4	2 3	sylan	$⊢ (ω ≼ A \land B \in ω) \to B ≺ ω$
5		simpl	$⊢ (ω ≼ A \land B \in ω) \to ω ≼ A$
6		sdomdomtr	$⊢ (B ≺ ω \land ω ≼ A) \to B ≺ A$
7	4 5 6	syl2anc	$⊢ (ω ≼ A \land B \in ω) \to B ≺ A$