Theorem opncldf2

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 ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝑋 ∖ 𝐴 ) )

Proof

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 ∧ 𝐴 ∈ 𝐽 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝑋 ∖ 𝐴 ) )