Step | Hyp | Ref
| Expression |
1 | | dfin5 3582 |
. . . 4
|
2 | | sseqin2 3817 |
. . . . 5
|
3 | 2 | biimpi 206 |
. . . 4
|
4 | 1, 3 | syl5reqr 2671 |
. . 3
|
5 | 4 | fveq2d 6195 |
. 2
|
6 | | glbcon.b |
. . . 4
|
7 | | eqid 2622 |
. . . 4
|
8 | | glbcon.g |
. . . 4
|
9 | | biid 251 |
. . . 4
|
10 | | id 22 |
. . . 4
|
11 | | ssrab2 3687 |
. . . . 5
|
12 | 11 | a1i 11 |
. . . 4
|
13 | 6, 7, 8, 9, 10, 12 | glbval 16997 |
. . 3
|
14 | | hlop 34649 |
. . . 4
|
15 | | hlclat 34645 |
. . . . . . 7
|
16 | 6, 8 | clatglbcl 17114 |
. . . . . . 7
|
17 | 15, 11, 16 | sylancl 694 |
. . . . . 6
|
18 | 13, 17 | eqeltrrd 2702 |
. . . . 5
|
19 | | fvex 6201 |
. . . . . . 7
|
20 | 6, 19 | eqeltri 2697 |
. . . . . 6
|
21 | 20 | riotaclbBAD 34241 |
. . . . 5
|
22 | 18, 21 | sylibr 224 |
. . . 4
|
23 | | glbcon.o |
. . . . 5
|
24 | | breq1 4656 |
. . . . . . 7
|
25 | 24 | ralbidv 2986 |
. . . . . 6
|
26 | | breq2 4657 |
. . . . . . . 8
|
27 | 26 | imbi2d 330 |
. . . . . . 7
|
28 | 27 | ralbidv 2986 |
. . . . . 6
|
29 | 25, 28 | anbi12d 747 |
. . . . 5
|
30 | 6, 23, 29 | riotaocN 34496 |
. . . 4
|
31 | 14, 22, 30 | syl2anc 693 |
. . 3
|
32 | 14 | ad2antrr 762 |
. . . . . . . . . . 11
|
33 | 6, 23 | opoccl 34481 |
. . . . . . . . . . 11
|
34 | 32, 33 | sylancom 701 |
. . . . . . . . . 10
|
35 | 14 | ad2antrr 762 |
. . . . . . . . . . . 12
|
36 | 6, 23 | opoccl 34481 |
. . . . . . . . . . . 12
|
37 | 35, 36 | sylancom 701 |
. . . . . . . . . . 11
|
38 | 6, 23 | opococ 34482 |
. . . . . . . . . . . . 13
|
39 | 35, 38 | sylancom 701 |
. . . . . . . . . . . 12
|
40 | 39 | eqcomd 2628 |
. . . . . . . . . . 11
|
41 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
42 | 41 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
43 | 42 | rspcev 3309 |
. . . . . . . . . . 11
|
44 | 37, 40, 43 | syl2anc 693 |
. . . . . . . . . 10
|
45 | | eleq1 2689 |
. . . . . . . . . . . 12
|
46 | | breq2 4657 |
. . . . . . . . . . . 12
|
47 | 45, 46 | imbi12d 334 |
. . . . . . . . . . 11
|
48 | 47 | adantl 482 |
. . . . . . . . . 10
|
49 | 34, 44, 48 | ralxfrd 4879 |
. . . . . . . . 9
|
50 | | simpr 477 |
. . . . . . . . . . . 12
|
51 | | simplr 792 |
. . . . . . . . . . . 12
|
52 | 6, 7, 23 | oplecon3b 34487 |
. . . . . . . . . . . 12
|
53 | 32, 50, 51, 52 | syl3anc 1326 |
. . . . . . . . . . 11
|
54 | 53 | imbi2d 330 |
. . . . . . . . . 10
|
55 | 54 | ralbidva 2985 |
. . . . . . . . 9
|
56 | 49, 55 | bitr4d 271 |
. . . . . . . 8
|
57 | | eleq1 2689 |
. . . . . . . . 9
|
58 | 57 | ralrab 3368 |
. . . . . . . 8
|
59 | | fveq2 6191 |
. . . . . . . . . 10
|
60 | 59 | eleq1d 2686 |
. . . . . . . . 9
|
61 | 60 | ralrab 3368 |
. . . . . . . 8
|
62 | 56, 58, 61 | 3bitr4g 303 |
. . . . . . 7
|
63 | 14 | ad2antrr 762 |
. . . . . . . . . 10
|
64 | 6, 23 | opoccl 34481 |
. . . . . . . . . 10
|
65 | 63, 64 | sylancom 701 |
. . . . . . . . 9
|
66 | 14 | ad2antrr 762 |
. . . . . . . . . . 11
|
67 | 6, 23 | opoccl 34481 |
. . . . . . . . . . 11
|
68 | 66, 67 | sylancom 701 |
. . . . . . . . . 10
|
69 | 6, 23 | opococ 34482 |
. . . . . . . . . . . 12
|
70 | 66, 69 | sylancom 701 |
. . . . . . . . . . 11
|
71 | 70 | eqcomd 2628 |
. . . . . . . . . 10
|
72 | | fveq2 6191 |
. . . . . . . . . . . 12
|
73 | 72 | eqeq2d 2632 |
. . . . . . . . . . 11
|
74 | 73 | rspcev 3309 |
. . . . . . . . . 10
|
75 | 68, 71, 74 | syl2anc 693 |
. . . . . . . . 9
|
76 | | breq1 4656 |
. . . . . . . . . . . 12
|
77 | 76 | ralbidv 2986 |
. . . . . . . . . . 11
|
78 | | breq1 4656 |
. . . . . . . . . . 11
|
79 | 77, 78 | imbi12d 334 |
. . . . . . . . . 10
|
80 | 79 | adantl 482 |
. . . . . . . . 9
|
81 | 65, 75, 80 | ralxfrd 4879 |
. . . . . . . 8
|
82 | 14 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
83 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
84 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
85 | 6, 7, 23 | oplecon3b 34487 |
. . . . . . . . . . . . . . 15
|
86 | 82, 83, 84, 85 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
87 | 86 | imbi2d 330 |
. . . . . . . . . . . . 13
|
88 | 87 | ralbidva 2985 |
. . . . . . . . . . . 12
|
89 | 82, 33 | sylancom 701 |
. . . . . . . . . . . . 13
|
90 | 14 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
91 | 90, 36 | sylancom 701 |
. . . . . . . . . . . . . 14
|
92 | 90, 38 | sylancom 701 |
. . . . . . . . . . . . . . 15
|
93 | 92 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
94 | 91, 93, 43 | syl2anc 693 |
. . . . . . . . . . . . 13
|
95 | | breq2 4657 |
. . . . . . . . . . . . . . 15
|
96 | 45, 95 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
97 | 96 | adantl 482 |
. . . . . . . . . . . . 13
|
98 | 89, 94, 97 | ralxfrd 4879 |
. . . . . . . . . . . 12
|
99 | 88, 98 | bitr4d 271 |
. . . . . . . . . . 11
|
100 | 60 | ralrab 3368 |
. . . . . . . . . . 11
|
101 | 57 | ralrab 3368 |
. . . . . . . . . . 11
|
102 | 99, 100, 101 | 3bitr4g 303 |
. . . . . . . . . 10
|
103 | | simplr 792 |
. . . . . . . . . . 11
|
104 | | simpr 477 |
. . . . . . . . . . 11
|
105 | 6, 7, 23 | oplecon3b 34487 |
. . . . . . . . . . 11
|
106 | 63, 103, 104, 105 | syl3anc 1326 |
. . . . . . . . . 10
|
107 | 102, 106 | imbi12d 334 |
. . . . . . . . 9
|
108 | 107 | ralbidva 2985 |
. . . . . . . 8
|
109 | 81, 108 | bitr4d 271 |
. . . . . . 7
|
110 | 62, 109 | anbi12d 747 |
. . . . . 6
|
111 | 110 | riotabidva 6627 |
. . . . 5
|
112 | | ssrab2 3687 |
. . . . . 6
|
113 | | glbcon.u |
. . . . . . 7
|
114 | | biid 251 |
. . . . . . 7
|
115 | | simpl 473 |
. . . . . . 7
|
116 | | simpr 477 |
. . . . . . 7
|
117 | 6, 7, 113, 114, 115, 116 | lubval 16984 |
. . . . . 6
|
118 | 112, 117 | mpan2 707 |
. . . . 5
|
119 | 111, 118 | eqtr4d 2659 |
. . . 4
|
120 | 119 | fveq2d 6195 |
. . 3
|
121 | 13, 31, 120 | 3eqtrd 2660 |
. 2
|
122 | 5, 121 | sylan9eqr 2678 |
1
|