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	$$⊢X=\bigcup J$$
	opncldf.2	$$⊢F=\left(u\in J⟼X\setminus u\right)$$
Assertion	opncldf3	$$⊢B\in \mathrm{Clsd}\left(J\right)\to F^{-1}\left(B\right)=X\setminus B$$

Proof

Step	Hyp	Ref	Expression
1		opncldf.1	$$⊢X=\bigcup J$$
2		opncldf.2	$$⊢F=\left(u\in J⟼X\setminus u\right)$$
3		cldrcl	$$⊢B\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
4	1 2	opncldf1	$$⊢J\in \mathrm{Top}\to \left(F:J\underset{1-1\; onto}{⟶}\mathrm{Clsd}\left(J\right)\wedge F^{-1}=\left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)\right)$$
5	4	simprd	$$⊢J\in \mathrm{Top}\to F^{-1}=\left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)$$
6	3 5	syl	$$⊢B\in \mathrm{Clsd}\left(J\right)\to F^{-1}=\left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)$$
7	6	fveq1d	$$⊢B\in \mathrm{Clsd}\left(J\right)\to F^{-1}\left(B\right)=\left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)\left(B\right)$$
8	1	cldopn	$$⊢B\in \mathrm{Clsd}\left(J\right)\to X\setminus B\in J$$
9		difeq2	$$⊢x=B\to X\setminus x=X\setminus B$$
10		eqid	$$⊢\left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)=\left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)$$
11	9 10	fvmptg	$$⊢\left(B\in \mathrm{Clsd}\left(J\right)\wedge X\setminus B\in J\right)\to \left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)\left(B\right)=X\setminus B$$
12	8 11	mpdan	$$⊢B\in \mathrm{Clsd}\left(J\right)\to \left(x\in \mathrm{Clsd}\left(J\right)⟼X\setminus x\right)\left(B\right)=X\setminus B$$
13	7 12	eqtrd	$$⊢B\in \mathrm{Clsd}\left(J\right)\to F^{-1}\left(B\right)=X\setminus B$$