Step | Hyp | Ref
| Expression |
1 | | dihglbc.h |
. . . 4
|
2 | | dihglbc.i |
. . . 4
|
3 | 1, 2 | dihvalrel 36568 |
. . 3
|
4 | 3 | 3ad2ant1 1082 |
. 2
|
5 | | simp2r 1088 |
. . . . . 6
|
6 | | n0 3931 |
. . . . . 6
|
7 | 5, 6 | sylib 208 |
. . . . 5
|
8 | | simpr 477 |
. . . . . . . 8
|
9 | | simpl1 1064 |
. . . . . . . . 9
|
10 | 1, 2 | dihvalrel 36568 |
. . . . . . . . 9
|
11 | 9, 10 | syl 17 |
. . . . . . . 8
|
12 | 8, 11 | jca 554 |
. . . . . . 7
|
13 | 12 | ex 450 |
. . . . . 6
|
14 | 13 | eximdv 1846 |
. . . . 5
|
15 | 7, 14 | mpd 15 |
. . . 4
|
16 | | df-rex 2918 |
. . . 4
|
17 | 15, 16 | sylibr 224 |
. . 3
|
18 | | reliin 5240 |
. . 3
|
19 | 17, 18 | syl 17 |
. 2
|
20 | | id 22 |
. 2
|
21 | | simp1 1061 |
. . . . 5
|
22 | | simp1l 1085 |
. . . . . . 7
|
23 | | hlclat 34645 |
. . . . . . 7
|
24 | 22, 23 | syl 17 |
. . . . . 6
|
25 | | simp2l 1087 |
. . . . . 6
|
26 | | dihglbc.b |
. . . . . . 7
|
27 | | dihglbc.g |
. . . . . . 7
|
28 | 26, 27 | clatglbcl 17114 |
. . . . . 6
|
29 | 24, 25, 28 | syl2anc 693 |
. . . . 5
|
30 | | simp3 1063 |
. . . . 5
|
31 | | dihglbc.l |
. . . . . 6
|
32 | | dihglbcpre.j |
. . . . . 6
|
33 | | dihglbcpre.m |
. . . . . 6
|
34 | | dihglbcpre.a |
. . . . . 6
|
35 | 26, 31, 32, 33, 34, 1 | lhpmcvr2 35310 |
. . . . 5
|
36 | 21, 29, 30, 35 | syl12anc 1324 |
. . . 4
|
37 | | simpl1 1064 |
. . . . . . . . 9
|
38 | 29 | adantr 481 |
. . . . . . . . 9
|
39 | | simpl3 1066 |
. . . . . . . . 9
|
40 | | simpr 477 |
. . . . . . . . 9
|
41 | | dihglbcpre.p |
. . . . . . . . . 10
|
42 | | dihglbcpre.t |
. . . . . . . . . 10
|
43 | | dihglbcpre.r |
. . . . . . . . . 10
|
44 | | dihglbcpre.e |
. . . . . . . . . 10
|
45 | | dihglbcpre.f |
. . . . . . . . . 10
|
46 | | vex 3203 |
. . . . . . . . . 10
|
47 | | vex 3203 |
. . . . . . . . . 10
|
48 | 26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47 | dihopelvalc 36538 |
. . . . . . . . 9
|
49 | 37, 38, 39, 40, 48 | syl121anc 1331 |
. . . . . . . 8
|
50 | | simpl2r 1115 |
. . . . . . . . . . 11
|
51 | | r19.28zv 4066 |
. . . . . . . . . . 11
|
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
|
53 | | simp11 1091 |
. . . . . . . . . . . . 13
|
54 | | simp12l 1174 |
. . . . . . . . . . . . . 14
|
55 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
56 | 54, 55 | sseldd 3604 |
. . . . . . . . . . . . 13
|
57 | | simp13 1093 |
. . . . . . . . . . . . . 14
|
58 | | simp11l 1172 |
. . . . . . . . . . . . . . . . 17
|
59 | 58, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
|
60 | 26, 31, 27 | clatglble 17125 |
. . . . . . . . . . . . . . . 16
|
61 | 59, 54, 55, 60 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
62 | | hllat 34650 |
. . . . . . . . . . . . . . . . 17
|
63 | 58, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
|
64 | 29 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
65 | | simp11r 1173 |
. . . . . . . . . . . . . . . . 17
|
66 | 26, 1 | lhpbase 35284 |
. . . . . . . . . . . . . . . . 17
|
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
|
68 | 26, 31 | lattr 17056 |
. . . . . . . . . . . . . . . 16
|
69 | 63, 64, 56, 67, 68 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
|
70 | 61, 69 | mpand 711 |
. . . . . . . . . . . . . 14
|
71 | 57, 70 | mtod 189 |
. . . . . . . . . . . . 13
|
72 | | simp2l 1087 |
. . . . . . . . . . . . 13
|
73 | | simp2ll 1128 |
. . . . . . . . . . . . . . 15
|
74 | 26, 34 | atbase 34576 |
. . . . . . . . . . . . . . . . 17
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . 16
|
76 | 26, 33 | latmcl 17052 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 63, 64, 67, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
78 | 26, 31, 32 | latlej1 17060 |
. . . . . . . . . . . . . . . . . 18
|
79 | 63, 75, 77, 78 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
80 | | simp2r 1088 |
. . . . . . . . . . . . . . . . 17
|
81 | 79, 80 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
82 | 26, 31, 63, 75, 64, 56, 81, 61 | lattrd 17058 |
. . . . . . . . . . . . . . 15
|
83 | 26, 31, 32, 33, 34 | atmod3i1 35150 |
. . . . . . . . . . . . . . 15
|
84 | 58, 73, 56, 67, 82, 83 | syl131anc 1339 |
. . . . . . . . . . . . . 14
|
85 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
86 | 31, 32, 85, 34, 1 | lhpjat2 35307 |
. . . . . . . . . . . . . . . 16
|
87 | 53, 72, 86 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
88 | 87 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
89 | | hlol 34648 |
. . . . . . . . . . . . . . . 16
|
90 | 58, 89 | syl 17 |
. . . . . . . . . . . . . . 15
|
91 | 26, 33, 85 | olm11 34514 |
. . . . . . . . . . . . . . 15
|
92 | 90, 56, 91 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
93 | 84, 88, 92 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
94 | 26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47 | dihopelvalc 36538 |
. . . . . . . . . . . . 13
|
95 | 53, 56, 71, 72, 93, 94 | syl122anc 1335 |
. . . . . . . . . . . 12
|
96 | 95 | 3expa 1265 |
. . . . . . . . . . 11
|
97 | 96 | ralbidva 2985 |
. . . . . . . . . 10
|
98 | | simp11l 1172 |
. . . . . . . . . . . . . 14
|
99 | 98, 23 | syl 17 |
. . . . . . . . . . . . 13
|
100 | | simp11 1091 |
. . . . . . . . . . . . . 14
|
101 | | simp3l 1089 |
. . . . . . . . . . . . . . 15
|
102 | | simp3r 1090 |
. . . . . . . . . . . . . . . . 17
|
103 | 31, 34, 1, 41 | lhpocnel2 35305 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 100, 103 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
105 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . 18
|
106 | 31, 34, 1, 42, 45 | ltrniotacl 35867 |
. . . . . . . . . . . . . . . . . 18
|
107 | 100, 104,
105, 106 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
108 | 1, 42, 44 | tendocl 36055 |
. . . . . . . . . . . . . . . . 17
|
109 | 100, 102,
107, 108 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
110 | 1, 42 | ltrncnv 35432 |
. . . . . . . . . . . . . . . 16
|
111 | 100, 109,
110 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
112 | 1, 42 | ltrnco 36007 |
. . . . . . . . . . . . . . 15
|
113 | 100, 101,
111, 112 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
114 | 26, 1, 42, 43 | trlcl 35451 |
. . . . . . . . . . . . . 14
|
115 | 100, 113,
114 | syl2anc 693 |
. . . . . . . . . . . . 13
|
116 | | simp12l 1174 |
. . . . . . . . . . . . 13
|
117 | 26, 31, 27 | clatleglb 17126 |
. . . . . . . . . . . . 13
|
118 | 99, 115, 116, 117 | syl3anc 1326 |
. . . . . . . . . . . 12
|
119 | 118 | 3expa 1265 |
. . . . . . . . . . 11
|
120 | 119 | pm5.32da 673 |
. . . . . . . . . 10
|
121 | 52, 97, 120 | 3bitr4rd 301 |
. . . . . . . . 9
|
122 | | opex 4932 |
. . . . . . . . . 10
|
123 | | eliin 4525 |
. . . . . . . . . 10
|
124 | 122, 123 | ax-mp 5 |
. . . . . . . . 9
|
125 | 121, 124 | syl6bbr 278 |
. . . . . . . 8
|
126 | 49, 125 | bitrd 268 |
. . . . . . 7
|
127 | 126 | exp44 641 |
. . . . . 6
|
128 | 127 | imp4a 614 |
. . . . 5
|
129 | 128 | rexlimdv 3030 |
. . . 4
|
130 | 36, 129 | mpd 15 |
. . 3
|
131 | 130 | eqrelrdv2 5219 |
. 2
|
132 | 4, 19, 20, 131 | syl21anc 1325 |
1
|