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

Metamath Proof Explorer

Theorem ordtri2

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995)

Ref Expression
Assertion ordtri2 ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ordsseleq ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
2 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
3 2 orbi2i ⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵 ) )
4 orcom ⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )
5 3 4 bitri ⊢ ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) )
6 1 5 bitrdi ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
7 ordtri1 ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
8 6 7 bitr3d ⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
9 8 ancoms ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
10 9 con2bid ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )