Description: The predicate "is a complete lattice". (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isclat.b | |
|
isclat.u | |
||
isclat.g | |
||
Assertion | isclat | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isclat.b | |
|
2 | isclat.u | |
|
3 | isclat.g | |
|
4 | fveq2 | |
|
5 | 4 2 | eqtr4di | |
6 | 5 | dmeqd | |
7 | fveq2 | |
|
8 | 7 1 | eqtr4di | |
9 | 8 | pweqd | |
10 | 6 9 | eqeq12d | |
11 | fveq2 | |
|
12 | 11 3 | eqtr4di | |
13 | 12 | dmeqd | |
14 | 13 9 | eqeq12d | |
15 | 10 14 | anbi12d | |
16 | df-clat | |
|
17 | 15 16 | elrab2 | |