Definition df-bj-lt 35340

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

Step	Hyp	Ref	Expression
1		cltxr 35339	. 2 class <ℝ̅
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1538	. . . . . . . . . 10 class 𝑥
4		c1st 7802	. . . . . . . . . 10 class 1st
5	3, 4	cfv 6418	. . . . . . . . 9 class (1st ‘𝑥)
6		vy	. . . . . . . . . . 11 setvar 𝑦
7	6	cv 1538	. . . . . . . . . 10 class 𝑦
8		c0r 10553	. . . . . . . . . 10 class 0R
9	7, 8	cop 4564	. . . . . . . . 9 class ⟨𝑦, 0R⟩
10	5, 9	wceq 1539	. . . . . . . 8 wff (1st ‘𝑥) = ⟨𝑦, 0R⟩
11		c2nd 7803	. . . . . . . . . 10 class 2nd
12	3, 11	cfv 6418	. . . . . . . . 9 class (2nd ‘𝑥)
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1538	. . . . . . . . . 10 class 𝑧
15	14, 8	cop 4564	. . . . . . . . 9 class ⟨𝑧, 0R⟩
16	12, 15	wceq 1539	. . . . . . . 8 wff (2nd ‘𝑥) = ⟨𝑧, 0R⟩
17	10, 16	wa 395	. . . . . . 7 wff ((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩)
18		cltr 10558	. . . . . . . 8 class <R
19	7, 14, 18	wbr 5070	. . . . . . 7 wff 𝑦 <R 𝑧
20	17, 19	wa 395	. . . . . 6 wff (((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
21	20, 13	wex 1783	. . . . 5 wff ∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
22	21, 6	wex 1783	. . . 4 wff ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
23		crrbar 35326	. . . . 5 class ℝ̅
24	23, 23	cxp 5578	. . . 4 class (ℝ̅ × ℝ̅)
25	22, 2, 24	crab 3067	. . 3 class {𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)}
26		cminfty 35321	. . . . . . 7 class -∞
27	26	csn 4558	. . . . . 6 class {-∞}
28		cr 10801	. . . . . 6 class ℝ
29	27, 28	cxp 5578	. . . . 5 class ({-∞} × ℝ)
30		cpinfty 35317	. . . . . . 7 class +∞
31	30	csn 4558	. . . . . 6 class {+∞}
32	28, 31	cxp 5578	. . . . 5 class (ℝ × {+∞})
33	29, 32	cun 3881	. . . 4 class (({-∞} × ℝ) ∪ (ℝ × {+∞}))
34	27, 31	cxp 5578	. . . 4 class ({-∞} × {+∞})
35	33, 34	cun 3881	. . 3 class ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞}))
36	25, 35	cun 3881	. 2 class ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
37	1, 36	wceq 1539	1 wff <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))

This definition is referenced by: (None)