Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-pre-ltirr | GIF version |
Description: Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7839. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Ref | Expression |
---|---|
ax-pre-ltirr | ⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cr 7726 | . . 3 class ℝ | |
3 | 1, 2 | wcel 2128 | . 2 wff 𝐴 ∈ ℝ |
4 | cltrr 7731 | . . . 4 class <ℝ | |
5 | 1, 1, 4 | wbr 3965 | . . 3 wff 𝐴 <ℝ 𝐴 |
6 | 5 | wn 3 | . 2 wff ¬ 𝐴 <ℝ 𝐴 |
7 | 3, 6 | wi 4 | 1 wff (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴) |
Colors of variables: wff set class |
This axiom is referenced by: axltirr 7939 |
Copyright terms: Public domain | W3C validator |