Metamath Proof Explorer


Theorem ntreq0

Description: Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis clscld.1 X=J
Assertion ntreq0 JTopSXintJS=xJxSx=

Proof

Step Hyp Ref Expression
1 clscld.1 X=J
2 1 ntrval JTopSXintJS=J𝒫S
3 2 eqeq1d JTopSXintJS=J𝒫S=
4 neq0 ¬J𝒫S=yyJ𝒫S
5 4 con1bii ¬yyJ𝒫SJ𝒫S=
6 ancom yxxJ𝒫SxJ𝒫Syx
7 elin xJ𝒫SxJx𝒫S
8 7 anbi1i xJ𝒫SyxxJx𝒫Syx
9 anass xJx𝒫SyxxJx𝒫Syx
10 6 8 9 3bitri yxxJ𝒫SxJx𝒫Syx
11 10 exbii xyxxJ𝒫SxxJx𝒫Syx
12 eluni yJ𝒫SxyxxJ𝒫S
13 df-rex xJx𝒫SyxxxJx𝒫Syx
14 11 12 13 3bitr4i yJ𝒫SxJx𝒫Syx
15 14 exbii yyJ𝒫SyxJx𝒫Syx
16 rexcom4 xJyx𝒫SyxyxJx𝒫Syx
17 19.42v yx𝒫Syxx𝒫Syyx
18 17 rexbii xJyx𝒫SyxxJx𝒫Syyx
19 15 16 18 3bitr2i yyJ𝒫SxJx𝒫Syyx
20 19 notbii ¬yyJ𝒫S¬xJx𝒫Syyx
21 5 20 bitr3i J𝒫S=¬xJx𝒫Syyx
22 ralinexa xJx𝒫S¬yyx¬xJx𝒫Syyx
23 velpw x𝒫SxS
24 neq0 ¬x=yyx
25 24 con1bii ¬yyxx=
26 23 25 imbi12i x𝒫S¬yyxxSx=
27 26 ralbii xJx𝒫S¬yyxxJxSx=
28 21 22 27 3bitr2i J𝒫S=xJxSx=
29 3 28 bitrdi JTopSXintJS=xJxSx=