onsdominel

Description: An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014)

		Ref	Expression
	Assertion	onsdominel	$⊢ (A \in On \land B \in On \land (A \cap C) ≺ (B \cap C)) \to A \in B$

Step	Hyp	Ref	Expression
1		ontri1	$⊢ (B \in On \land A \in On) \to (B \subseteq A \leftrightarrow \neg A \in B)$
2	1	ancoms	$⊢ (A \in On \land B \in On) \to (B \subseteq A \leftrightarrow \neg A \in B)$
3		inex1g	$⊢ A \in On \to A \cap C \in V$
4		ssrin	$⊢ B \subseteq A \to B \cap C \subseteq A \cap C$
5		ssdomg	$⊢ A \cap C \in V \to (B \cap C \subseteq A \cap C \to (B \cap C) ≼ (A \cap C))$
6	3 4 5	syl2im	$⊢ A \in On \to (B \subseteq A \to (B \cap C) ≼ (A \cap C))$
7		domnsym	$⊢ (B \cap C) ≼ (A \cap C) \to \neg (A \cap C) ≺ (B \cap C)$
8	6 7	syl6	$⊢ A \in On \to (B \subseteq A \to \neg (A \cap C) ≺ (B \cap C))$
9	8	adantr	$⊢ (A \in On \land B \in On) \to (B \subseteq A \to \neg (A \cap C) ≺ (B \cap C))$
10	2 9	sylbird	$⊢ (A \in On \land B \in On) \to (\neg A \in B \to \neg (A \cap C) ≺ (B \cap C))$
11	10	con4d	$⊢ (A \in On \land B \in On) \to ((A \cap C) ≺ (B \cap C) \to A \in B)$
12	11	3impia	$⊢ (A \in On \land B \in On \land (A \cap C) ≺ (B \cap C)) \to A \in B$

Metamath Proof Explorer