Metamath Proof Explorer

Theorem opncldf1

Description: A bijection useful for converting statements about open sets to statements about closed sets and vice versa. (Contributed by Jeff Hankins, 27-Aug-2009) (Proof shortened by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses opncldf.1 ⊢ X = ⋃ J
opncldf.2 ⊢ F = u ∈ J ⟼ X ∖ u
Assertion opncldf1 ⊢ J ∈ Top → F : J ⟶ 1-1 onto Clsd ⁡ J ∧ F -1 = x ∈ Clsd ⁡ J ⟼ X ∖ x

Proof

Step Hyp Ref Expression
1 opncldf.1 ⊢ X = ⋃ J
2 opncldf.2 ⊢ F = u ∈ J ⟼ X ∖ u
3 1 opncld ⊢ J ∈ Top ∧ u ∈ J → X ∖ u ∈ Clsd ⁡ J
4 1 cldopn ⊢ x ∈ Clsd ⁡ J → X ∖ x ∈ J
5 4 adantl ⊢ J ∈ Top ∧ x ∈ Clsd ⁡ J → X ∖ x ∈ J
6 1 cldss ⊢ x ∈ Clsd ⁡ J → x ⊆ X
7 6 ad2antll ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → x ⊆ X
8 dfss4 ⊢ x ⊆ X ↔ X ∖ X ∖ x = x
9 7 8 sylib ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → X ∖ X ∖ x = x
10 9 eqcomd ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → x = X ∖ X ∖ x
11 difeq2 ⊢ u = X ∖ x → X ∖ u = X ∖ X ∖ x
12 11 eqeq2d ⊢ u = X ∖ x → x = X ∖ u ↔ x = X ∖ X ∖ x
13 10 12 syl5ibrcom ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → u = X ∖ x → x = X ∖ u
14 1 eltopss ⊢ J ∈ Top ∧ u ∈ J → u ⊆ X
15 14 adantrr ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → u ⊆ X
16 dfss4 ⊢ u ⊆ X ↔ X ∖ X ∖ u = u
17 15 16 sylib ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → X ∖ X ∖ u = u
18 17 eqcomd ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → u = X ∖ X ∖ u
19 difeq2 ⊢ x = X ∖ u → X ∖ x = X ∖ X ∖ u
20 19 eqeq2d ⊢ x = X ∖ u → u = X ∖ x ↔ u = X ∖ X ∖ u
21 18 20 syl5ibrcom ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → x = X ∖ u → u = X ∖ x
22 13 21 impbid ⊢ J ∈ Top ∧ u ∈ J ∧ x ∈ Clsd ⁡ J → u = X ∖ x ↔ x = X ∖ u
23 2 3 5 22 f1ocnv2d ⊢ J ∈ Top → F : J ⟶ 1-1 onto Clsd ⁡ J ∧ F -1 = x ∈ Clsd ⁡ J ⟼ X ∖ x