Metamath Proof Explorer

Axiom ax-pre-lttri

Description: Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by theorem axpre-lttri . Note: The more general version for extended reals is axlttri . Normally new proofs would use xrlttri . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-lttri ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < ℝ B ↔ ¬ A = B ∨ B < ℝ A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class ℝ
2 0 1 wcel wff A ∈ ℝ
3 cB class B
4 3 1 wcel wff B ∈ ℝ
5 2 4 wa wff A ∈ ℝ ∧ B ∈ ℝ
6 cltrr class < ℝ
7 0 3 6 wbr wff A < ℝ B
8 0 3 wceq wff A = B
9 3 0 6 wbr wff B < ℝ A
10 8 9 wo wff A = B ∨ B < ℝ A
11 10 wn wff ¬ A = B ∨ B < ℝ A
12 7 11 wb wff A < ℝ B ↔ ¬ A = B ∨ B < ℝ A
13 5 12 wi wff A ∈ ℝ ∧ B ∈ ℝ → A < ℝ B ↔ ¬ A = B ∨ B < ℝ A