Metamath Proof Explorer

Definition df-lt

Description: Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr . (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-lt 
|- . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrr 
 |-
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 cr 
 |-  RR
5 3 4 wcel 
 |-  x e. RR
6 2 cv 
 |-  y
7 6 4 wcel 
 |-  y e. RR
8 5 7 wa 
 |-  ( x e. RR /\ y e. RR )
9 vz 
 |-  z
10 vw 
 |-  w
11 9 cv 
 |-  z
12 c0r 
 |-  0R
13 11 12 cop 
 |-  <. z , 0R >.
14 3 13 wceq 
 |-  x = <. z , 0R >.
15 10 cv 
 |-  w
16 15 12 cop 
 |-  <. w , 0R >.
17 6 16 wceq 
 |-  y = <. w , 0R >.
18 14 17 wa 
 |-  ( x = <. z , 0R >. /\ y = <. w , 0R >. )
19 cltr 
 |-
20 11 15 19 wbr 
 |-  z
21 18 20 wa 
 |-  ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
22 21 10 wex 
 |-  E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
23 22 9 wex 
 |-  E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
24 8 23 wa 
 |-  ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
25 24 1 2 copab 
 |-  { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
26 0 25 wceq 
 |-  . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z