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 ontoClsd⁡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 ontoClsd⁡J∧F-1=x∈Clsd⁡J⟼X∖x