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 ‘ 𝐽 ) → ( ◡ 𝐹 ‘ 𝐵 ) = ( 𝑋 ∖ 𝐵 ) )