Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-lt Structured version   Visualization version   GIF version

Definition df-bj-lt 34542
Description: Define the standard (strict) order on the extended reals. (Contributed by BJ, 4-Feb-2023.)
Assertion
Ref Expression
df-bj-lt <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦𝑧(((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-bj-lt
StepHypRef Expression
1 cltxr 34541 . 2 class <ℝ̅
2 vx . . . . . . . . . . 11 setvar 𝑥
32cv 1537 . . . . . . . . . 10 class 𝑥
4 c1st 7662 . . . . . . . . . 10 class 1st
53, 4cfv 6328 . . . . . . . . 9 class (1st𝑥)
6 vy . . . . . . . . . . 11 setvar 𝑦
76cv 1537 . . . . . . . . . 10 class 𝑦
8 c0r 10265 . . . . . . . . . 10 class 0R
97, 8cop 4546 . . . . . . . . 9 class 𝑦, 0R
105, 9wceq 1538 . . . . . . . 8 wff (1st𝑥) = ⟨𝑦, 0R
11 c2nd 7663 . . . . . . . . . 10 class 2nd
123, 11cfv 6328 . . . . . . . . 9 class (2nd𝑥)
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1537 . . . . . . . . . 10 class 𝑧
1514, 8cop 4546 . . . . . . . . 9 class 𝑧, 0R
1612, 15wceq 1538 . . . . . . . 8 wff (2nd𝑥) = ⟨𝑧, 0R
1710, 16wa 399 . . . . . . 7 wff ((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩)
18 cltr 10270 . . . . . . . 8 class <R
197, 14, 18wbr 5039 . . . . . . 7 wff 𝑦 <R 𝑧
2017, 19wa 399 . . . . . 6 wff (((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
2120, 13wex 1781 . . . . 5 wff 𝑧(((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
2221, 6wex 1781 . . . 4 wff 𝑦𝑧(((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
23 crrbar 34528 . . . . 5 class ℝ̅
2423, 23cxp 5526 . . . 4 class (ℝ̅ × ℝ̅)
2522, 2, 24crab 3130 . . 3 class {𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦𝑧(((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)}
26 cminfty 34523 . . . . . . 7 class -∞
2726csn 4540 . . . . . 6 class {-∞}
28 cr 10513 . . . . . 6 class
2927, 28cxp 5526 . . . . 5 class ({-∞} × ℝ)
30 cpinfty 34519 . . . . . . 7 class +∞
3130csn 4540 . . . . . 6 class {+∞}
3228, 31cxp 5526 . . . . 5 class (ℝ × {+∞})
3329, 32cun 3908 . . . 4 class (({-∞} × ℝ) ∪ (ℝ × {+∞}))
3427, 31cxp 5526 . . . 4 class ({-∞} × {+∞})
3533, 34cun 3908 . . 3 class ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞}))
3625, 35cun 3908 . 2 class ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦𝑧(((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
371, 36wceq 1538 1 wff <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦𝑧(((1st𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator