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	⊢ <ℝ̅ = ( { 𝑥 ∈ ( ℝ̅ × ℝ̅ ) ∣ ∃ 𝑦 ∃ 𝑧 ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 ) } ∪ ( ( ( { -∞ } × ℝ ) ∪ ( ℝ × { +∞ } ) ) ∪ ( { -∞ } × { +∞ } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltxr	⊢ <ℝ̅
1		vx	⊢ 𝑥
2		crrbar	⊢ ℝ̅
3	2 2	cxp	⊢ ( ℝ̅ × ℝ̅ )
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6		c1st	⊢ 1st
7	1	cv	⊢ 𝑥
8	7 6	cfv	⊢ ( 1st ‘ 𝑥 )
9	4	cv	⊢ 𝑦
10		c0r	⊢ 0R
11	9 10	cop	⊢ ⟨ 𝑦 , 0R ⟩
12	8 11	wceq	⊢ ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩
13		c2nd	⊢ 2nd
14	7 13	cfv	⊢ ( 2nd ‘ 𝑥 )
15	5	cv	⊢ 𝑧
16	15 10	cop	⊢ ⟨ 𝑧 , 0R ⟩
17	14 16	wceq	⊢ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩
18	12 17	wa	⊢ ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ )
19		cltr	⊢ <R
20	9 15 19	wbr	⊢ 𝑦 <R 𝑧
21	18 20	wa	⊢ ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 )
22	21 5	wex	⊢ ∃ 𝑧 ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 )
23	22 4	wex	⊢ ∃ 𝑦 ∃ 𝑧 ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 )
24	23 1 3	crab	⊢ { 𝑥 ∈ ( ℝ̅ × ℝ̅ ) ∣ ∃ 𝑦 ∃ 𝑧 ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 ) }
25		cminfty	⊢ -∞
26	25	csn	⊢ { -∞ }
27		cr	⊢ ℝ
28	26 27	cxp	⊢ ( { -∞ } × ℝ )
29		cpinfty	⊢ +∞
30	29	csn	⊢ { +∞ }
31	27 30	cxp	⊢ ( ℝ × { +∞ } )
32	28 31	cun	⊢ ( ( { -∞ } × ℝ ) ∪ ( ℝ × { +∞ } ) )
33	26 30	cxp	⊢ ( { -∞ } × { +∞ } )
34	32 33	cun	⊢ ( ( ( { -∞ } × ℝ ) ∪ ( ℝ × { +∞ } ) ) ∪ ( { -∞ } × { +∞ } ) )
35	24 34	cun	⊢ ( { 𝑥 ∈ ( ℝ̅ × ℝ̅ ) ∣ ∃ 𝑦 ∃ 𝑧 ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 ) } ∪ ( ( ( { -∞ } × ℝ ) ∪ ( ℝ × { +∞ } ) ) ∪ ( { -∞ } × { +∞ } ) ) )
36	0 35	wceq	⊢ <ℝ̅ = ( { 𝑥 ∈ ( ℝ̅ × ℝ̅ ) ∣ ∃ 𝑦 ∃ 𝑧 ( ( ( 1st ‘ 𝑥 ) = ⟨ 𝑦 , 0R ⟩ ∧ ( 2nd ‘ 𝑥 ) = ⟨ 𝑧 , 0R ⟩ ) ∧ 𝑦 <R 𝑧 ) } ∪ ( ( ( { -∞ } × ℝ ) ∪ ( ℝ × { +∞ } ) ) ∪ ( { -∞ } × { +∞ } ) ) )