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 ⊢ 𝑋 = ∪ 𝐽
opncldf.2 ⊢ 𝐹 = ( 𝑢 ∈ 𝐽 ↦ ( 𝑋 ∖ 𝑢 ) )
Assertion opncldf1 ( 𝐽 ∈ Top → ( 𝐹 : 𝐽 –1-1-onto→ ( Clsd ‘ 𝐽 ) ∧ ◡ 𝐹 = ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 opncldf.1 ⊢ 𝑋 = ∪ 𝐽
2 opncldf.2 ⊢ 𝐹 = ( 𝑢 ∈ 𝐽 ↦ ( 𝑋 ∖ 𝑢 ) )
3 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑢 ) ∈ ( Clsd ‘ 𝐽 ) )
4 1 cldopn ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 )
5 4 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 )
6 1 cldss ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ 𝑋 )
7 6 ad2antll ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑥 ⊆ 𝑋 )
8 dfss4 ⊢ ( 𝑥 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
9 7 8 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
10 9 eqcomd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑥 = ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) )
11 difeq2 ⊢ ( 𝑢 = ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑢 ) = ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) )
12 11 eqeq2d ⊢ ( 𝑢 = ( 𝑋 ∖ 𝑥 ) → ( 𝑥 = ( 𝑋 ∖ 𝑢 ) ↔ 𝑥 = ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ) )
13 10 12 syl5ibrcom ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑢 = ( 𝑋 ∖ 𝑥 ) → 𝑥 = ( 𝑋 ∖ 𝑢 ) ) )
14 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ) → 𝑢 ⊆ 𝑋 )
15 14 adantrr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑢 ⊆ 𝑋 )
16 dfss4 ⊢ ( 𝑢 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑢 ) ) = 𝑢 )
17 15 16 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑢 ) ) = 𝑢 )
18 17 eqcomd ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑢 = ( 𝑋 ∖ ( 𝑋 ∖ 𝑢 ) ) )
19 difeq2 ⊢ ( 𝑥 = ( 𝑋 ∖ 𝑢 ) → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ ( 𝑋 ∖ 𝑢 ) ) )
20 19 eqeq2d ⊢ ( 𝑥 = ( 𝑋 ∖ 𝑢 ) → ( 𝑢 = ( 𝑋 ∖ 𝑥 ) ↔ 𝑢 = ( 𝑋 ∖ ( 𝑋 ∖ 𝑢 ) ) ) )
21 18 20 syl5ibrcom ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑥 = ( 𝑋 ∖ 𝑢 ) → 𝑢 = ( 𝑋 ∖ 𝑥 ) ) )
22 13 21 impbid ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑢 = ( 𝑋 ∖ 𝑥 ) ↔ 𝑥 = ( 𝑋 ∖ 𝑢 ) ) )
23 2 3 5 22 f1ocnv2d ⊢ ( 𝐽 ∈ Top → ( 𝐹 : 𝐽 –1-1-onto→ ( Clsd ‘ 𝐽 ) ∧ ◡ 𝐹 = ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) ) )