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 ) ) )
2 1 3adant3 
 |-  ( ( 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 ) ) )