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

Definition df-latalg 25182
 Description: Algebraic definition of a lattice. is called the join of the lattice (and is denoted by in textbooks) , is called the meet (and is denoted by in textbooks). (Contributed by FL, 11-Dec-2009.)
Assertion
Ref Expression
df-latalg
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-latalg
StepHypRef Expression
1 clatalg 25181 . 2
2 vt . . . . . . . 8
32cv 1622 . . . . . . 7
43, 3cxp 4687 . . . . . 6
5 vj . . . . . . 7
65cv 1622 . . . . . 6
74, 3, 6wf 5251 . . . . 5
8 vm . . . . . . 7
98cv 1622 . . . . . 6
104, 3, 9wf 5251 . . . . 5
11 vx . . . . . . . . . . 11
1211cv 1622 . . . . . . . . . 10
13 vy . . . . . . . . . . 11
1413cv 1622 . . . . . . . . . 10
1512, 14, 6co 5858 . . . . . . . . 9
1614, 12, 6co 5858 . . . . . . . . 9
1715, 16wceq 1623 . . . . . . . 8
1812, 14, 9co 5858 . . . . . . . . 9
1914, 12, 9co 5858 . . . . . . . . 9
2018, 19wceq 1623 . . . . . . . 8
2112, 15, 9co 5858 . . . . . . . . . 10
2221, 12wceq 1623 . . . . . . . . 9
2312, 18, 6co 5858 . . . . . . . . . 10
2423, 12wceq 1623 . . . . . . . . 9
25 vz . . . . . . . . . . . . . . 15
2625cv 1622 . . . . . . . . . . . . . 14
2714, 26, 9co 5858 . . . . . . . . . . . . 13
2812, 27, 9co 5858 . . . . . . . . . . . 12
2918, 26, 9co 5858 . . . . . . . . . . . 12
3028, 29wceq 1623 . . . . . . . . . . 11
3114, 26, 6co 5858 . . . . . . . . . . . . 13
3212, 31, 6co 5858 . . . . . . . . . . . 12
3315, 26, 6co 5858 . . . . . . . . . . . 12
3432, 33wceq 1623 . . . . . . . . . . 11
3530, 34wa 358 . . . . . . . . . 10
3635, 25, 3wral 2543 . . . . . . . . 9
3722, 24, 36w3a 934 . . . . . . . 8
3817, 20, 37w3a 934 . . . . . . 7
3938, 13, 3wral 2543 . . . . . 6
4039, 11, 3wral 2543 . . . . 5
417, 10, 40w3a 934 . . . 4
4241, 2wex 1528 . . 3
4342, 5, 8copab 4076 . 2
441, 43wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  islatalg  25183
 Copyright terms: Public domain W3C validator