Step | Hyp | Ref
| Expression |
1 | | ssrab 3231 |
. . . . 5
|
2 | | simprl 529 |
. . . . . . . . 9
|
3 | | sspwuni 3966 |
. . . . . . . . 9
|
4 | 2, 3 | sylib 122 |
. . . . . . . 8
|
5 | | vuniex 4432 |
. . . . . . . . 9
|
6 | 5 | elpw 3578 |
. . . . . . . 8
|
7 | 4, 6 | sylibr 134 |
. . . . . . 7
|
8 | | eluni2 3809 |
. . . . . . . . . 10
|
9 | | r19.29 2612 |
. . . . . . . . . . . . 13
|
10 | | simpr 110 |
. . . . . . . . . . . . . . . 16
|
11 | 10 | impr 379 |
. . . . . . . . . . . . . . 15
|
12 | | elssuni 3833 |
. . . . . . . . . . . . . . . 16
|
13 | 12 | adantr 276 |
. . . . . . . . . . . . . . 15
|
14 | 11, 13 | eqsstrrd 3190 |
. . . . . . . . . . . . . 14
|
15 | 14 | rexlimiva 2587 |
. . . . . . . . . . . . 13
|
16 | 9, 15 | syl 14 |
. . . . . . . . . . . 12
|
17 | 16 | ex 115 |
. . . . . . . . . . 11
|
18 | 17 | ad2antll 491 |
. . . . . . . . . 10
|
19 | 8, 18 | biimtrid 152 |
. . . . . . . . 9
|
20 | 19, 4 | jctild 316 |
. . . . . . . 8
|
21 | | eqss 3168 |
. . . . . . . 8
|
22 | 20, 21 | syl6ibr 162 |
. . . . . . 7
|
23 | | eleq2 2239 |
. . . . . . . . 9
|
24 | | eqeq1 2182 |
. . . . . . . . 9
|
25 | 23, 24 | imbi12d 234 |
. . . . . . . 8
|
26 | 25 | elrab 2891 |
. . . . . . 7
|
27 | 7, 22, 26 | sylanbrc 417 |
. . . . . 6
|
28 | 27 | ex 115 |
. . . . 5
|
29 | 1, 28 | biimtrid 152 |
. . . 4
|
30 | 29 | alrimiv 1872 |
. . 3
|
31 | | inss1 3353 |
. . . . . . . . 9
|
32 | | simprll 537 |
. . . . . . . . . 10
|
33 | 32 | elpwid 3583 |
. . . . . . . . 9
|
34 | 31, 33 | sstrid 3164 |
. . . . . . . 8
|
35 | | vex 2738 |
. . . . . . . . . 10
|
36 | 35 | inex1 4132 |
. . . . . . . . 9
|
37 | 36 | elpw 3578 |
. . . . . . . 8
|
38 | 34, 37 | sylibr 134 |
. . . . . . 7
|
39 | | elin 3316 |
. . . . . . . 8
|
40 | | simprlr 538 |
. . . . . . . . . 10
|
41 | | simprrr 540 |
. . . . . . . . . 10
|
42 | 40, 41 | anim12d 335 |
. . . . . . . . 9
|
43 | | ineq12 3329 |
. . . . . . . . . 10
|
44 | | inidm 3342 |
. . . . . . . . . 10
|
45 | 43, 44 | eqtrdi 2224 |
. . . . . . . . 9
|
46 | 42, 45 | syl6 33 |
. . . . . . . 8
|
47 | 39, 46 | biimtrid 152 |
. . . . . . 7
|
48 | 38, 47 | jca 306 |
. . . . . 6
|
49 | 48 | ex 115 |
. . . . 5
|
50 | | eleq2 2239 |
. . . . . . . 8
|
51 | | eqeq1 2182 |
. . . . . . . 8
|
52 | 50, 51 | imbi12d 234 |
. . . . . . 7
|
53 | 52 | elrab 2891 |
. . . . . 6
|
54 | | eleq2 2239 |
. . . . . . . 8
|
55 | | eqeq1 2182 |
. . . . . . . 8
|
56 | 54, 55 | imbi12d 234 |
. . . . . . 7
|
57 | 56 | elrab 2891 |
. . . . . 6
|
58 | 53, 57 | anbi12i 460 |
. . . . 5
|
59 | | eleq2 2239 |
. . . . . . 7
|
60 | | eqeq1 2182 |
. . . . . . 7
|
61 | 59, 60 | imbi12d 234 |
. . . . . 6
|
62 | 61 | elrab 2891 |
. . . . 5
|
63 | 49, 58, 62 | 3imtr4g 205 |
. . . 4
|
64 | 63 | ralrimivv 2556 |
. . 3
|
65 | | pwexg 4175 |
. . . . . 6
|
66 | 65 | adantr 276 |
. . . . 5
|
67 | | rabexg 4141 |
. . . . 5
|
68 | 66, 67 | syl 14 |
. . . 4
|
69 | | istopg 13066 |
. . . 4
|
70 | 68, 69 | syl 14 |
. . 3
|
71 | 30, 64, 70 | mpbir2and 944 |
. 2
|
72 | | pwidg 3586 |
. . . . . 6
|
73 | 72 | adantr 276 |
. . . . 5
|
74 | | eqidd 2176 |
. . . . . 6
|
75 | 74 | a1d 22 |
. . . . 5
|
76 | | eleq2 2239 |
. . . . . . 7
|
77 | | eqeq1 2182 |
. . . . . . 7
|
78 | 76, 77 | imbi12d 234 |
. . . . . 6
|
79 | 78 | elrab 2891 |
. . . . 5
|
80 | 73, 75, 79 | sylanbrc 417 |
. . . 4
|
81 | | elssuni 3833 |
. . . 4
|
82 | 80, 81 | syl 14 |
. . 3
|
83 | | ssrab2 3238 |
. . . . 5
|
84 | | sspwuni 3966 |
. . . . 5
|
85 | 83, 84 | mpbi 145 |
. . . 4
|
86 | 85 | a1i 9 |
. . 3
|
87 | 82, 86 | eqssd 3170 |
. 2
|
88 | | istopon 13080 |
. 2
TopOn
|
89 | 71, 87, 88 | sylanbrc 417 |
1
TopOn |