Definition df-bj-lt

Description: Define the standard (strict) order on the extended reals. (Contributed by BJ, 4-Feb-2023)

	Ref	Expression
Assertion	df-bj-lt	$$⊢{<}_R=\left\{x\in \left(\overline{ℝ}\times \overline{ℝ}\right)|\exists y\exists z\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)\right\}\cup \left(\left(\left(\left\{-\infty \right\}\times ℝ\right)\cup \left(ℝ\times \left\{+\infty \right\}\right)\right)\cup \left(\left\{-\infty \right\}\times \left\{+\infty \right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltxr	$$class{<}_R$$
1		vx	$$setvarx$$
2		crrbar	$$class\overline{ℝ}$$
3	2 2	cxp	$$class\left(\overline{ℝ}\times \overline{ℝ}\right)$$
4		vy	$$setvary$$
5		vz	$$setvarz$$
6		c1st	$$class{1}^{st}$$
7	1	cv	$$setvarx$$
8	7 6	cfv	$$class{1}^{st}\left(x\right)$$
9	4	cv	$$setvary$$
10		c0r	$$class{0}_{𝑹}$$
11	9 10	cop	$$class⟨y,0_{𝑹}⟩$$
12	8 11	wceq	$$wff{1}^{st}\left(x\right)=⟨y,0_{𝑹}⟩$$
13		c2nd	$$class{2}^{nd}$$
14	7 13	cfv	$$class{2}^{nd}\left(x\right)$$
15	5	cv	$$setvarz$$
16	15 10	cop	$$class⟨z,0_{𝑹}⟩$$
17	14 16	wceq	$$wff{2}^{nd}\left(x\right)=⟨z,0_{𝑹}⟩$$
18	12 17	wa	$$wff\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)$$
19		cltr	$$class{<}_{𝑹}$$
20	9 15 19	wbr	$$wffy{<}_{𝑹}z$$
21	18 20	wa	$$wff\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)$$
22	21 5	wex	$$wff\exists z\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)$$
23	22 4	wex	$$wff\exists y\exists z\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)$$
24	23 1 3	crab	$$class\left\{x\in \left(\overline{ℝ}\times \overline{ℝ}\right)|\exists y\exists z\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)\right\}$$
25		cminfty	$$class-\infty$$
26	25	csn	$$class\left\{-\infty \right\}$$
27		cr	$$classℝ$$
28	26 27	cxp	$$class\left(\left\{-\infty \right\}\times ℝ\right)$$
29		cpinfty	$$class+\infty$$
30	29	csn	$$class\left\{+\infty \right\}$$
31	27 30	cxp	$$class\left(ℝ\times \left\{+\infty \right\}\right)$$
32	28 31	cun	$$class\left(\left(\left\{-\infty \right\}\times ℝ\right)\cup \left(ℝ\times \left\{+\infty \right\}\right)\right)$$
33	26 30	cxp	$$class\left(\left\{-\infty \right\}\times \left\{+\infty \right\}\right)$$
34	32 33	cun	$$class\left(\left(\left(\left\{-\infty \right\}\times ℝ\right)\cup \left(ℝ\times \left\{+\infty \right\}\right)\right)\cup \left(\left\{-\infty \right\}\times \left\{+\infty \right\}\right)\right)$$
35	24 34	cun	$$class\left(\left\{x\in \left(\overline{ℝ}\times \overline{ℝ}\right)|\exists y\exists z\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)\right\}\cup \left(\left(\left(\left\{-\infty \right\}\times ℝ\right)\cup \left(ℝ\times \left\{+\infty \right\}\right)\right)\cup \left(\left\{-\infty \right\}\times \left\{+\infty \right\}\right)\right)\right)$$
36	0 35	wceq	$$wff{<}_R=\left\{x\in \left(\overline{ℝ}\times \overline{ℝ}\right)|\exists y\exists z\left(\left(1^{st}\left(x\right)=⟨y,0_{𝑹}⟩\wedge 2^{nd}\left(x\right)=⟨z,0_{𝑹}⟩\right)\wedge y{<}_{𝑹}z\right)\right\}\cup \left(\left(\left(\left\{-\infty \right\}\times ℝ\right)\cup \left(ℝ\times \left\{+\infty \right\}\right)\right)\cup \left(\left\{-\infty \right\}\times \left\{+\infty \right\}\right)\right)$$