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

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

Proof

Step Hyp Ref Expression
1 nelss ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → ¬ 𝐵 ⊆ 𝐶 )
2 1 adantl ⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ¬ 𝐵 ⊆ 𝐶 )
3 ordtri1 ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝐵 ) )
4 3 con2bid ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐶 ∈ 𝐵 ↔ ¬ 𝐵 ⊆ 𝐶 ) )
5 4 adantr ⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → ( 𝐶 ∈ 𝐵 ↔ ¬ 𝐵 ⊆ 𝐶 ) )
6 2 5 mpbird ⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) → 𝐶 ∈ 𝐵 )
7 6 expr ⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ 𝐶 → 𝐶 ∈ 𝐵 ) )
8 7 orrd ⊢ ( ( ( Ord 𝐵 ∧ Ord 𝐶 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) )
9 8 ex ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵 ) ) )