Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tofld Unicode version

Definition df-tofld 25440
 Description: Definition of a totally ordered field. Experimental. (Contributed by FL, 27-Jun-2011.)
Assertion
Ref Expression
df-tofld GId
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-tofld
StepHypRef Expression
1 ctofld 25439 . 2
2 vg . . . . . . 7
32cv 1622 . . . . . 6
4 vh . . . . . . 7
54cv 1622 . . . . . 6
63, 5cop 3643 . . . . 5
7 cfld 21080 . . . . 5
86, 7wcel 1684 . . . 4
9 vr . . . . . . 7
109cv 1622 . . . . . 6
11 ctsr 14302 . . . . . 6
1210, 11wcel 1684 . . . . 5
1310cuni 3827 . . . . . . 7
1413cuni 3827 . . . . . 6
153crn 4690 . . . . . 6
1614, 15wceq 1623 . . . . 5
1712, 16wa 358 . . . 4
18 vx . . . . . . . . . . 11
1918cv 1622 . . . . . . . . . 10
20 vy . . . . . . . . . . 11
2120cv 1622 . . . . . . . . . 10
2219, 21, 10wbr 4023 . . . . . . . . 9
23 vz . . . . . . . . . . . 12
2423cv 1622 . . . . . . . . . . 11
2519, 24, 3co 5858 . . . . . . . . . 10
2621, 24, 3co 5858 . . . . . . . . . 10
2725, 26, 10wbr 4023 . . . . . . . . 9
2822, 27wi 4 . . . . . . . 8
29 cgi 20854 . . . . . . . . . . 11 GId
303, 29cfv 5255 . . . . . . . . . 10 GId
3130, 24, 10wbr 4023 . . . . . . . . 9 GId
3219, 24, 5co 5858 . . . . . . . . . 10
3321, 24, 5co 5858 . . . . . . . . . 10
3432, 33, 10wbr 4023 . . . . . . . . 9
3531, 34wi 4 . . . . . . . 8 GId
3628, 35wa 358 . . . . . . 7 GId
3736, 23, 14wral 2543 . . . . . 6 GId
3837, 20, 14wral 2543 . . . . 5 GId
3938, 18, 14wral 2543 . . . 4 GId
408, 17, 39w3a 934 . . 3 GId
4140, 2, 4, 9coprab 5859 . 2 GId
421, 41wceq 1623 1 GId
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator