Step | Hyp | Ref
| Expression |
1 | | simpl1 1190 |
. . . 4
β’ (((πΎ β CLat β§ π β π΅ β§ π β π) β§ π¦ β π) β πΎ β CLat) |
2 | | simpl2 1191 |
. . . 4
β’ (((πΎ β CLat β§ π β π΅ β§ π β π) β§ π¦ β π) β π β π΅) |
3 | | simp3 1137 |
. . . . 5
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β π β π) |
4 | 3 | sselda 3983 |
. . . 4
β’ (((πΎ β CLat β§ π β π΅ β§ π β π) β§ π¦ β π) β π¦ β π) |
5 | | clatglb.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
6 | | clatglb.l |
. . . . 5
β’ β€ =
(leβπΎ) |
7 | | clatglb.g |
. . . . 5
β’ πΊ = (glbβπΎ) |
8 | 5, 6, 7 | clatglble 18475 |
. . . 4
β’ ((πΎ β CLat β§ π β π΅ β§ π¦ β π) β (πΊβπ) β€ π¦) |
9 | 1, 2, 4, 8 | syl3anc 1370 |
. . 3
β’ (((πΎ β CLat β§ π β π΅ β§ π β π) β§ π¦ β π) β (πΊβπ) β€ π¦) |
10 | 9 | ralrimiva 3145 |
. 2
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β βπ¦ β π (πΊβπ) β€ π¦) |
11 | | simp1 1135 |
. . 3
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β πΎ β CLat) |
12 | 5, 7 | clatglbcl 18463 |
. . . 4
β’ ((πΎ β CLat β§ π β π΅) β (πΊβπ) β π΅) |
13 | 12 | 3adant3 1131 |
. . 3
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πΊβπ) β π΅) |
14 | | sstr 3991 |
. . . . 5
β’ ((π β π β§ π β π΅) β π β π΅) |
15 | 14 | ancoms 458 |
. . . 4
β’ ((π β π΅ β§ π β π) β π β π΅) |
16 | 15 | 3adant1 1129 |
. . 3
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β π β π΅) |
17 | 5, 6, 7 | clatleglb 18476 |
. . 3
β’ ((πΎ β CLat β§ (πΊβπ) β π΅ β§ π β π΅) β ((πΊβπ) β€ (πΊβπ) β βπ¦ β π (πΊβπ) β€ π¦)) |
18 | 11, 13, 16, 17 | syl3anc 1370 |
. 2
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β ((πΊβπ) β€ (πΊβπ) β βπ¦ β π (πΊβπ) β€ π¦)) |
19 | 10, 18 | mpbird 256 |
1
β’ ((πΎ β CLat β§ π β π΅ β§ π β π) β (πΊβπ) β€ (πΊβπ)) |