Metamath Proof Explorer

Theorem clsval2

Description: Express closure in terms of interior. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis clscld.1 ${⊢}{X}=\bigcup {J}$
Assertion clsval2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)={X}\setminus \mathrm{int}\left({J}\right)\left({X}\setminus {S}\right)$

Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 df-rab ${⊢}\left\{{z}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {z}\right\}=\left\{{z}|\left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right\}$
3 1 cldopn ${⊢}{z}\in \mathrm{Clsd}\left({J}\right)\to {X}\setminus {z}\in {J}$
4 3 ad2antrl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {X}\setminus {z}\in {J}$
5 sscon ${⊢}{S}\subseteq {z}\to {X}\setminus {z}\subseteq {X}\setminus {S}$
6 5 ad2antll ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {X}\setminus {z}\subseteq {X}\setminus {S}$
7 1 topopn ${⊢}{J}\in \mathrm{Top}\to {X}\in {J}$
8 difexg ${⊢}{X}\in {J}\to {X}\setminus {z}\in \mathrm{V}$
9 elpwg ${⊢}{X}\setminus {z}\in \mathrm{V}\to \left({X}\setminus {z}\in 𝒫\left({X}\setminus {S}\right)↔{X}\setminus {z}\subseteq {X}\setminus {S}\right)$
10 7 8 9 3syl ${⊢}{J}\in \mathrm{Top}\to \left({X}\setminus {z}\in 𝒫\left({X}\setminus {S}\right)↔{X}\setminus {z}\subseteq {X}\setminus {S}\right)$
11 10 ad2antrr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to \left({X}\setminus {z}\in 𝒫\left({X}\setminus {S}\right)↔{X}\setminus {z}\subseteq {X}\setminus {S}\right)$
12 6 11 mpbird ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {X}\setminus {z}\in 𝒫\left({X}\setminus {S}\right)$
13 4 12 elind ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {X}\setminus {z}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)$
14 1 cldss ${⊢}{z}\in \mathrm{Clsd}\left({J}\right)\to {z}\subseteq {X}$
15 14 ad2antrl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {z}\subseteq {X}$
16 dfss4 ${⊢}{z}\subseteq {X}↔{X}\setminus \left({X}\setminus {z}\right)={z}$
17 15 16 sylib ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {X}\setminus \left({X}\setminus {z}\right)={z}$
18 17 eqcomd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to {z}={X}\setminus \left({X}\setminus {z}\right)$
19 difeq2 ${⊢}{x}={X}\setminus {z}\to {X}\setminus {x}={X}\setminus \left({X}\setminus {z}\right)$
20 19 rspceeqv ${⊢}\left({X}\setminus {z}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\wedge {z}={X}\setminus \left({X}\setminus {z}\right)\right)\to \exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}$
21 13 18 20 syl2anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)\to \exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}$
22 21 ex ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\to \exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right)$
23 simpl ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {J}\in \mathrm{Top}$
24 elinel1 ${⊢}{x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\to {x}\in {J}$
25 1 opncld ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\to {X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)$
26 23 24 25 syl2an ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to {X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)$
27 elinel2 ${⊢}{x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\to {x}\in 𝒫\left({X}\setminus {S}\right)$
28 27 adantl ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to {x}\in 𝒫\left({X}\setminus {S}\right)$
29 28 elpwid ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to {x}\subseteq {X}\setminus {S}$
30 29 difss2d ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to {x}\subseteq {X}$
31 simplr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to {S}\subseteq {X}$
32 ssconb ${⊢}\left({x}\subseteq {X}\wedge {S}\subseteq {X}\right)\to \left({x}\subseteq {X}\setminus {S}↔{S}\subseteq {X}\setminus {x}\right)$
33 30 31 32 syl2anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to \left({x}\subseteq {X}\setminus {S}↔{S}\subseteq {X}\setminus {x}\right)$
34 29 33 mpbid ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to {S}\subseteq {X}\setminus {x}$
35 26 34 jca ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to \left({X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {X}\setminus {x}\right)$
36 eleq1 ${⊢}{z}={X}\setminus {x}\to \left({z}\in \mathrm{Clsd}\left({J}\right)↔{X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)\right)$
37 sseq2 ${⊢}{z}={X}\setminus {x}\to \left({S}\subseteq {z}↔{S}\subseteq {X}\setminus {x}\right)$
38 36 37 anbi12d ${⊢}{z}={X}\setminus {x}\to \left(\left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)↔\left({X}\setminus {x}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {X}\setminus {x}\right)\right)$
39 35 38 syl5ibrcom ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\right)\to \left({z}={X}\setminus {x}\to \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)$
40 39 rexlimdva ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\to \left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right)$
41 22 40 impbid ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left(\left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)↔\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right)$
42 41 abbidv ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left\{{z}|\left({z}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {z}\right)\right\}=\left\{{z}|\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right\}$
43 2 42 syl5eq ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left\{{z}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {z}\right\}=\left\{{z}|\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right\}$
44 43 inteqd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \bigcap \left\{{z}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {z}\right\}=\bigcap \left\{{z}|\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right\}$
45 difexg ${⊢}{X}\in {J}\to {X}\setminus {x}\in \mathrm{V}$
46 45 ralrimivw ${⊢}{X}\in {J}\to \forall {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{X}\setminus {x}\in \mathrm{V}$
47 dfiin2g ${⊢}\forall {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{X}\setminus {x}\in \mathrm{V}\to \bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)=\bigcap \left\{{z}|\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right\}$
48 7 46 47 3syl ${⊢}{J}\in \mathrm{Top}\to \bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)=\bigcap \left\{{z}|\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right\}$
49 48 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)=\bigcap \left\{{z}|\exists {x}\in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\phantom{\rule{.4em}{0ex}}{z}={X}\setminus {x}\right\}$
50 44 49 eqtr4d ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \bigcap \left\{{z}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {z}\right\}=\bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)$
51 1 clsval ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)=\bigcap \left\{{z}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {z}\right\}$
52 uniiun ${⊢}\bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)=\bigcup _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}{x}$
53 52 difeq2i ${⊢}{X}\setminus \bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)={X}\setminus \bigcup _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}{x}$
54 53 a1i ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {X}\setminus \bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)={X}\setminus \bigcup _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}{x}$
55 0opn ${⊢}{J}\in \mathrm{Top}\to \varnothing \in {J}$
56 55 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \varnothing \in {J}$
57 0elpw ${⊢}\varnothing \in 𝒫\left({X}\setminus {S}\right)$
58 57 a1i ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \varnothing \in 𝒫\left({X}\setminus {S}\right)$
59 56 58 elind ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \varnothing \in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)$
60 ne0i ${⊢}\varnothing \in \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)\to {J}\cap 𝒫\left({X}\setminus {S}\right)\ne \varnothing$
61 iindif2 ${⊢}{J}\cap 𝒫\left({X}\setminus {S}\right)\ne \varnothing \to \bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)={X}\setminus \bigcup _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}{x}$
62 59 60 61 3syl ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)={X}\setminus \bigcup _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}{x}$
63 54 62 eqtr4d ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {X}\setminus \bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)=\bigcap _{{x}\in {J}\cap 𝒫\left({X}\setminus {S}\right)}\left({X}\setminus {x}\right)$
64 50 51 63 3eqtr4d ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)={X}\setminus \bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)$
65 difssd ${⊢}{S}\subseteq {X}\to {X}\setminus {S}\subseteq {X}$
66 1 ntrval ${⊢}\left({J}\in \mathrm{Top}\wedge {X}\setminus {S}\subseteq {X}\right)\to \mathrm{int}\left({J}\right)\left({X}\setminus {S}\right)=\bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)$
67 65 66 sylan2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{int}\left({J}\right)\left({X}\setminus {S}\right)=\bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)$
68 67 difeq2d ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {X}\setminus \mathrm{int}\left({J}\right)\left({X}\setminus {S}\right)={X}\setminus \bigcup \left({J}\cap 𝒫\left({X}\setminus {S}\right)\right)$
69 64 68 eqtr4d ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)={X}\setminus \mathrm{int}\left({J}\right)\left({X}\setminus {S}\right)$