Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
|
2 | 1 | fclscmpi 21833 |
. . . 4
|
3 | 2 | ralrimiva 2966 |
. . 3
|
4 | | toponuni 20719 |
. . . . 5
TopOn
|
5 | 4 | fveq2d 6195 |
. . . 4
TopOn
|
6 | 5 | raleqdv 3144 |
. . 3
TopOn
|
7 | 3, 6 | syl5ibr 236 |
. 2
TopOn
|
8 | | elpwi 4168 |
. . . . . 6
|
9 | | vn0 3924 |
. . . . . . . . . 10
|
10 | | simpr 477 |
. . . . . . . . . . . . 13
TopOn
|
11 | 10 | inteqd 4480 |
. . . . . . . . . . . 12
TopOn
|
12 | | int0 4490 |
. . . . . . . . . . . 12
|
13 | 11, 12 | syl6eq 2672 |
. . . . . . . . . . 11
TopOn
|
14 | 13 | neeq1d 2853 |
. . . . . . . . . 10
TopOn
|
15 | 9, 14 | mpbiri 248 |
. . . . . . . . 9
TopOn
|
16 | 15 | a1d 25 |
. . . . . . . 8
TopOn
|
17 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
18 | | ssfii 8325 |
. . . . . . . . . . . . . . . 16
|
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
20 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
21 | 1 | cldss2 20834 |
. . . . . . . . . . . . . . . . . . 19
|
22 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
TopOn
|
23 | 22 | pweqd 4163 |
. . . . . . . . . . . . . . . . . . 19
TopOn
|
24 | 21, 23 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
25 | 20, 24 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
TopOn
|
26 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
TopOn
|
27 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
TopOn
|
28 | | toponmax 20730 |
. . . . . . . . . . . . . . . . . . 19
TopOn
|
29 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
30 | | fsubbas 21671 |
. . . . . . . . . . . . . . . . . 18
|
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
TopOn
|
32 | 25, 26, 27, 31 | mpbir3and 1245 |
. . . . . . . . . . . . . . . 16
TopOn
|
33 | | ssfg 21676 |
. . . . . . . . . . . . . . . 16
|
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
TopOn
|
35 | 19, 34 | syl5ss 3614 |
. . . . . . . . . . . . . 14
TopOn
|
36 | 35 | sselda 3603 |
. . . . . . . . . . . . 13
TopOn
|
37 | | fclssscls 21822 |
. . . . . . . . . . . . 13
|
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
TopOn
|
39 | 20 | sselda 3603 |
. . . . . . . . . . . . 13
TopOn
|
40 | | cldcls 20846 |
. . . . . . . . . . . . 13
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
TopOn
|
42 | 38, 41 | sseqtrd 3641 |
. . . . . . . . . . 11
TopOn
|
43 | 42 | ralrimiva 2966 |
. . . . . . . . . 10
TopOn
|
44 | | ssint 4493 |
. . . . . . . . . 10
|
45 | 43, 44 | sylibr 224 |
. . . . . . . . 9
TopOn
|
46 | | fgcl 21682 |
. . . . . . . . . 10
|
47 | | oveq2 6658 |
. . . . . . . . . . . 12
|
48 | 47 | neeq1d 2853 |
. . . . . . . . . . 11
|
49 | 48 | rspcv 3305 |
. . . . . . . . . 10
|
50 | 32, 46, 49 | 3syl 18 |
. . . . . . . . 9
TopOn
|
51 | | ssn0 3976 |
. . . . . . . . 9
|
52 | 45, 50, 51 | syl6an 568 |
. . . . . . . 8
TopOn
|
53 | 16, 52 | pm2.61dane 2881 |
. . . . . . 7
TopOn
|
54 | 53 | expr 643 |
. . . . . 6
TopOn |
55 | 8, 54 | sylan2 491 |
. . . . 5
TopOn |
56 | 55 | com23 86 |
. . . 4
TopOn
|
57 | 56 | ralrimdva 2969 |
. . 3
TopOn
|
58 | | topontop 20718 |
. . . 4
TopOn
|
59 | | cmpfi 21211 |
. . . 4
|
60 | 58, 59 | syl 17 |
. . 3
TopOn
|
61 | 57, 60 | sylibrd 249 |
. 2
TopOn
|
62 | 7, 61 | impbid 202 |
1
TopOn
|