Step | Hyp | Ref
| Expression |
1 | | cntop1 13272 |
. . . 4
|
2 | 1 | a1i 9 |
. . 3
TopOn
|
3 | | eqid 2175 |
. . . . . . . 8
|
4 | | eqid 2175 |
. . . . . . . 8
|
5 | 3, 4 | cnf 13275 |
. . . . . . 7
|
6 | 5 | ffnd 5358 |
. . . . . 6
|
7 | 6 | a1i 9 |
. . . . 5
TopOn
|
8 | | simp2 998 |
. . . . 5
TopOn |
9 | 7, 8 | jctird 317 |
. . . 4
TopOn
|
10 | | df-f 5212 |
. . . 4
|
11 | 9, 10 | syl6ibr 162 |
. . 3
TopOn
|
12 | 2, 11 | jcad 307 |
. 2
TopOn
|
13 | | cntop1 13272 |
. . . . 5
↾t
|
14 | 13 | adantl 277 |
. . . 4
TopOn ↾t |
15 | 3 | toptopon 13087 |
. . . . . 6
TopOn |
16 | 14, 15 | sylib 122 |
. . . . 5
TopOn ↾t TopOn |
17 | | resttopon 13242 |
. . . . . . 7
TopOn ↾t TopOn |
18 | 17 | 3adant2 1016 |
. . . . . 6
TopOn ↾t TopOn |
19 | 18 | adantr 276 |
. . . . 5
TopOn ↾t ↾t TopOn |
20 | | simpr 110 |
. . . . 5
TopOn ↾t ↾t |
21 | | cnf2 13276 |
. . . . 5
TopOn ↾t TopOn ↾t |
22 | 16, 19, 20, 21 | syl3anc 1238 |
. . . 4
TopOn ↾t |
23 | 14, 22 | jca 306 |
. . 3
TopOn ↾t
|
24 | 23 | ex 115 |
. 2
TopOn
↾t |
25 | | vex 2738 |
. . . . . . . . 9
|
26 | 25 | inex1 4132 |
. . . . . . . 8
|
27 | 26 | a1i 9 |
. . . . . . 7
TopOn
|
28 | | simpl1 1000 |
. . . . . . . 8
TopOn
TopOn |
29 | | toponmax 13094 |
. . . . . . . . . 10
TopOn
|
30 | 28, 29 | syl 14 |
. . . . . . . . 9
TopOn
|
31 | | simpl3 1002 |
. . . . . . . . 9
TopOn
|
32 | 30, 31 | ssexd 4138 |
. . . . . . . 8
TopOn
|
33 | | elrest 12617 |
. . . . . . . 8
TopOn ↾t
|
34 | 28, 32, 33 | syl2anc 411 |
. . . . . . 7
TopOn
↾t
|
35 | | imaeq2 4959 |
. . . . . . . . 9
|
36 | 35 | eleq1d 2244 |
. . . . . . . 8
|
37 | 36 | adantl 277 |
. . . . . . 7
TopOn
|
38 | 27, 34, 37 | ralxfr2d 4458 |
. . . . . 6
TopOn
↾t |
39 | | simplrr 536 |
. . . . . . . . . 10
TopOn
|
40 | | ffun 5360 |
. . . . . . . . . 10
|
41 | | inpreima 5634 |
. . . . . . . . . 10
|
42 | 39, 40, 41 | 3syl 17 |
. . . . . . . . 9
TopOn
|
43 | | cnvimass 4984 |
. . . . . . . . . . . 12
|
44 | | cnvimarndm 4985 |
. . . . . . . . . . . 12
|
45 | 43, 44 | sseqtrri 3188 |
. . . . . . . . . . 11
|
46 | | simpll2 1037 |
. . . . . . . . . . . 12
TopOn
|
47 | | imass2 4997 |
. . . . . . . . . . . 12
|
48 | 46, 47 | syl 14 |
. . . . . . . . . . 11
TopOn
|
49 | 45, 48 | sstrid 3164 |
. . . . . . . . . 10
TopOn
|
50 | | df-ss 3140 |
. . . . . . . . . 10
|
51 | 49, 50 | sylib 122 |
. . . . . . . . 9
TopOn
|
52 | 42, 51 | eqtrd 2208 |
. . . . . . . 8
TopOn
|
53 | 52 | eleq1d 2244 |
. . . . . . 7
TopOn
|
54 | 53 | ralbidva 2471 |
. . . . . 6
TopOn
|
55 | | simprr 531 |
. . . . . . . 8
TopOn
|
56 | 55, 31 | fssd 5370 |
. . . . . . 7
TopOn
|
57 | 56 | biantrurd 305 |
. . . . . 6
TopOn
|
58 | 38, 54, 57 | 3bitrrd 215 |
. . . . 5
TopOn
↾t |
59 | 55 | biantrurd 305 |
. . . . 5
TopOn
↾t
↾t |
60 | 58, 59 | bitrd 188 |
. . . 4
TopOn
↾t |
61 | | simprl 529 |
. . . . . 6
TopOn
|
62 | 61, 15 | sylib 122 |
. . . . 5
TopOn
TopOn |
63 | | iscn 13268 |
. . . . 5
TopOn TopOn
|
64 | 62, 28, 63 | syl2anc 411 |
. . . 4
TopOn
|
65 | 18 | adantr 276 |
. . . . 5
TopOn
↾t TopOn |
66 | | iscn 13268 |
. . . . 5
TopOn ↾t TopOn ↾t
↾t |
67 | 62, 65, 66 | syl2anc 411 |
. . . 4
TopOn
↾t
↾t |
68 | 60, 64, 67 | 3bitr4d 220 |
. . 3
TopOn
↾t |
69 | 68 | ex 115 |
. 2
TopOn
↾t |
70 | 12, 24, 69 | pm5.21ndd 705 |
1
TopOn
↾t |