This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion clsval2 ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 df-rab ⊢ { 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑧 } = { 𝑧 ∣ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) }
3 1 cldopn ⊢ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝑧 ) ∈ 𝐽 )
4 3 ad2antrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ( 𝑋 ∖ 𝑧 ) ∈ 𝐽 )
5 sscon ⊢ ( 𝑆 ⊆ 𝑧 → ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
6 5 ad2antll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) )
7 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
8 difexg ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑋 ∖ 𝑧 ) ∈ V )
9 elpwg ⊢ ( ( 𝑋 ∖ 𝑧 ) ∈ V → ( ( 𝑋 ∖ 𝑧 ) ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) ↔ ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
10 7 8 9 3syl ⊢ ( 𝐽 ∈ Top → ( ( 𝑋 ∖ 𝑧 ) ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) ↔ ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
11 10 ad2antrr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ( ( 𝑋 ∖ 𝑧 ) ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) ↔ ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) )
12 6 11 mpbird ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ( 𝑋 ∖ 𝑧 ) ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) )
13 4 12 elind ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ( 𝑋 ∖ 𝑧 ) ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) )
14 1 cldss ⊢ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) → 𝑧 ⊆ 𝑋 )
15 14 ad2antrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → 𝑧 ⊆ 𝑋 )
16 dfss4 ⊢ ( 𝑧 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = 𝑧 )
17 15 16 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = 𝑧 )
18 17 eqcomd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → 𝑧 = ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) )
19 difeq2 ⊢ ( 𝑥 = ( 𝑋 ∖ 𝑧 ) → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) )
20 19 rspceeqv ⊢ ( ( ( 𝑋 ∖ 𝑧 ) ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ∧ 𝑧 = ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) ) → ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) )
21 13 18 20 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) → ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) )
22 21 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) → ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) ) )
23 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝐽 ∈ Top )
24 elinel1 ⊢ ( 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) → 𝑥 ∈ 𝐽 )
25 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
26 23 24 25 syl2an ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
27 elinel2 ⊢ ( 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) → 𝑥 ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) )
28 27 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → 𝑥 ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) )
29 28 elpwid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → 𝑥 ⊆ ( 𝑋 ∖ 𝑆 ) )
30 29 difss2d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → 𝑥 ⊆ 𝑋 )
31 simplr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → 𝑆 ⊆ 𝑋 )
32 ssconb ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ⊆ ( 𝑋 ∖ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
33 30 31 32 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → ( 𝑥 ⊆ ( 𝑋 ∖ 𝑆 ) ↔ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
34 29 33 mpbid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) )
35 26 34 jca ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → ( ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
36 eleq1 ⊢ ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
37 sseq2 ⊢ ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( 𝑆 ⊆ 𝑧 ↔ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) )
38 36 37 anbi12d ⊢ ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ↔ ( ( 𝑋 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ ( 𝑋 ∖ 𝑥 ) ) ) )
39 35 38 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) → ( 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) )
40 39 rexlimdva ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) → ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ) )
41 22 40 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) ↔ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) ) )
42 41 abbidv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑧 ∣ ( 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑧 ) } = { 𝑧 ∣ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) } )
43 2 42 eqtrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑧 } = { 𝑧 ∣ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) } )
44 43 inteqd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∩ { 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑧 } = ∩ { 𝑧 ∣ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) } )
45 difexg ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑋 ∖ 𝑥 ) ∈ V )
46 45 ralrimivw ⊢ ( 𝑋 ∈ 𝐽 → ∀ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) ∈ V )
47 dfiin2g ⊢ ( ∀ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) ∈ V → ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) = ∩ { 𝑧 ∣ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) } )
48 7 46 47 3syl ⊢ ( 𝐽 ∈ Top → ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) = ∩ { 𝑧 ∣ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) } )
49 48 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) = ∩ { 𝑧 ∣ ∃ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑧 = ( 𝑋 ∖ 𝑥 ) } )
50 44 49 eqtr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∩ { 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑧 } = ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) )
51 1 clsval ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑧 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑧 } )
52 uniiun ⊢ ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) = ∪ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑥
53 52 difeq2i ⊢ ( 𝑋 ∖ ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) = ( 𝑋 ∖ ∪ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑥 )
54 53 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) = ( 𝑋 ∖ ∪ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑥 ) )
55 0opn ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
56 55 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∅ ∈ 𝐽 )
57 0elpw ⊢ ∅ ∈ 𝒫 ( 𝑋 ∖ 𝑆 )
58 57 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∅ ∈ 𝒫 ( 𝑋 ∖ 𝑆 ) )
59 56 58 elind ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∅ ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) )
60 ne0i ⊢ ( ∅ ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) → ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ≠ ∅ )
61 iindif2 ⊢ ( ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ≠ ∅ → ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ ∪ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑥 ) )
62 59 60 61 3syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ ∪ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) 𝑥 ) )
63 54 62 eqtr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) = ∩ 𝑥 ∈ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ( 𝑋 ∖ 𝑥 ) )
64 50 51 63 3eqtr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) )
65 difssd ⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 )
66 1 ntrval ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑋 ∖ 𝑆 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) = ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) )
67 65 66 sylan2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) = ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) )
68 67 difeq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) = ( 𝑋 ∖ ∪ ( 𝐽 ∩ 𝒫 ( 𝑋 ∖ 𝑆 ) ) ) )
69 64 68 eqtr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )