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 syl5eq ( ( 𝐽 ∈ 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 ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) ) )