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\leftrightarrow \neg \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\leftrightarrow \neg \left(A=B\vee B{<}_{ℝ}A\right)\right)$$
2		ltxrlt	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow A{<}_{ℝ}B\right)$$
3		ltxrlt	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B<A\leftrightarrow B{<}_{ℝ}A\right)$$
4	3	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B<A\leftrightarrow B{<}_{ℝ}A\right)$$
5	4	orbi2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A=B\vee B<A\right)\leftrightarrow \left(A=B\vee B{<}_{ℝ}A\right)\right)$$
6	5	notbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\neg \left(A=B\vee B<A\right)\leftrightarrow \neg \left(A=B\vee B{<}_{ℝ}A\right)\right)$$
7	1 2 6	3bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow \neg \left(A=B\vee B<A\right)\right)$$