sdomel

Description: For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013)

		Ref	Expression
	Assertion	sdomel	$⊢ (A \in On \land B \in On) \to (A ≺ B \to A \in B)$

Step	Hyp	Ref	Expression
1		ssdomg	$⊢ A \in On \to (B \subseteq A \to B ≼ A)$
2	1	adantl	$⊢ (B \in On \land A \in On) \to (B \subseteq A \to B ≼ A)$
3		ontri1	$⊢ (B \in On \land A \in On) \to (B \subseteq A \leftrightarrow \neg A \in B)$
4		domtriord	$⊢ (B \in On \land A \in On) \to (B ≼ A \leftrightarrow \neg A ≺ B)$
5	2 3 4	3imtr3d	$⊢ (B \in On \land A \in On) \to (\neg A \in B \to \neg A ≺ B)$
6	5	con4d	$⊢ (B \in On \land A \in On) \to (A ≺ B \to A \in B)$
7	6	ancoms	$⊢ (A \in On \land B \in On) \to (A ≺ B \to A \in B)$

Metamath Proof Explorer