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 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-pre-lttri | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) ) | |
| 2 | ltxrlt | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵 ) ) | |
| 3 | ltxrlt | ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ 𝐵 <ℝ 𝐴 ) ) | |
| 4 | 3 | ancoms | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ 𝐵 <ℝ 𝐴 ) ) |
| 5 | 4 | orbi2d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) ) |
| 6 | 5 | notbid | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) ) |
| 7 | 1 2 6 | 3bitr4d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |