# 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 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({A}\cap {B}\in {C}↔\left({A}\in {C}\vee {B}\in {C}\right)\right)$

### Proof

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