Description: Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihglblem.b | |
|
dihglblem.l | |
||
dihglblem.m | |
||
dihglblem.g | |
||
dihglblem.h | |
||
dihglblem.t | |
||
dihglblem.i | |
||
dihglblem.ih | |
||
Assertion | dihglblem3N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihglblem.b | |
|
2 | dihglblem.l | |
|
3 | dihglblem.m | |
|
4 | dihglblem.g | |
|
5 | dihglblem.h | |
|
6 | dihglblem.t | |
|
7 | dihglblem.i | |
|
8 | dihglblem.ih | |
|
9 | simp1 | |
|
10 | simp11l | |
|
11 | 10 | hllatd | |
12 | simp12l | |
|
13 | simp3 | |
|
14 | 12 13 | sseldd | |
15 | simp11r | |
|
16 | 1 5 | lhpbase | |
17 | 15 16 | syl | |
18 | 1 2 3 | latmle2 | |
19 | 11 14 17 18 | syl3anc | |
20 | 19 | 3expia | |
21 | breq1 | |
|
22 | 21 | biimprcd | |
23 | 20 22 | syl6 | |
24 | 23 | rexlimdv | |
25 | 24 | ss2rabdv | |
26 | 6 25 | eqsstrid | |
27 | 1 2 5 7 | dibdmN | |
28 | 27 | 3ad2ant1 | |
29 | 26 28 | sseqtrrd | |
30 | 1 2 3 4 5 6 | dihglblem2aN | |
31 | 30 | 3adant3 | |
32 | 4 5 7 | dibglbN | |
33 | 9 29 31 32 | syl12anc | |
34 | 1 2 3 4 5 6 | dihglblem2N | |
35 | 34 | 3adant2r | |
36 | 35 | fveq2d | |
37 | simpl1 | |
|
38 | 26 | sselda | |
39 | breq1 | |
|
40 | 39 | elrab | |
41 | 38 40 | sylib | |
42 | 1 2 5 8 7 | dihvalb | |
43 | 37 41 42 | syl2anc | |
44 | 43 | iineq2dv | |
45 | 33 36 44 | 3eqtr4rd | |
46 | simp1l | |
|
47 | hlclat | |
|
48 | 46 47 | syl | |
49 | simp2l | |
|
50 | 1 4 | clatglbcl | |
51 | 48 49 50 | syl2anc | |
52 | simp3 | |
|
53 | 1 2 5 8 7 | dihvalb | |
54 | 9 51 52 53 | syl12anc | |
55 | 35 | fveq2d | |
56 | 45 54 55 | 3eqtr2rd | |