This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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