Step | Hyp | Ref
| Expression |
1 | | llytop 21275 |
. . . 4
Locally
|
2 | 1 | adantl 482 |
. . 3
Locally
|
3 | | simplr 792 |
. . . . . 6
Locally Locally |
4 | 2 | adantr 481 |
. . . . . . 7
Locally |
5 | | islly2.2 |
. . . . . . . 8
|
6 | 5 | topopn 20711 |
. . . . . . 7
|
7 | 4, 6 | syl 17 |
. . . . . 6
Locally |
8 | | simpr 477 |
. . . . . 6
Locally |
9 | | llyi 21277 |
. . . . . 6
Locally
↾t |
10 | 3, 7, 8, 9 | syl3anc 1326 |
. . . . 5
Locally
↾t |
11 | | 3simpc 1060 |
. . . . . 6
↾t
↾t |
12 | 11 | reximi 3011 |
. . . . 5
↾t
↾t |
13 | 10, 12 | syl 17 |
. . . 4
Locally
↾t |
14 | 13 | ralrimiva 2966 |
. . 3
Locally
↾t |
15 | 2, 14 | jca 554 |
. 2
Locally
↾t |
16 | | simprl 794 |
. . 3
↾t
|
17 | | elssuni 4467 |
. . . . . . . . 9
|
18 | 17, 5 | syl6sseqr 3652 |
. . . . . . . 8
|
19 | 18 | adantl 482 |
. . . . . . 7
|
20 | | ssralv 3666 |
. . . . . . 7
↾t
↾t |
21 | 19, 20 | syl 17 |
. . . . . 6
↾t
↾t |
22 | | simpllr 799 |
. . . . . . . . . . . 12
↾t
|
23 | | simplrl 800 |
. . . . . . . . . . . 12
↾t |
24 | | simprl 794 |
. . . . . . . . . . . 12
↾t
|
25 | | inopn 20704 |
. . . . . . . . . . . 12
|
26 | 22, 23, 24, 25 | syl3anc 1326 |
. . . . . . . . . . 11
↾t |
27 | | inss1 3833 |
. . . . . . . . . . . . 13
|
28 | | vex 3203 |
. . . . . . . . . . . . . 14
|
29 | 28 | elpw2 4828 |
. . . . . . . . . . . . 13
|
30 | 27, 29 | mpbir 221 |
. . . . . . . . . . . 12
|
31 | 30 | a1i 11 |
. . . . . . . . . . 11
↾t |
32 | 26, 31 | elind 3798 |
. . . . . . . . . 10
↾t |
33 | | simplrr 801 |
. . . . . . . . . . 11
↾t |
34 | | simprrl 804 |
. . . . . . . . . . 11
↾t |
35 | 33, 34 | elind 3798 |
. . . . . . . . . 10
↾t |
36 | | inss2 3834 |
. . . . . . . . . . . . 13
|
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
↾t
|
38 | | restabs 20969 |
. . . . . . . . . . . 12
↾t ↾t ↾t |
39 | 22, 37, 24, 38 | syl3anc 1326 |
. . . . . . . . . . 11
↾t ↾t ↾t ↾t |
40 | | elrestr 16089 |
. . . . . . . . . . . . 13
↾t |
41 | 22, 24, 23, 40 | syl3anc 1326 |
. . . . . . . . . . . 12
↾t ↾t |
42 | | simprrr 805 |
. . . . . . . . . . . . 13
↾t
↾t |
43 | | restlly.1 |
. . . . . . . . . . . . . . 15
↾t |
44 | 43 | ralrimivva 2971 |
. . . . . . . . . . . . . 14
↾t |
45 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . 13
↾t
↾t |
46 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
↾t ↾t ↾t ↾t |
47 | 46 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
↾t ↾t
↾t
↾t |
48 | 47 | raleqbi1dv 3146 |
. . . . . . . . . . . . . 14
↾t
↾t
↾t ↾t
↾t |
49 | 48 | rspcv 3305 |
. . . . . . . . . . . . 13
↾t ↾t
↾t ↾t
↾t |
50 | 42, 45, 49 | sylc 65 |
. . . . . . . . . . . 12
↾t
↾t ↾t
↾t |
51 | | oveq2 6658 |
. . . . . . . . . . . . . 14
↾t
↾t
↾t
↾t |
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . 13
↾t ↾t
↾t
↾t |
53 | 52 | rspcv 3305 |
. . . . . . . . . . . 12
↾t
↾t ↾t
↾t ↾t ↾t |
54 | 41, 50, 53 | sylc 65 |
. . . . . . . . . . 11
↾t ↾t ↾t |
55 | 39, 54 | eqeltrrd 2702 |
. . . . . . . . . 10
↾t
↾t |
56 | | eleq2 2690 |
. . . . . . . . . . . 12
|
57 | | oveq2 6658 |
. . . . . . . . . . . . 13
↾t ↾t |
58 | 57 | eleq1d 2686 |
. . . . . . . . . . . 12
↾t ↾t |
59 | 56, 58 | anbi12d 747 |
. . . . . . . . . . 11
↾t
↾t
|
60 | 59 | rspcev 3309 |
. . . . . . . . . 10
↾t
↾t |
61 | 32, 35, 55, 60 | syl12anc 1324 |
. . . . . . . . 9
↾t
↾t |
62 | 61 | rexlimdvaa 3032 |
. . . . . . . 8
↾t
↾t |
63 | 62 | anassrs 680 |
. . . . . . 7
↾t
↾t |
64 | 63 | ralimdva 2962 |
. . . . . 6
↾t
↾t |
65 | 21, 64 | syld 47 |
. . . . 5
↾t
↾t |
66 | 65 | ralrimdva 2969 |
. . . 4
↾t
↾t |
67 | 66 | impr 649 |
. . 3
↾t
↾t |
68 | | islly 21271 |
. . 3
Locally
↾t |
69 | 16, 67, 68 | sylanbrc 698 |
. 2
↾t
Locally |
70 | 15, 69 | impbida 877 |
1
Locally
↾t |