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 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ↔ ( 𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtri2or3	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ∨ 𝐵 = ( 𝐴 ∩ 𝐵 ) ) )
2	1	3adant3	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ∨ 𝐵 = ( 𝐴 ∩ 𝐵 ) ) )
3		eleq1a	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 → ( 𝐴 = ( 𝐴 ∩ 𝐵 ) → 𝐴 ∈ 𝐶 ) )
4		eleq1a	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 → ( 𝐵 = ( 𝐴 ∩ 𝐵 ) → 𝐵 ∈ 𝐶 ) )
5	3 4	orim12d	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 → ( ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ∨ 𝐵 = ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶 ) ) )
6	2 5	syl5com	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 → ( 𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶 ) ) )
7		ordin	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord ( 𝐴 ∩ 𝐵 ) )
8		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
9		ordtr2	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐶 ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ) )
10	8 9	mpani	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐶 ) → ( 𝐴 ∈ 𝐶 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ) )
11		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
12		ordtr2	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐶 ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ) )
13	11 12	mpani	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐶 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ) )
14	10 13	jaod	⊢ ( ( Ord ( 𝐴 ∩ 𝐵 ) ∧ Ord 𝐶 ) → ( ( 𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ) )
15	7 14	stoic3	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶 ) → ( ( 𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ) )
16	6 15	impbid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 ↔ ( 𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶 ) ) )