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 = U. J
	opncldf.2	|- F = ( u e. J |-> ( X \ u ) )
Assertion	opncldf2	|- ( ( J e. Top /\ A e. J ) -> ( F ` A ) = ( X \ A ) )

Proof

Step	Hyp	Ref	Expression
1		opncldf.1	|- X = U. J
2		opncldf.2	|- F = ( u e. J |-> ( X \ u ) )
3		difeq2	|- ( u = A -> ( X \ u ) = ( X \ A ) )
4		simpr	|- ( ( J e. Top /\ A e. J ) -> A e. J )
5	1	opncld	|- ( ( J e. Top /\ A e. J ) -> ( X \ A ) e. ( Clsd ` J ) )
6	2 3 4 5	fvmptd3	|- ( ( J e. Top /\ A e. J ) -> ( F ` A ) = ( X \ A ) )