Metamath Proof Explorer

Theorem ordtr3

Description: Transitive law for ordinal classes. (Contributed by Mario Carneiro, 30-Dec-2014) (Proof shortened by JJ, 24-Sep-2021)

Ref Expression
Assertion ordtr3 ⊢ Ord ⁡ B ∧ Ord ⁡ C → A ∈ B → A ∈ C ∨ C ∈ B

Proof

Step Hyp Ref Expression
1 nelss ⊢ A ∈ B ∧ ¬ A ∈ C → ¬ B ⊆ C
2 1 adantl ⊢ Ord ⁡ B ∧ Ord ⁡ C ∧ A ∈ B ∧ ¬ A ∈ C → ¬ B ⊆ C
3 ordtri1 ⊢ Ord ⁡ B ∧ Ord ⁡ C → B ⊆ C ↔ ¬ C ∈ B
4 3 con2bid ⊢ Ord ⁡ B ∧ Ord ⁡ C → C ∈ B ↔ ¬ B ⊆ C
5 4 adantr ⊢ Ord ⁡ B ∧ Ord ⁡ C ∧ A ∈ B ∧ ¬ A ∈ C → C ∈ B ↔ ¬ B ⊆ C
6 2 5 mpbird ⊢ Ord ⁡ B ∧ Ord ⁡ C ∧ A ∈ B ∧ ¬ A ∈ C → C ∈ B
7 6 expr ⊢ Ord ⁡ B ∧ Ord ⁡ C ∧ A ∈ B → ¬ A ∈ C → C ∈ B
8 7 orrd ⊢ Ord ⁡ B ∧ Ord ⁡ C ∧ A ∈ B → A ∈ C ∨ C ∈ B
9 8 ex ⊢ Ord ⁡ B ∧ Ord ⁡ C → A ∈ B → A ∈ C ∨ C ∈ B