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

Metamath Proof Explorer

Theorem opncldf3

Description: The values of the converse/inverse of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009) (Proof shortened by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses opncldf.1 ⊢ 𝑋 = ∪ 𝐽
opncldf.2 ⊢ 𝐹 = ( 𝑢 ∈ 𝐽 ↦ ( 𝑋 ∖ 𝑢 ) )
Assertion opncldf3 ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( ◡ 𝐹 ‘ 𝐵 ) = ( 𝑋 ∖ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opncldf.1 ⊢ 𝑋 = ∪ 𝐽
2 opncldf.2 ⊢ 𝐹 = ( 𝑢 ∈ 𝐽 ↦ ( 𝑋 ∖ 𝑢 ) )
3 cldrcl ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
4 1 2 opncldf1 ⊢ ( 𝐽 ∈ Top → ( 𝐹 : 𝐽 –1-1-onto→ ( Clsd ‘ 𝐽 ) ∧ ◡ 𝐹 = ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) ) )
5 4 simprd ⊢ ( 𝐽 ∈ Top → ◡ 𝐹 = ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) )
6 3 5 syl ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ◡ 𝐹 = ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) )
7 6 fveq1d ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( ◡ 𝐹 ‘ 𝐵 ) = ( ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) ‘ 𝐵 ) )
8 1 cldopn ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝐵 ) ∈ 𝐽 )
9 difeq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ 𝐵 ) )
10 eqid ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) = ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) )
11 9 10 fvmptg ⊢ ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑋 ∖ 𝐵 ) ∈ 𝐽 ) → ( ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) ‘ 𝐵 ) = ( 𝑋 ∖ 𝐵 ) )
12 8 11 mpdan ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↦ ( 𝑋 ∖ 𝑥 ) ) ‘ 𝐵 ) = ( 𝑋 ∖ 𝐵 ) )
13 7 12 eqtrd ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( ◡ 𝐹 ‘ 𝐵 ) = ( 𝑋 ∖ 𝐵 ) )