Step | Hyp | Ref
| Expression |
1 | | simpl1 1000 |
. . . . . . . . 9
|
2 | | simpl3 1002 |
. . . . . . . . 9
|
3 | | cnprest.1 |
. . . . . . . . . 10
|
4 | 3 | ntrss2 13192 |
. . . . . . . . 9
|
5 | 1, 2, 4 | syl2anc 411 |
. . . . . . . 8
|
6 | | simprl 529 |
. . . . . . . 8
|
7 | 5, 6 | sseldd 3154 |
. . . . . . 7
|
8 | | fvres 5531 |
. . . . . . 7
|
9 | 7, 8 | syl 14 |
. . . . . 6
|
10 | 9 | eqcomd 2181 |
. . . . 5
|
11 | 10 | eleq1d 2244 |
. . . 4
|
12 | | inss1 3353 |
. . . . . . . . 9
|
13 | | imass2 4997 |
. . . . . . . . 9
|
14 | | sstr2 3160 |
. . . . . . . . 9
|
15 | 12, 13, 14 | mp2b 8 |
. . . . . . . 8
|
16 | 15 | anim2i 342 |
. . . . . . 7
|
17 | 16 | reximi 2572 |
. . . . . 6
|
18 | 3 | ntropn 13188 |
. . . . . . . . . . . . 13
|
19 | 1, 2, 18 | syl2anc 411 |
. . . . . . . . . . . 12
|
20 | | inopn 13072 |
. . . . . . . . . . . . . 14
|
21 | 20 | 3com23 1209 |
. . . . . . . . . . . . 13
|
22 | 21 | 3expia 1205 |
. . . . . . . . . . . 12
|
23 | 1, 19, 22 | syl2anc 411 |
. . . . . . . . . . 11
|
24 | | elin 3316 |
. . . . . . . . . . . . . 14
|
25 | 24 | simplbi2com 1442 |
. . . . . . . . . . . . 13
|
26 | 6, 25 | syl 14 |
. . . . . . . . . . . 12
|
27 | | sslin 3359 |
. . . . . . . . . . . . . 14
|
28 | | imass2 4997 |
. . . . . . . . . . . . . 14
|
29 | 5, 27, 28 | 3syl 17 |
. . . . . . . . . . . . 13
|
30 | | sstr2 3160 |
. . . . . . . . . . . . 13
|
31 | 29, 30 | syl 14 |
. . . . . . . . . . . 12
|
32 | 26, 31 | anim12d 335 |
. . . . . . . . . . 11
|
33 | 23, 32 | anim12d 335 |
. . . . . . . . . 10
|
34 | | eleq2 2239 |
. . . . . . . . . . . 12
|
35 | | imaeq2 4959 |
. . . . . . . . . . . . 13
|
36 | 35 | sseq1d 3182 |
. . . . . . . . . . . 12
|
37 | 34, 36 | anbi12d 473 |
. . . . . . . . . . 11
|
38 | 37 | rspcev 2839 |
. . . . . . . . . 10
|
39 | 33, 38 | syl6 33 |
. . . . . . . . 9
|
40 | 39 | expdimp 259 |
. . . . . . . 8
|
41 | 40 | rexlimdva 2592 |
. . . . . . 7
|
42 | | eleq2 2239 |
. . . . . . . . 9
|
43 | | imaeq2 4959 |
. . . . . . . . . 10
|
44 | 43 | sseq1d 3182 |
. . . . . . . . 9
|
45 | 42, 44 | anbi12d 473 |
. . . . . . . 8
|
46 | 45 | cbvrexv 2702 |
. . . . . . 7
|
47 | 41, 46 | syl6ib 161 |
. . . . . 6
|
48 | 17, 47 | impbid2 143 |
. . . . 5
|
49 | | vex 2738 |
. . . . . . . 8
|
50 | 49 | inex1 4132 |
. . . . . . 7
|
51 | 50 | a1i 9 |
. . . . . 6
|
52 | | uniexg 4433 |
. . . . . . . . 9
|
53 | 1, 52 | syl 14 |
. . . . . . . 8
|
54 | 2, 3 | sseqtrdi 3201 |
. . . . . . . 8
|
55 | 53, 54 | ssexd 4138 |
. . . . . . 7
|
56 | | elrest 12617 |
. . . . . . 7
↾t
|
57 | 1, 55, 56 | syl2anc 411 |
. . . . . 6
↾t
|
58 | | eleq2 2239 |
. . . . . . . 8
|
59 | | elin 3316 |
. . . . . . . . . 10
|
60 | 59 | rbaib 921 |
. . . . . . . . 9
|
61 | 7, 60 | syl 14 |
. . . . . . . 8
|
62 | 58, 61 | sylan9bbr 463 |
. . . . . . 7
|
63 | | simpr 110 |
. . . . . . . . . 10
|
64 | 63 | imaeq2d 4963 |
. . . . . . . . 9
|
65 | | inss2 3354 |
. . . . . . . . . 10
|
66 | | resima2 4934 |
. . . . . . . . . 10
|
67 | 65, 66 | ax-mp 5 |
. . . . . . . . 9
|
68 | 64, 67 | eqtrdi 2224 |
. . . . . . . 8
|
69 | 68 | sseq1d 3182 |
. . . . . . 7
|
70 | 62, 69 | anbi12d 473 |
. . . . . 6
|
71 | 51, 57, 70 | rexxfr2d 4459 |
. . . . 5
↾t
|
72 | 48, 71 | bitr4d 191 |
. . . 4
↾t |
73 | 11, 72 | imbi12d 234 |
. . 3
↾t |
74 | 73 | ralbidv 2475 |
. 2
↾t |
75 | 3 | toptopon 13087 |
. . . . 5
TopOn |
76 | 1, 75 | sylib 122 |
. . . 4
TopOn |
77 | | simpl2 1001 |
. . . . 5
|
78 | | cnprest.2 |
. . . . . 6
|
79 | 78 | toptopon 13087 |
. . . . 5
TopOn |
80 | 77, 79 | sylib 122 |
. . . 4
TopOn |
81 | 2, 7 | sseldd 3154 |
. . . 4
|
82 | | iscnp 13270 |
. . . 4
TopOn TopOn
|
83 | 76, 80, 81, 82 | syl3anc 1238 |
. . 3
|
84 | | simprr 531 |
. . . 4
|
85 | 84 | biantrurd 305 |
. . 3
|
86 | 83, 85 | bitr4d 191 |
. 2
|
87 | | simp1l 1021 |
. . . . . . 7
|
88 | 87, 75 | sylib 122 |
. . . . . 6
TopOn |
89 | | simp1r 1022 |
. . . . . 6
|
90 | | resttopon 13242 |
. . . . . 6
TopOn ↾t TopOn |
91 | 88, 89, 90 | syl2anc 411 |
. . . . 5
↾t TopOn |
92 | | simp3 999 |
. . . . . 6
|
93 | 92, 79 | sylib 122 |
. . . . 5
TopOn |
94 | 4 | 3ad2ant1 1018 |
. . . . . 6
|
95 | | simp2l 1023 |
. . . . . 6
|
96 | 94, 95 | sseldd 3154 |
. . . . 5
|
97 | | iscnp 13270 |
. . . . 5
↾t TopOn TopOn
↾t
↾t |
98 | 91, 93, 96, 97 | syl3anc 1238 |
. . . 4
↾t
↾t |
99 | | simp2r 1024 |
. . . . . 6
|
100 | 99, 89 | fssresd 5384 |
. . . . 5
|
101 | 100 | biantrurd 305 |
. . . 4
↾t
↾t |
102 | 98, 101 | bitr4d 191 |
. . 3
↾t
↾t |
103 | 1, 2, 6, 84, 77, 102 | syl221anc 1249 |
. 2
↾t
↾t |
104 | 74, 86, 103 | 3bitr4d 220 |
1
↾t |