Metamath Proof Explorer

Theorem ordelinel

Description: The intersection of two ordinal classes is an element of a third if and only if either one of them is. (Contributed by David Moews, 1-May-2017) (Proof shortened by JJ, 24-Sep-2021)

		Ref	Expression
	Assertion	ordelinel	$⊢ (Ord A \land Ord B \land Ord C) \to (A \cap B \in C \leftrightarrow (A \in C \lor B \in C))$

Proof

Step	Hyp	Ref	Expression
1		ordtri2or3	$⊢ (Ord A \land Ord B) \to (A = A \cap B \lor B = A \cap B)$
2	1	3adant3	$⊢ (Ord A \land Ord B \land Ord C) \to (A = A \cap B \lor B = A \cap B)$
3		eleq1a	$⊢ A \cap B \in C \to (A = A \cap B \to A \in C)$
4		eleq1a	$⊢ A \cap B \in C \to (B = A \cap B \to B \in C)$
5	3 4	orim12d	$⊢ A \cap B \in C \to ((A = A \cap B \lor B = A \cap B) \to (A \in C \lor B \in C))$
6	2 5	syl5com	$⊢ (Ord A \land Ord B \land Ord C) \to (A \cap B \in C \to (A \in C \lor B \in C))$
7		ordin	$⊢ (Ord A \land Ord B) \to Ord (A \cap B)$
8		inss1	$⊢ A \cap B \subseteq A$
9		ordtr2	$⊢ (Ord (A \cap B) \land Ord C) \to ((A \cap B \subseteq A \land A \in C) \to A \cap B \in C)$
10	8 9	mpani	$⊢ (Ord (A \cap B) \land Ord C) \to (A \in C \to A \cap B \in C)$
11		inss2	$⊢ A \cap B \subseteq B$
12		ordtr2	$⊢ (Ord (A \cap B) \land Ord C) \to ((A \cap B \subseteq B \land B \in C) \to A \cap B \in C)$
13	11 12	mpani	$⊢ (Ord (A \cap B) \land Ord C) \to (B \in C \to A \cap B \in C)$
14	10 13	jaod	$⊢ (Ord (A \cap B) \land Ord C) \to ((A \in C \lor B \in C) \to A \cap B \in C)$
15	7 14	stoic3	$⊢ (Ord A \land Ord B \land Ord C) \to ((A \in C \lor B \in C) \to A \cap B \in C)$
16	6 15	impbid	$⊢ (Ord A \land Ord B \land Ord C) \to (A \cap B \in C \leftrightarrow (A \in C \lor B \in C))$