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

Theorem axpre-apti 6769
 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 6798. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-apti ((A B ¬ (A < B B < A)) → A = B)

Proof of Theorem axpre-apti
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 6727 . . 3 (A ℝ ↔ x Rx, 0R⟩ = A)
2 elreal 6727 . . 3 (B ℝ ↔ y Ry, 0R⟩ = B)
3 breq1 3758 . . . . . 6 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ <y, 0R⟩ ↔ A <y, 0R⟩))
4 breq2 3759 . . . . . 6 (⟨x, 0R⟩ = A → (⟨y, 0R⟩ <x, 0R⟩ ↔ ⟨y, 0R⟩ < A))
53, 4orbi12d 706 . . . . 5 (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ (A <y, 0Ry, 0R⟩ < A)))
65notbid 591 . . . 4 (⟨x, 0R⟩ = A → (¬ (⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ ¬ (A <y, 0Ry, 0R⟩ < A)))
7 eqeq1 2043 . . . 4 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ = ⟨y, 0R⟩ ↔ A = ⟨y, 0R⟩))
86, 7imbi12d 223 . . 3 (⟨x, 0R⟩ = A → ((¬ (⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) → ⟨x, 0R⟩ = ⟨y, 0R⟩) ↔ (¬ (A <y, 0Ry, 0R⟩ < A) → A = ⟨y, 0R⟩)))
9 breq2 3759 . . . . . 6 (⟨y, 0R⟩ = B → (A <y, 0R⟩ ↔ A < B))
10 breq1 3758 . . . . . 6 (⟨y, 0R⟩ = B → (⟨y, 0R⟩ < AB < A))
119, 10orbi12d 706 . . . . 5 (⟨y, 0R⟩ = B → ((A <y, 0Ry, 0R⟩ < A) ↔ (A < B B < A)))
1211notbid 591 . . . 4 (⟨y, 0R⟩ = B → (¬ (A <y, 0Ry, 0R⟩ < A) ↔ ¬ (A < B B < A)))
13 eqeq2 2046 . . . 4 (⟨y, 0R⟩ = B → (A = ⟨y, 0R⟩ ↔ A = B))
1412, 13imbi12d 223 . . 3 (⟨y, 0R⟩ = B → ((¬ (A <y, 0Ry, 0R⟩ < A) → A = ⟨y, 0R⟩) ↔ (¬ (A < B B < A) → A = B)))
15 aptisr 6705 . . . . 5 ((x R y R ¬ (x <R y y <R x)) → x = y)
16153expia 1105 . . . 4 ((x R y R) → (¬ (x <R y y <R x) → x = y))
17 ltresr 6736 . . . . . 6 (⟨x, 0R⟩ <y, 0R⟩ ↔ x <R y)
18 ltresr 6736 . . . . . 6 (⟨y, 0R⟩ <x, 0R⟩ ↔ y <R x)
1917, 18orbi12i 680 . . . . 5 ((⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ (x <R y y <R x))
2019notbii 593 . . . 4 (¬ (⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) ↔ ¬ (x <R y y <R x))
21 vex 2554 . . . . 5 x V
2221eqresr 6733 . . . 4 (⟨x, 0R⟩ = ⟨y, 0R⟩ ↔ x = y)
2316, 20, 223imtr4g 194 . . 3 ((x R y R) → (¬ (⟨x, 0R⟩ <y, 0Ry, 0R⟩ <x, 0R⟩) → ⟨x, 0R⟩ = ⟨y, 0R⟩))
241, 2, 8, 14, 232gencl 2581 . 2 ((A B ℝ) → (¬ (A < B B < A) → A = B))
25243impia 1100 1 ((A B ¬ (A < B B < A)) → A = B)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  Rcnr 6281  0Rc0r 6282
 Copyright terms: Public domain W3C validator