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

Theorem axpre-lttrn 7182
 Description: Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 7222. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-lttrn ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Proof of Theorem axpre-lttrn
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 7129 . 2 (𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)
2 elreal 7129 . 2 (𝐵 ∈ ℝ ↔ ∃𝑦R𝑦, 0R⟩ = 𝐵)
3 elreal 7129 . 2 (𝐶 ∈ ℝ ↔ ∃𝑧R𝑧, 0R⟩ = 𝐶)
4 breq1 3808 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝐴 <𝑦, 0R⟩))
54anbi1d 453 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) ↔ (𝐴 <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩)))
6 breq1 3808 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ <𝑧, 0R⟩ ↔ 𝐴 <𝑧, 0R⟩))
75, 6imbi12d 232 . 2 (⟨𝑥, 0R⟩ = 𝐴 → (((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) → ⟨𝑥, 0R⟩ <𝑧, 0R⟩) ↔ ((𝐴 <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) → 𝐴 <𝑧, 0R⟩)))
8 breq2 3809 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → (𝐴 <𝑦, 0R⟩ ↔ 𝐴 < 𝐵))
9 breq1 3808 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → (⟨𝑦, 0R⟩ <𝑧, 0R⟩ ↔ 𝐵 <𝑧, 0R⟩))
108, 9anbi12d 457 . . 3 (⟨𝑦, 0R⟩ = 𝐵 → ((𝐴 <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) ↔ (𝐴 < 𝐵𝐵 <𝑧, 0R⟩)))
1110imbi1d 229 . 2 (⟨𝑦, 0R⟩ = 𝐵 → (((𝐴 <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) → 𝐴 <𝑧, 0R⟩) ↔ ((𝐴 < 𝐵𝐵 <𝑧, 0R⟩) → 𝐴 <𝑧, 0R⟩)))
12 breq2 3809 . . . 4 (⟨𝑧, 0R⟩ = 𝐶 → (𝐵 <𝑧, 0R⟩ ↔ 𝐵 < 𝐶))
1312anbi2d 452 . . 3 (⟨𝑧, 0R⟩ = 𝐶 → ((𝐴 < 𝐵𝐵 <𝑧, 0R⟩) ↔ (𝐴 < 𝐵𝐵 < 𝐶)))
14 breq2 3809 . . 3 (⟨𝑧, 0R⟩ = 𝐶 → (𝐴 <𝑧, 0R⟩ ↔ 𝐴 < 𝐶))
1513, 14imbi12d 232 . 2 (⟨𝑧, 0R⟩ = 𝐶 → (((𝐴 < 𝐵𝐵 <𝑧, 0R⟩) → 𝐴 <𝑧, 0R⟩) ↔ ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶)))
16 ltresr 7139 . . . . 5 (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝑥 <R 𝑦)
17 ltresr 7139 . . . . 5 (⟨𝑦, 0R⟩ <𝑧, 0R⟩ ↔ 𝑦 <R 𝑧)
18 ltsosr 7073 . . . . . 6 <R Or R
19 ltrelsr 7047 . . . . . 6 <R ⊆ (R × R)
2018, 19sotri 4770 . . . . 5 ((𝑥 <R 𝑦𝑦 <R 𝑧) → 𝑥 <R 𝑧)
2116, 17, 20syl2anb 285 . . . 4 ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) → 𝑥 <R 𝑧)
22 ltresr 7139 . . . 4 (⟨𝑥, 0R⟩ <𝑧, 0R⟩ ↔ 𝑥 <R 𝑧)
2321, 22sylibr 132 . . 3 ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) → ⟨𝑥, 0R⟩ <𝑧, 0R⟩)
2423a1i 9 . 2 ((𝑥R𝑦R𝑧R) → ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ∧ ⟨𝑦, 0R⟩ <𝑧, 0R⟩) → ⟨𝑥, 0R⟩ <𝑧, 0R⟩))
251, 2, 3, 7, 11, 15, 243gencl 2642 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  ⟨cop 3419   class class class wbr 3805  Rcnr 6619  0Rc0r 6620
 Copyright terms: Public domain W3C validator