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