Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ltxr Structured version   Visualization version   Unicode version

Definition df-ltxr 9698
 Description: Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, is primitive and not necessarily a relation on . (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
df-ltxr
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ltxr
StepHypRef Expression
1 clt 9693 . 2
2 vx . . . . . . 7
32cv 1451 . . . . . 6
4 cr 9556 . . . . . 6
53, 4wcel 1904 . . . . 5
6 vy . . . . . . 7
76cv 1451 . . . . . 6
87, 4wcel 1904 . . . . 5
9 cltrr 9561 . . . . . 6
103, 7, 9wbr 4395 . . . . 5
115, 8, 10w3a 1007 . . . 4
1211, 2, 6copab 4453 . . 3
13 cmnf 9691 . . . . . . 7
1413csn 3959 . . . . . 6
154, 14cun 3388 . . . . 5
16 cpnf 9690 . . . . . 6
1716csn 3959 . . . . 5
1815, 17cxp 4837 . . . 4
1914, 4cxp 4837 . . . 4
2018, 19cun 3388 . . 3
2112, 20cun 3388 . 2
221, 21wceq 1452 1
 Colors of variables: wff setvar class This definition is referenced by:  ltrelxr  9713  ltxrlt  9722  ltxr  11438
 Copyright terms: Public domain W3C validator