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

Metamath Proof Explorer

Theorem cldval

Description: The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis cldval.1 ⊢ X = ⋃ J
Assertion cldval ⊢ J ∈ Top → Clsd ⁡ J = x ∈ 𝒫 X | X ∖ x ∈ J

Proof

Step Hyp Ref Expression
1 cldval.1 ⊢ X = ⋃ J
2 1 topopn ⊢ J ∈ Top → X ∈ J
3 pwexg ⊢ X ∈ J → 𝒫 X ∈ V
4 rabexg ⊢ 𝒫 X ∈ V → x ∈ 𝒫 X | X ∖ x ∈ J ∈ V
5 2 3 4 3syl ⊢ J ∈ Top → x ∈ 𝒫 X | X ∖ x ∈ J ∈ V
6 unieq ⊢ j = J → ⋃ j = ⋃ J
7 6 1 eqtr4di ⊢ j = J → ⋃ j = X
8 7 pweqd ⊢ j = J → 𝒫 ⋃ j = 𝒫 X
9 7 difeq1d ⊢ j = J → ⋃ j ∖ x = X ∖ x
10 eleq12 ⊢ ⋃ j ∖ x = X ∖ x ∧ j = J → ⋃ j ∖ x ∈ j ↔ X ∖ x ∈ J
11 9 10 mpancom ⊢ j = J → ⋃ j ∖ x ∈ j ↔ X ∖ x ∈ J
12 8 11 rabeqbidv ⊢ j = J → x ∈ 𝒫 ⋃ j | ⋃ j ∖ x ∈ j = x ∈ 𝒫 X | X ∖ x ∈ J
13 df-cld ⊢ Clsd = j ∈ Top ⟼ x ∈ 𝒫 ⋃ j | ⋃ j ∖ x ∈ j
14 12 13 fvmptg ⊢ J ∈ Top ∧ x ∈ 𝒫 X | X ∖ x ∈ J ∈ V → Clsd ⁡ J = x ∈ 𝒫 X | X ∖ x ∈ J
15 5 14 mpdan ⊢ J ∈ Top → Clsd ⁡ J = x ∈ 𝒫 X | X ∖ x ∈ J