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

Theorem axpre-ltwlin 6576
 Description: Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6603. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-ltwlin ((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

Proof of Theorem axpre-ltwlin
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 6540 . 2 (A ℝ ↔ x Rx, 0R⟩ = A)
2 elreal 6540 . 2 (B ℝ ↔ y Ry, 0R⟩ = B)
3 elreal 6540 . 2 (𝐶 ℝ ↔ z Rz, 0R⟩ = 𝐶)
4 breq1 3737 . . 3 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ <y, 0R⟩ ↔ A <y, 0R⟩))
5 breq1 3737 . . . 4 (⟨x, 0R⟩ = A → (⟨x, 0R⟩ <z, 0R⟩ ↔ A <z, 0R⟩))
65orbi1d 692 . . 3 (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ <z, 0Rz, 0R⟩ <y, 0R⟩) ↔ (A <z, 0Rz, 0R⟩ <y, 0R⟩)))
74, 6imbi12d 223 . 2 (⟨x, 0R⟩ = A → ((⟨x, 0R⟩ <y, 0R⟩ → (⟨x, 0R⟩ <z, 0Rz, 0R⟩ <y, 0R⟩)) ↔ (A <y, 0R⟩ → (A <z, 0Rz, 0R⟩ <y, 0R⟩))))
8 breq2 3738 . . 3 (⟨y, 0R⟩ = B → (A <y, 0R⟩ ↔ A < B))
9 breq2 3738 . . . 4 (⟨y, 0R⟩ = B → (⟨z, 0R⟩ <y, 0R⟩ ↔ ⟨z, 0R⟩ < B))
109orbi2d 691 . . 3 (⟨y, 0R⟩ = B → ((A <z, 0Rz, 0R⟩ <y, 0R⟩) ↔ (A <z, 0Rz, 0R⟩ < B)))
118, 10imbi12d 223 . 2 (⟨y, 0R⟩ = B → ((A <y, 0R⟩ → (A <z, 0Rz, 0R⟩ <y, 0R⟩)) ↔ (A < B → (A <z, 0Rz, 0R⟩ < B))))
12 breq2 3738 . . . 4 (⟨z, 0R⟩ = 𝐶 → (A <z, 0R⟩ ↔ A < 𝐶))
13 breq1 3737 . . . 4 (⟨z, 0R⟩ = 𝐶 → (⟨z, 0R⟩ < B𝐶 < B))
1412, 13orbi12d 694 . . 3 (⟨z, 0R⟩ = 𝐶 → ((A <z, 0Rz, 0R⟩ < B) ↔ (A < 𝐶 𝐶 < B)))
1514imbi2d 219 . 2 (⟨z, 0R⟩ = 𝐶 → ((A < B → (A <z, 0Rz, 0R⟩ < B)) ↔ (A < B → (A < 𝐶 𝐶 < B))))
16 ltsosr 6508 . . . 4 <R Or R
17 sowlin 4027 . . . 4 (( <R Or R (x R y R z R)) → (x <R y → (x <R z z <R y)))
1816, 17mpan 402 . . 3 ((x R y R z R) → (x <R y → (x <R z z <R y)))
19 ltresr 6549 . . 3 (⟨x, 0R⟩ <y, 0R⟩ ↔ x <R y)
20 ltresr 6549 . . . 4 (⟨x, 0R⟩ <z, 0R⟩ ↔ x <R z)
21 ltresr 6549 . . . 4 (⟨z, 0R⟩ <y, 0R⟩ ↔ z <R y)
2220, 21orbi12i 668 . . 3 ((⟨x, 0R⟩ <z, 0Rz, 0R⟩ <y, 0R⟩) ↔ (x <R z z <R y))
2318, 19, 223imtr4g 194 . 2 ((x R y R z R) → (⟨x, 0R⟩ <y, 0R⟩ → (⟨x, 0R⟩ <z, 0Rz, 0R⟩ <y, 0R⟩)))
241, 2, 3, 7, 11, 15, 233gencl 2561 1 ((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 616   ∧ w3a 871   = wceq 1226   ∈ wcel 1370  ⟨cop 3349   class class class wbr 3734   Or wor 4002  Rcnr 6151  0Rc0r 6152
 Copyright terms: Public domain W3C validator