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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) )

Detailed syntax breakdown

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