Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  axpre-ltirr GIF version

Theorem axpre-ltirr 7014
 Description: Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 7054. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-ltirr (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)

Proof of Theorem axpre-ltirr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elreal 6963 . . 3 (𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)
2 df-rex 2329 . . 3 (∃𝑥R𝑥, 0R⟩ = 𝐴 ↔ ∃𝑥(𝑥R ∧ ⟨𝑥, 0R⟩ = 𝐴))
31, 2bitri 177 . 2 (𝐴 ∈ ℝ ↔ ∃𝑥(𝑥R ∧ ⟨𝑥, 0R⟩ = 𝐴))
4 id 19 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → ⟨𝑥, 0R⟩ = 𝐴)
54, 4breq12d 3805 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ <𝑥, 0R⟩ ↔ 𝐴 < 𝐴))
65notbid 602 . 2 (⟨𝑥, 0R⟩ = 𝐴 → (¬ ⟨𝑥, 0R⟩ <𝑥, 0R⟩ ↔ ¬ 𝐴 < 𝐴))
7 ltsosr 6907 . . . . 5 <R Or R
8 ltrelsr 6881 . . . . 5 <R ⊆ (R × R)
97, 8soirri 4747 . . . 4 ¬ 𝑥 <R 𝑥
10 ltresr 6973 . . . 4 (⟨𝑥, 0R⟩ <𝑥, 0R⟩ ↔ 𝑥 <R 𝑥)
119, 10mtbir 606 . . 3 ¬ ⟨𝑥, 0R⟩ <𝑥, 0R
1211a1i 9 . 2 (𝑥R → ¬ ⟨𝑥, 0R⟩ <𝑥, 0R⟩)
133, 6, 12gencl 2603 1 (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 101   = wceq 1259  ∃wex 1397   ∈ wcel 1409  ∃wrex 2324  ⟨cop 3406   class class class wbr 3792  Rcnr 6453  0Rc0r 6454
 Copyright terms: Public domain W3C validator