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	$$⊢X=\bigcup J$$
	opncldf.2	$$⊢F=\left(u\in J⟼X\setminus u\right)$$
Assertion	opncldf2	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to F\left(A\right)=X\setminus A$$

Proof

Step	Hyp	Ref	Expression
1		opncldf.1	$$⊢X=\bigcup J$$
2		opncldf.2	$$⊢F=\left(u\in J⟼X\setminus u\right)$$
3		difeq2	$$⊢u=A\to X\setminus u=X\setminus A$$
4		simpr	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to A\in J$$
5	1	opncld	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to X\setminus A\in \mathrm{Clsd}\left(J\right)$$
6	2 3 4 5	fvmptd3	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\right)\to F\left(A\right)=X\setminus A$$