# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔¬\left({A}={B}\vee {B}<{A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ax-pre-lttri ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}{<}_{ℝ}{B}↔¬\left({A}={B}\vee {B}{<}_{ℝ}{A}\right)\right)$
2 ltxrlt ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔{A}{<}_{ℝ}{B}\right)$
3 ltxrlt ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to \left({B}<{A}↔{B}{<}_{ℝ}{A}\right)$
4 3 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({B}<{A}↔{B}{<}_{ℝ}{A}\right)$
5 4 orbi2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({A}={B}\vee {B}<{A}\right)↔\left({A}={B}\vee {B}{<}_{ℝ}{A}\right)\right)$
6 5 notbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(¬\left({A}={B}\vee {B}<{A}\right)↔¬\left({A}={B}\vee {B}{<}_{ℝ}{A}\right)\right)$
7 1 2 6 3bitr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔¬\left({A}={B}\vee {B}<{A}\right)\right)$