Definition df-bj-lt 36118

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 36117	. 2 class <ℝ̅
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1540	. . . . . . . . . 10 class 𝑥
4		c1st 7972	. . . . . . . . . 10 class 1st
5	3, 4	cfv 6543	. . . . . . . . 9 class (1st ‘𝑥)
6		vy	. . . . . . . . . . 11 setvar 𝑦
7	6	cv 1540	. . . . . . . . . 10 class 𝑦
8		c0r 10860	. . . . . . . . . 10 class 0R
9	7, 8	cop 4634	. . . . . . . . 9 class ⟨𝑦, 0R⟩
10	5, 9	wceq 1541	. . . . . . . 8 wff (1st ‘𝑥) = ⟨𝑦, 0R⟩
11		c2nd 7973	. . . . . . . . . 10 class 2nd
12	3, 11	cfv 6543	. . . . . . . . 9 class (2nd ‘𝑥)
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1540	. . . . . . . . . 10 class 𝑧
15	14, 8	cop 4634	. . . . . . . . 9 class ⟨𝑧, 0R⟩
16	12, 15	wceq 1541	. . . . . . . 8 wff (2nd ‘𝑥) = ⟨𝑧, 0R⟩
17	10, 16	wa 396	. . . . . . 7 wff ((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩)
18		cltr 10865	. . . . . . . 8 class <R
19	7, 14, 18	wbr 5148	. . . . . . 7 wff 𝑦 <R 𝑧
20	17, 19	wa 396	. . . . . 6 wff (((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
21	20, 13	wex 1781	. . . . 5 wff ∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
22	21, 6	wex 1781	. . . 4 wff ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)
23		crrbar 36104	. . . . 5 class ℝ̅
24	23, 23	cxp 5674	. . . 4 class (ℝ̅ × ℝ̅)
25	22, 2, 24	crab 3432	. . 3 class {𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)}
26		cminfty 36099	. . . . . . 7 class -∞
27	26	csn 4628	. . . . . 6 class {-∞}
28		cr 11108	. . . . . 6 class ℝ
29	27, 28	cxp 5674	. . . . 5 class ({-∞} × ℝ)
30		cpinfty 36095	. . . . . . 7 class +∞
31	30	csn 4628	. . . . . 6 class {+∞}
32	28, 31	cxp 5674	. . . . 5 class (ℝ × {+∞})
33	29, 32	cun 3946	. . . 4 class (({-∞} × ℝ) ∪ (ℝ × {+∞}))
34	27, 31	cxp 5674	. . . 4 class ({-∞} × {+∞})
35	33, 34	cun 3946	. . 3 class ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞}))
36	25, 35	cun 3946	. 2 class ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
37	1, 36	wceq 1541	1 wff <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))

This definition is referenced by: (None)