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

Theorem axpre-ltirr 6766
 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 6795. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-ltirr (A ℝ → ¬ A < A)

Proof of Theorem axpre-ltirr
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 elreal 6727 . . 3 (A ℝ ↔ x Rx, 0R⟩ = A)
2 df-rex 2306 . . 3 (x Rx, 0R⟩ = Ax(x R x, 0R⟩ = A))
31, 2bitri 173 . 2 (A ℝ ↔ x(x R x, 0R⟩ = A))
4 id 19 . . . 4 (⟨x, 0R⟩ = A → ⟨x, 0R⟩ = A)
54, 4breq12d 3768 . . 3 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ <x, 0R⟩ ↔ A < A))
65notbid 591 . 2 (⟨x, 0R⟩ = A → (¬ ⟨x, 0R⟩ <x, 0R⟩ ↔ ¬ A < A))
7 ltsosr 6692 . . . . 5 <R Or R
8 ltrelsr 6666 . . . . 5 <R ⊆ (R × R)
97, 8soirri 4662 . . . 4 ¬ x <R x
10 ltresr 6736 . . . 4 (⟨x, 0R⟩ <x, 0R⟩ ↔ x <R x)
119, 10mtbir 595 . . 3 ¬ ⟨x, 0R⟩ <x, 0R
1211a1i 9 . 2 (x R → ¬ ⟨x, 0R⟩ <x, 0R⟩)
133, 6, 12gencl 2580 1 (A ℝ → ¬ A < A)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755  Rcnr 6281  0Rc0r 6282
 Copyright terms: Public domain W3C validator