Step | Hyp | Ref
| Expression |
1 | | df-rab 2921 |
. . . . . 6
|
2 | | clscld.1 |
. . . . . . . . . . . . 13
|
3 | 2 | cldopn 20835 |
. . . . . . . . . . . 12
|
4 | 3 | ad2antrl 764 |
. . . . . . . . . . 11
|
5 | | sscon 3744 |
. . . . . . . . . . . . 13
|
6 | 5 | ad2antll 765 |
. . . . . . . . . . . 12
|
7 | 2 | topopn 20711 |
. . . . . . . . . . . . . 14
|
8 | | difexg 4808 |
. . . . . . . . . . . . . 14
|
9 | | elpwg 4166 |
. . . . . . . . . . . . . 14
|
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . 13
|
11 | 10 | ad2antrr 762 |
. . . . . . . . . . . 12
|
12 | 6, 11 | mpbird 247 |
. . . . . . . . . . 11
|
13 | 4, 12 | elind 3798 |
. . . . . . . . . 10
|
14 | 2 | cldss 20833 |
. . . . . . . . . . . . 13
|
15 | 14 | ad2antrl 764 |
. . . . . . . . . . . 12
|
16 | | dfss4 3858 |
. . . . . . . . . . . 12
|
17 | 15, 16 | sylib 208 |
. . . . . . . . . . 11
|
18 | 17 | eqcomd 2628 |
. . . . . . . . . 10
|
19 | | difeq2 3722 |
. . . . . . . . . . . 12
|
20 | 19 | eqeq2d 2632 |
. . . . . . . . . . 11
|
21 | 20 | rspcev 3309 |
. . . . . . . . . 10
|
22 | 13, 18, 21 | syl2anc 693 |
. . . . . . . . 9
|
23 | 22 | ex 450 |
. . . . . . . 8
|
24 | | simpl 473 |
. . . . . . . . . . . 12
|
25 | | elin 3796 |
. . . . . . . . . . . . 13
|
26 | 25 | simplbi 476 |
. . . . . . . . . . . 12
|
27 | 2 | opncld 20837 |
. . . . . . . . . . . 12
|
28 | 24, 26, 27 | syl2an 494 |
. . . . . . . . . . 11
|
29 | 25 | simprbi 480 |
. . . . . . . . . . . . . 14
|
30 | 29 | adantl 482 |
. . . . . . . . . . . . 13
|
31 | 30 | elpwid 4170 |
. . . . . . . . . . . 12
|
32 | 31 | difss2d 3740 |
. . . . . . . . . . . . 13
|
33 | | simplr 792 |
. . . . . . . . . . . . 13
|
34 | | ssconb 3743 |
. . . . . . . . . . . . 13
|
35 | 32, 33, 34 | syl2anc 693 |
. . . . . . . . . . . 12
|
36 | 31, 35 | mpbid 222 |
. . . . . . . . . . 11
|
37 | 28, 36 | jca 554 |
. . . . . . . . . 10
|
38 | | eleq1 2689 |
. . . . . . . . . . 11
|
39 | | sseq2 3627 |
. . . . . . . . . . 11
|
40 | 38, 39 | anbi12d 747 |
. . . . . . . . . 10
|
41 | 37, 40 | syl5ibrcom 237 |
. . . . . . . . 9
|
42 | 41 | rexlimdva 3031 |
. . . . . . . 8
|
43 | 23, 42 | impbid 202 |
. . . . . . 7
|
44 | 43 | abbidv 2741 |
. . . . . 6
|
45 | 1, 44 | syl5eq 2668 |
. . . . 5
|
46 | 45 | inteqd 4480 |
. . . 4
|
47 | | difexg 4808 |
. . . . . . 7
|
48 | 47 | ralrimivw 2967 |
. . . . . 6
|
49 | | dfiin2g 4553 |
. . . . . 6
|
50 | 7, 48, 49 | 3syl 18 |
. . . . 5
|
51 | 50 | adantr 481 |
. . . 4
|
52 | 46, 51 | eqtr4d 2659 |
. . 3
|
53 | 2 | clsval 20841 |
. . 3
|
54 | | uniiun 4573 |
. . . . . 6
|
55 | 54 | difeq2i 3725 |
. . . . 5
|
56 | 55 | a1i 11 |
. . . 4
|
57 | | 0opn 20709 |
. . . . . . 7
|
58 | 57 | adantr 481 |
. . . . . 6
|
59 | | 0elpw 4834 |
. . . . . . 7
|
60 | 59 | a1i 11 |
. . . . . 6
|
61 | 58, 60 | elind 3798 |
. . . . 5
|
62 | | ne0i 3921 |
. . . . 5
|
63 | | iindif2 4589 |
. . . . 5
|
64 | 61, 62, 63 | 3syl 18 |
. . . 4
|
65 | 56, 64 | eqtr4d 2659 |
. . 3
|
66 | 52, 53, 65 | 3eqtr4d 2666 |
. 2
|
67 | | difssd 3738 |
. . . 4
|
68 | 2 | ntrval 20840 |
. . . 4
|
69 | 67, 68 | sylan2 491 |
. . 3
|
70 | 69 | difeq2d 3728 |
. 2
|
71 | 66, 70 | eqtr4d 2659 |
1
|