Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-pre-ltwlin | GIF version |
Description: Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 7838. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Ref | Expression |
---|---|
ax-pre-ltwlin | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class 𝐴 | |
2 | cr 7766 | . . . 4 class ℝ | |
3 | 1, 2 | wcel 2141 | . . 3 wff 𝐴 ∈ ℝ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2141 | . . 3 wff 𝐵 ∈ ℝ |
6 | cC | . . . 4 class 𝐶 | |
7 | 6, 2 | wcel 2141 | . . 3 wff 𝐶 ∈ ℝ |
8 | 3, 5, 7 | w3a 973 | . 2 wff (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) |
9 | cltrr 7771 | . . . 4 class <ℝ | |
10 | 1, 4, 9 | wbr 3987 | . . 3 wff 𝐴 <ℝ 𝐵 |
11 | 1, 6, 9 | wbr 3987 | . . . 4 wff 𝐴 <ℝ 𝐶 |
12 | 6, 4, 9 | wbr 3987 | . . . 4 wff 𝐶 <ℝ 𝐵 |
13 | 11, 12 | wo 703 | . . 3 wff (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵) |
14 | 10, 13 | wi 4 | . 2 wff (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)) |
15 | 8, 14 | wi 4 | 1 wff ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) |
Colors of variables: wff set class |
This axiom is referenced by: axltwlin 7980 |
Copyright terms: Public domain | W3C validator |