This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )