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 = U. J
	opncldf.2	|- F = ( u e. J |-> ( X \ u ) )
Assertion	opncldf3	|- ( B e. ( Clsd ` J ) -> ( `' F ` B ) = ( X \ B ) )

Proof

Step	Hyp	Ref	Expression
1		opncldf.1	|- X = U. J
2		opncldf.2	|- F = ( u e. J |-> ( X \ u ) )
3		cldrcl	|- ( B e. ( Clsd ` J ) -> J e. Top )
4	1 2	opncldf1	|- ( J e. Top -> ( F : J -1-1-onto-> ( Clsd ` J ) /\ `' F = ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ) )
5	4	simprd	|- ( J e. Top -> `' F = ( x e. ( Clsd ` J ) |-> ( X \ x ) ) )
6	3 5	syl	|- ( B e. ( Clsd ` J ) -> `' F = ( x e. ( Clsd ` J ) |-> ( X \ x ) ) )
7	6	fveq1d	|- ( B e. ( Clsd ` J ) -> ( `' F ` B ) = ( ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ` B ) )
8	1	cldopn	|- ( B e. ( Clsd ` J ) -> ( X \ B ) e. J )
9		difeq2	|- ( x = B -> ( X \ x ) = ( X \ B ) )
10		eqid	|- ( x e. ( Clsd ` J ) |-> ( X \ x ) ) = ( x e. ( Clsd ` J ) |-> ( X \ x ) )
11	9 10	fvmptg	|- ( ( B e. ( Clsd ` J ) /\ ( X \ B ) e. J ) -> ( ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ` B ) = ( X \ B ) )
12	8 11	mpdan	|- ( B e. ( Clsd ` J ) -> ( ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ` B ) = ( X \ B ) )
13	7 12	eqtrd	|- ( B e. ( Clsd ` J ) -> ( `' F ` B ) = ( X \ B ) )