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

Metamath Proof Explorer

Theorem axlttri

Description: Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-lttri with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion axlttri ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ A = B ∨ B < A

Proof

Step Hyp Ref Expression
1 ax-pre-lttri ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < ℝ B ↔ ¬ A = B ∨ B < ℝ A
2 ltxrlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ A < ℝ B
3 ltxrlt ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ B < ℝ A
4 3 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ B < ℝ A
5 4 orbi2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ∨ B < A ↔ A = B ∨ B < ℝ A
6 5 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ A = B ∨ B < A ↔ ¬ A = B ∨ B < ℝ A
7 1 2 6 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ A = B ∨ B < A