Step | Hyp | Ref
| Expression |
1 | | neibastop1.1 |
. . . . . . . . 9
|
2 | | neibastop1.2 |
. . . . . . . . 9
|
3 | | neibastop1.3 |
. . . . . . . . 9
|
4 | | neibastop1.4 |
. . . . . . . . 9
|
5 | 1, 2, 3, 4 | neibastop1 32354 |
. . . . . . . 8
TopOn |
6 | | topontop 20718 |
. . . . . . . 8
TopOn
|
7 | 5, 6 | syl 17 |
. . . . . . 7
|
8 | 7 | adantr 481 |
. . . . . 6
|
9 | | eqid 2622 |
. . . . . . 7
|
10 | 9 | neii1 20910 |
. . . . . 6
|
11 | 8, 10 | sylan 488 |
. . . . 5
|
12 | | toponuni 20719 |
. . . . . . 7
TopOn
|
13 | 5, 12 | syl 17 |
. . . . . 6
|
14 | 13 | ad2antrr 762 |
. . . . 5
|
15 | 11, 14 | sseqtr4d 3642 |
. . . 4
|
16 | | neii2 20912 |
. . . . . 6
|
17 | 8, 16 | sylan 488 |
. . . . 5
|
18 | | pweq 4161 |
. . . . . . . . . . 11
|
19 | 18 | ineq2d 3814 |
. . . . . . . . . 10
|
20 | 19 | neeq1d 2853 |
. . . . . . . . 9
|
21 | 20 | raleqbi1dv 3146 |
. . . . . . . 8
|
22 | 21, 4 | elrab2 3366 |
. . . . . . 7
|
23 | | simprrr 805 |
. . . . . . . . . . . . 13
|
24 | | sspwb 4917 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | sylib 208 |
. . . . . . . . . . . 12
|
26 | | sslin 3839 |
. . . . . . . . . . . 12
|
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
|
28 | | simprrl 804 |
. . . . . . . . . . . . 13
|
29 | | snssg 4327 |
. . . . . . . . . . . . . 14
|
30 | 29 | ad3antlr 767 |
. . . . . . . . . . . . 13
|
31 | 28, 30 | mpbird 247 |
. . . . . . . . . . . 12
|
32 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
33 | 32 | ineq1d 3813 |
. . . . . . . . . . . . . 14
|
34 | 33 | neeq1d 2853 |
. . . . . . . . . . . . 13
|
35 | 34 | rspcv 3305 |
. . . . . . . . . . . 12
|
36 | 31, 35 | syl 17 |
. . . . . . . . . . 11
|
37 | | ssn0 3976 |
. . . . . . . . . . 11
|
38 | 27, 36, 37 | syl6an 568 |
. . . . . . . . . 10
|
39 | 38 | expr 643 |
. . . . . . . . 9
|
40 | 39 | com23 86 |
. . . . . . . 8
|
41 | 40 | expimpd 629 |
. . . . . . 7
|
42 | 22, 41 | syl5bi 232 |
. . . . . 6
|
43 | 42 | rexlimdv 3030 |
. . . . 5
|
44 | 17, 43 | mpd 15 |
. . . 4
|
45 | 15, 44 | jca 554 |
. . 3
|
46 | 45 | ex 450 |
. 2
|
47 | | n0 3931 |
. . . 4
|
48 | | elin 3796 |
. . . . . 6
|
49 | | simprl 794 |
. . . . . . . . 9
|
50 | 13 | ad2antrr 762 |
. . . . . . . . 9
|
51 | 49, 50 | sseqtrd 3641 |
. . . . . . . 8
|
52 | 1 | ad2antrr 762 |
. . . . . . . . 9
|
53 | 2 | ad2antrr 762 |
. . . . . . . . 9
|
54 | | simpll 790 |
. . . . . . . . . 10
|
55 | 54, 3 | sylan 488 |
. . . . . . . . 9
|
56 | | neibastop1.5 |
. . . . . . . . . 10
|
57 | 54, 56 | sylan 488 |
. . . . . . . . 9
|
58 | | neibastop1.6 |
. . . . . . . . . 10
|
59 | 54, 58 | sylan 488 |
. . . . . . . . 9
|
60 | | simplr 792 |
. . . . . . . . 9
|
61 | | simprrl 804 |
. . . . . . . . 9
|
62 | | simprrr 805 |
. . . . . . . . . 10
|
63 | 62 | elpwid 4170 |
. . . . . . . . 9
|
64 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | ineq1d 3813 |
. . . . . . . . . . . . . . 15
|
66 | 65 | cbviunv 4559 |
. . . . . . . . . . . . . 14
|
67 | | pweq 4161 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | ineq2d 3814 |
. . . . . . . . . . . . . . 15
|
69 | 68 | iuneq2d 4547 |
. . . . . . . . . . . . . 14
|
70 | 66, 69 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
71 | 70 | cbviunv 4559 |
. . . . . . . . . . . 12
|
72 | 71 | mpteq2i 4741 |
. . . . . . . . . . 11
|
73 | | rdgeq1 7507 |
. . . . . . . . . . 11
|
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . 10
|
75 | 74 | reseq1i 5392 |
. . . . . . . . 9
|
76 | | pweq 4161 |
. . . . . . . . . . . . . 14
|
77 | 76 | ineq2d 3814 |
. . . . . . . . . . . . 13
|
78 | 77 | neeq1d 2853 |
. . . . . . . . . . . 12
|
79 | 78 | cbvrexv 3172 |
. . . . . . . . . . 11
|
80 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
81 | 80 | ineq1d 3813 |
. . . . . . . . . . . . 13
|
82 | 81 | neeq1d 2853 |
. . . . . . . . . . . 12
|
83 | 82 | rexbidv 3052 |
. . . . . . . . . . 11
|
84 | 79, 83 | syl5bb 272 |
. . . . . . . . . 10
|
85 | 84 | cbvrabv 3199 |
. . . . . . . . 9
|
86 | 52, 53, 55, 4, 57, 59, 60, 49, 61, 63, 75, 85 | neibastop2lem 32355 |
. . . . . . . 8
|
87 | 7 | ad2antrr 762 |
. . . . . . . . 9
|
88 | 60, 50 | eleqtrd 2703 |
. . . . . . . . 9
|
89 | 9 | isneip 20909 |
. . . . . . . . 9
|
90 | 87, 88, 89 | syl2anc 693 |
. . . . . . . 8
|
91 | 51, 86, 90 | mpbir2and 957 |
. . . . . . 7
|
92 | 91 | expr 643 |
. . . . . 6
|
93 | 48, 92 | syl5bi 232 |
. . . . 5
|
94 | 93 | exlimdv 1861 |
. . . 4
|
95 | 47, 94 | syl5bi 232 |
. . 3
|
96 | 95 | expimpd 629 |
. 2
|
97 | 46, 96 | impbid 202 |
1
|