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

Theorem axpre-apti 6959
 Description: Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-apti 6999. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-apti ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)

Proof of Theorem axpre-apti
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 6905 . . 3 (𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)
2 elreal 6905 . . 3 (𝐵 ∈ ℝ ↔ ∃𝑦R𝑦, 0R⟩ = 𝐵)
3 breq1 3767 . . . . . 6 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝐴 <𝑦, 0R⟩))
4 breq2 3768 . . . . . 6 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑦, 0R⟩ <𝑥, 0R⟩ ↔ ⟨𝑦, 0R⟩ < 𝐴))
53, 4orbi12d 707 . . . . 5 (⟨𝑥, 0R⟩ = 𝐴 → ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ (𝐴 <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴)))
65notbid 592 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → (¬ (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ ¬ (𝐴 <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴)))
7 eqeq1 2046 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ↔ 𝐴 = ⟨𝑦, 0R⟩))
86, 7imbi12d 223 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → ((¬ (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) → ⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩) ↔ (¬ (𝐴 <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴) → 𝐴 = ⟨𝑦, 0R⟩)))
9 breq2 3768 . . . . . 6 (⟨𝑦, 0R⟩ = 𝐵 → (𝐴 <𝑦, 0R⟩ ↔ 𝐴 < 𝐵))
10 breq1 3767 . . . . . 6 (⟨𝑦, 0R⟩ = 𝐵 → (⟨𝑦, 0R⟩ < 𝐴𝐵 < 𝐴))
119, 10orbi12d 707 . . . . 5 (⟨𝑦, 0R⟩ = 𝐵 → ((𝐴 <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴) ↔ (𝐴 < 𝐵𝐵 < 𝐴)))
1211notbid 592 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → (¬ (𝐴 <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴) ↔ ¬ (𝐴 < 𝐵𝐵 < 𝐴)))
13 eqeq2 2049 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → (𝐴 = ⟨𝑦, 0R⟩ ↔ 𝐴 = 𝐵))
1412, 13imbi12d 223 . . 3 (⟨𝑦, 0R⟩ = 𝐵 → ((¬ (𝐴 <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴) → 𝐴 = ⟨𝑦, 0R⟩) ↔ (¬ (𝐴 < 𝐵𝐵 < 𝐴) → 𝐴 = 𝐵)))
15 aptisr 6863 . . . . 5 ((𝑥R𝑦R ∧ ¬ (𝑥 <R 𝑦𝑦 <R 𝑥)) → 𝑥 = 𝑦)
16153expia 1106 . . . 4 ((𝑥R𝑦R) → (¬ (𝑥 <R 𝑦𝑦 <R 𝑥) → 𝑥 = 𝑦))
17 ltresr 6915 . . . . . 6 (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝑥 <R 𝑦)
18 ltresr 6915 . . . . . 6 (⟨𝑦, 0R⟩ <𝑥, 0R⟩ ↔ 𝑦 <R 𝑥)
1917, 18orbi12i 681 . . . . 5 ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ (𝑥 <R 𝑦𝑦 <R 𝑥))
2019notbii 594 . . . 4 (¬ (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ ¬ (𝑥 <R 𝑦𝑦 <R 𝑥))
21 vex 2560 . . . . 5 𝑥 ∈ V
2221eqresr 6912 . . . 4 (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ↔ 𝑥 = 𝑦)
2316, 20, 223imtr4g 194 . . 3 ((𝑥R𝑦R) → (¬ (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) → ⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩))
241, 2, 8, 14, 232gencl 2587 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬ (𝐴 < 𝐵𝐵 < 𝐴) → 𝐴 = 𝐵))
25243impia 1101 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 629   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764  Rcnr 6395  0Rc0r 6396
 Copyright terms: Public domain W3C validator