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

Metamath Proof Explorer

Theorem ordtri3

Description: A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by JJ, 24-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 ordirr ⊢ ( Ord 𝐵 → ¬ 𝐵 ∈ 𝐵 )
2 1 adantl ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ¬ 𝐵 ∈ 𝐵 )
3 eleq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵 ) )
4 3 notbid ⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵 ) )
5 2 4 syl5ibrcom ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴 ) )
6 5 pm4.71d ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴 ) ) )
7 pm5.61 ⊢ ( ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∧ ¬ 𝐵 ∈ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴 ) )
8 pm4.52 ⊢ ( ( ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∧ ¬ 𝐵 ∈ 𝐴 ) ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) )
9 7 8 bitr3i ⊢ ( ( 𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴 ) ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) )
10 6 9 bitrdi ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) ) )
11 ordtri2 ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
12 11 orbi1d ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) ) )
13 12 notbid ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ ¬ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴 ) ∨ 𝐵 ∈ 𝐴 ) ) )
14 10 13 bitr4d ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )