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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℝ$$
5	2 4	wa	$$wff\left(A\in ℝ\wedge B\in ℝ\right)$$
6		cltrr	$$class{<}_{ℝ}$$
7	0 3 6	wbr	$$wffA{<}_{ℝ}B$$
8	0 3	wceq	$$wffA=B$$
9	3 0 6	wbr	$$wffB{<}_{ℝ}A$$
10	8 9	wo	$$wff\left(A=B\vee B{<}_{ℝ}A\right)$$
11	10	wn	$$wff\neg \left(A=B\vee B{<}_{ℝ}A\right)$$
12	7 11	wb	$$wff\left(A{<}_{ℝ}B\leftrightarrow \neg \left(A=B\vee B{<}_{ℝ}A\right)\right)$$
13	5 12	wi	$$wff\left(\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{<}_{ℝ}B\leftrightarrow \neg \left(A=B\vee B{<}_{ℝ}A\right)\right)\right)$$