Metamath Proof Explorer

Theorem opncldf1

Description: A bijection useful for converting statements about open sets to statements about closed sets and vice versa. (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 opncldf1 
|- ( J e. Top -> ( F : J -1-1-onto-> ( Clsd ` J ) /\ `' F = ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ) )

Proof

Step Hyp Ref Expression
1 opncldf.1 
 |-  X = U. J
2 opncldf.2 
 |-  F = ( u e. J |-> ( X \ u ) )
3 1 opncld 
 |-  ( ( J e. Top /\ u e. J ) -> ( X \ u ) e. ( Clsd ` J ) )
4 1 cldopn 
 |-  ( x e. ( Clsd ` J ) -> ( X \ x ) e. J )
5 4 adantl 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( X \ x ) e. J )
6 1 cldss 
 |-  ( x e. ( Clsd ` J ) -> x C_ X )
7 6 ad2antll 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> x C_ X )
8 dfss4 
 |-  ( x C_ X <-> ( X \ ( X \ x ) ) = x )
9 7 8 sylib 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> ( X \ ( X \ x ) ) = x )
10 9 eqcomd 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> x = ( X \ ( X \ x ) ) )
11 difeq2 
 |-  ( u = ( X \ x ) -> ( X \ u ) = ( X \ ( X \ x ) ) )
12 11 eqeq2d 
 |-  ( u = ( X \ x ) -> ( x = ( X \ u ) <-> x = ( X \ ( X \ x ) ) ) )
13 10 12 syl5ibrcom 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> ( u = ( X \ x ) -> x = ( X \ u ) ) )
14 1 eltopss 
 |-  ( ( J e. Top /\ u e. J ) -> u C_ X )
15 14 adantrr 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> u C_ X )
16 dfss4 
 |-  ( u C_ X <-> ( X \ ( X \ u ) ) = u )
17 15 16 sylib 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> ( X \ ( X \ u ) ) = u )
18 17 eqcomd 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> u = ( X \ ( X \ u ) ) )
19 difeq2 
 |-  ( x = ( X \ u ) -> ( X \ x ) = ( X \ ( X \ u ) ) )
20 19 eqeq2d 
 |-  ( x = ( X \ u ) -> ( u = ( X \ x ) <-> u = ( X \ ( X \ u ) ) ) )
21 18 20 syl5ibrcom 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> ( x = ( X \ u ) -> u = ( X \ x ) ) )
22 13 21 impbid 
 |-  ( ( J e. Top /\ ( u e. J /\ x e. ( Clsd ` J ) ) ) -> ( u = ( X \ x ) <-> x = ( X \ u ) ) )
23 2 3 5 22 f1ocnv2d 
 |-  ( J e. Top -> ( F : J -1-1-onto-> ( Clsd ` J ) /\ `' F = ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ) )