Description: The values 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 | opncldf2 | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝑋 ∖ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opncldf.1 | ⊢ 𝑋 = ∪ 𝐽 | |
2 | opncldf.2 | ⊢ 𝐹 = ( 𝑢 ∈ 𝐽 ↦ ( 𝑋 ∖ 𝑢 ) ) | |
3 | difeq2 | ⊢ ( 𝑢 = 𝐴 → ( 𝑋 ∖ 𝑢 ) = ( 𝑋 ∖ 𝐴 ) ) | |
4 | simpr | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ∈ 𝐽 ) | |
5 | 1 | opncld | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝑋 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) ) |
6 | 2 3 4 5 | fvmptd3 | ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝑋 ∖ 𝐴 ) ) |