Metamath Proof Explorer

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 
|- . /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltxr 
 |-
1 vx 
 |-  x
2 crrbar 
 |-  RRbar
3 2 2 cxp 
 |-  ( RRbar X. RRbar )
4 vy 
 |-  y
5 vz 
 |-  z
6 c1st 
 |-  1st
7 1 cv 
 |-  x
8 7 6 cfv 
 |-  ( 1st ` x )
9 4 cv 
 |-  y
10 c0r 
 |-  0R
11 9 10 cop 
 |-  <. y , 0R >.
12 8 11 wceq 
 |-  ( 1st ` x ) = <. y , 0R >.
13 c2nd 
 |-  2nd
14 7 13 cfv 
 |-  ( 2nd ` x )
15 5 cv 
 |-  z
16 15 10 cop 
 |-  <. z , 0R >.
17 14 16 wceq 
 |-  ( 2nd ` x ) = <. z , 0R >.
18 12 17 wa 
 |-  ( ( 1st ` x ) = <. y , 0R >. /\ ( 2nd ` x ) = <. z , 0R >. )
19 cltr 
 |-
20 9 15 19 wbr 
 |-  y
21 18 20 wa 
 |-  ( ( ( 1st ` x ) = <. y , 0R >. /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y
22 21 5 wex 
 |-  E. z ( ( ( 1st ` x ) = <. y , 0R >. /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y
23 22 4 wex 
 |-  E. y E. z ( ( ( 1st ` x ) = <. y , 0R >. /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y
24 23 1 3 crab 
 |-  { x e. ( RRbar X. RRbar ) | E. y E. z ( ( ( 1st ` x ) = <. y , 0R >. /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y
25 cminfty 
 |-  minfty
26 25 csn 
 |-  { minfty }
27 cr 
 |-  RR
28 26 27 cxp 
 |-  ( { minfty } X. RR )
29 cpinfty 
 |-  pinfty
30 29 csn 
 |-  { pinfty }
31 27 30 cxp 
 |-  ( RR X. { pinfty } )
32 28 31 cun 
 |-  ( ( { minfty } X. RR ) u. ( RR X. { pinfty } ) )
33 26 30 cxp 
 |-  ( { minfty } X. { pinfty } )
34 32 33 cun 
 |-  ( ( ( { minfty } X. RR ) u. ( RR X. { pinfty } ) ) u. ( { minfty } X. { pinfty } ) )
35 24 34 cun 
 |-  ( { x e. ( RRbar X. RRbar ) | E. y E. z ( ( ( 1st ` x ) = <. y , 0R >. /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y
36 0 35 wceq 
 |-  . /\ ( 2nd ` x ) = <. z , 0R >. ) /\ y