# 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 /\ Ord B /\ Ord C ) -> ( ( A i^i B ) e. C <-> ( A e. C \/ B e. C ) ) )`

### Proof

Step Hyp Ref Expression
1 ordtri2or3
` |-  ( ( Ord A /\ Ord B ) -> ( A = ( A i^i B ) \/ B = ( A i^i B ) ) )`
` |-  ( ( Ord A /\ Ord B /\ Ord C ) -> ( A = ( A i^i B ) \/ B = ( A i^i B ) ) )`
3 eleq1a
` |-  ( ( A i^i B ) e. C -> ( A = ( A i^i B ) -> A e. C ) )`
4 eleq1a
` |-  ( ( A i^i B ) e. C -> ( B = ( A i^i B ) -> B e. C ) )`
5 3 4 orim12d
` |-  ( ( A i^i B ) e. C -> ( ( A = ( A i^i B ) \/ B = ( A i^i B ) ) -> ( A e. C \/ B e. C ) ) )`
6 2 5 syl5com
` |-  ( ( Ord A /\ Ord B /\ Ord C ) -> ( ( A i^i B ) e. C -> ( A e. C \/ B e. C ) ) )`
7 ordin
` |-  ( ( Ord A /\ Ord B ) -> Ord ( A i^i B ) )`
8 inss1
` |-  ( A i^i B ) C_ A`
9 ordtr2
` |-  ( ( Ord ( A i^i B ) /\ Ord C ) -> ( ( ( A i^i B ) C_ A /\ A e. C ) -> ( A i^i B ) e. C ) )`
10 8 9 mpani
` |-  ( ( Ord ( A i^i B ) /\ Ord C ) -> ( A e. C -> ( A i^i B ) e. C ) )`
11 inss2
` |-  ( A i^i B ) C_ B`
12 ordtr2
` |-  ( ( Ord ( A i^i B ) /\ Ord C ) -> ( ( ( A i^i B ) C_ B /\ B e. C ) -> ( A i^i B ) e. C ) )`
13 11 12 mpani
` |-  ( ( Ord ( A i^i B ) /\ Ord C ) -> ( B e. C -> ( A i^i B ) e. C ) )`
14 10 13 jaod
` |-  ( ( Ord ( A i^i B ) /\ Ord C ) -> ( ( A e. C \/ B e. C ) -> ( A i^i B ) e. C ) )`
15 7 14 stoic3
` |-  ( ( Ord A /\ Ord B /\ Ord C ) -> ( ( A e. C \/ B e. C ) -> ( A i^i B ) e. C ) )`
16 6 15 impbid
` |-  ( ( Ord A /\ Ord B /\ Ord C ) -> ( ( A i^i B ) e. C <-> ( A e. C \/ B e. C ) ) )`