Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . . 6
TopOn
TopOn |
2 | | filelss 21656 |
. . . . . . 7
|
3 | 2 | 3adant1 1079 |
. . . . . 6
TopOn
|
4 | | resttopon 20965 |
. . . . . 6
TopOn ↾t TopOn |
5 | 1, 3, 4 | syl2anc 693 |
. . . . 5
TopOn
↾t TopOn |
6 | | filfbas 21652 |
. . . . . . . 8
|
7 | 6 | 3ad2ant2 1083 |
. . . . . . 7
TopOn
|
8 | | simp3 1063 |
. . . . . . 7
TopOn
|
9 | | fbncp 21643 |
. . . . . . 7
|
10 | 7, 8, 9 | syl2anc 693 |
. . . . . 6
TopOn
|
11 | | simp2 1062 |
. . . . . . 7
TopOn
|
12 | | trfil3 21692 |
. . . . . . 7
↾t |
13 | 11, 3, 12 | syl2anc 693 |
. . . . . 6
TopOn
↾t |
14 | 10, 13 | mpbird 247 |
. . . . 5
TopOn
↾t |
15 | | fclsopn 21818 |
. . . . 5
↾t TopOn ↾t
↾t
↾t
↾t
↾t |
16 | 5, 14, 15 | syl2anc 693 |
. . . 4
TopOn
↾t ↾t
↾t
↾t |
17 | | in32 3825 |
. . . . . . . . . . . . . 14
|
18 | | ineq2 3808 |
. . . . . . . . . . . . . 14
|
19 | 17, 18 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
20 | 19 | neeq1d 2853 |
. . . . . . . . . . . 12
|
21 | 20 | rspccv 3306 |
. . . . . . . . . . 11
|
22 | | inss1 3833 |
. . . . . . . . . . . . 13
|
23 | | ssrin 3838 |
. . . . . . . . . . . . 13
|
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
|
25 | | ssn0 3976 |
. . . . . . . . . . . 12
|
26 | 24, 25 | mpan 706 |
. . . . . . . . . . 11
|
27 | 21, 26 | syl6 35 |
. . . . . . . . . 10
|
28 | 27 | ralrimiv 2965 |
. . . . . . . . 9
|
29 | 11 | ad3antrrr 766 |
. . . . . . . . . . . 12
TopOn
|
30 | | simpr 477 |
. . . . . . . . . . . 12
TopOn
|
31 | 8 | ad3antrrr 766 |
. . . . . . . . . . . 12
TopOn
|
32 | | filin 21658 |
. . . . . . . . . . . 12
|
33 | 29, 30, 31, 32 | syl3anc 1326 |
. . . . . . . . . . 11
TopOn
|
34 | | ineq2 3808 |
. . . . . . . . . . . . . 14
|
35 | | inass 3823 |
. . . . . . . . . . . . . 14
|
36 | 34, 35 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
37 | 36 | neeq1d 2853 |
. . . . . . . . . . . 12
|
38 | 37 | rspcv 3305 |
. . . . . . . . . . 11
|
39 | 33, 38 | syl 17 |
. . . . . . . . . 10
TopOn
|
40 | 39 | ralrimdva 2969 |
. . . . . . . . 9
TopOn
|
41 | 28, 40 | impbid2 216 |
. . . . . . . 8
TopOn
|
42 | 41 | imbi2d 330 |
. . . . . . 7
TopOn
|
43 | 42 | ralbidva 2985 |
. . . . . 6
TopOn
|
44 | | vex 3203 |
. . . . . . . . 9
|
45 | 44 | inex1 4799 |
. . . . . . . 8
|
46 | 45 | a1i 11 |
. . . . . . 7
TopOn
|
47 | | elrest 16088 |
. . . . . . . . 9
TopOn ↾t
|
48 | 47 | 3adant2 1080 |
. . . . . . . 8
TopOn
↾t
|
49 | 48 | adantr 481 |
. . . . . . 7
TopOn
↾t
|
50 | | eleq2 2690 |
. . . . . . . . 9
|
51 | | elin 3796 |
. . . . . . . . . . 11
|
52 | 51 | rbaib 947 |
. . . . . . . . . 10
|
53 | 52 | adantl 482 |
. . . . . . . . 9
TopOn
|
54 | 50, 53 | sylan9bbr 737 |
. . . . . . . 8
TopOn
|
55 | | vex 3203 |
. . . . . . . . . . . 12
|
56 | 55 | inex1 4799 |
. . . . . . . . . . 11
|
57 | 56 | a1i 11 |
. . . . . . . . . 10
TopOn
|
58 | | elrest 16088 |
. . . . . . . . . . . 12
↾t
|
59 | 58 | 3adant1 1079 |
. . . . . . . . . . 11
TopOn
↾t
|
60 | 59 | adantr 481 |
. . . . . . . . . 10
TopOn
↾t
|
61 | | ineq2 3808 |
. . . . . . . . . . . 12
|
62 | 61 | adantl 482 |
. . . . . . . . . . 11
TopOn
|
63 | 62 | neeq1d 2853 |
. . . . . . . . . 10
TopOn
|
64 | 57, 60, 63 | ralxfr2d 4882 |
. . . . . . . . 9
TopOn
↾t
|
65 | | ineq1 3807 |
. . . . . . . . . . . 12
|
66 | | inindir 3831 |
. . . . . . . . . . . 12
|
67 | 65, 66 | syl6eqr 2674 |
. . . . . . . . . . 11
|
68 | 67 | neeq1d 2853 |
. . . . . . . . . 10
|
69 | 68 | ralbidv 2986 |
. . . . . . . . 9
|
70 | 64, 69 | sylan9bb 736 |
. . . . . . . 8
TopOn
↾t
|
71 | 54, 70 | imbi12d 334 |
. . . . . . 7
TopOn
↾t
|
72 | 46, 49, 71 | ralxfr2d 4882 |
. . . . . 6
TopOn
↾t
↾t
|
73 | 1 | adantr 481 |
. . . . . . 7
TopOn
TopOn |
74 | 11 | adantr 481 |
. . . . . . 7
TopOn
|
75 | 3 | sselda 3603 |
. . . . . . 7
TopOn
|
76 | | fclsopn 21818 |
. . . . . . . 8
TopOn
|
77 | 76 | baibd 948 |
. . . . . . 7
TopOn
|
78 | 73, 74, 75, 77 | syl21anc 1325 |
. . . . . 6
TopOn
|
79 | 43, 72, 78 | 3bitr4d 300 |
. . . . 5
TopOn
↾t
↾t
|
80 | 79 | pm5.32da 673 |
. . . 4
TopOn
↾t
↾t
|
81 | 16, 80 | bitrd 268 |
. . 3
TopOn
↾t ↾t
|
82 | | elin 3796 |
. . . 4
|
83 | | ancom 466 |
. . . 4
|
84 | 82, 83 | bitri 264 |
. . 3
|
85 | 81, 84 | syl6bbr 278 |
. 2
TopOn
↾t ↾t
|
86 | 85 | eqrdv 2620 |
1
TopOn
↾t ↾t |