Metamath Proof Explorer

Theorem infsdomnnOLD

Description: Obsolete version of infsdomnn as of 7-Jan-2025. (Contributed by NM, 22-Nov-2004) (Revised by Mario Carneiro, 27-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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$