Metamath Proof Explorer

Theorem iscncl

Description: A characterization of a continuity function using closed sets. Theorem 1(d) of BourbakiTop1 p. I.9. (Contributed by FL, 19-Nov-2006) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscncl 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) )

Proof

Step Hyp Ref Expression
1 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : X --> Y )
2 1 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> F : X --> Y )
3 cnclima 
 |-  ( ( F e. ( J Cn K ) /\ y e. ( Clsd ` K ) ) -> ( `' F " y ) e. ( Clsd ` J ) )
4 3 ralrimiva 
 |-  ( F e. ( J Cn K ) -> A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) )
5 4 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) )
6 2 5 jca 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( J Cn K ) ) -> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) )
7 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) -> F : X --> Y )
8 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
9 8 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> X = U. J )
10 simplrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> F : X --> Y )
11 fimacnv 
 |-  ( F : X --> Y -> ( `' F " Y ) = X )
12 11 eqcomd 
 |-  ( F : X --> Y -> X = ( `' F " Y ) )
13 10 12 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> X = ( `' F " Y ) )
14 9 13 eqtr3d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> U. J = ( `' F " Y ) )
15 14 difeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( U. J \ ( `' F " x ) ) = ( ( `' F " Y ) \ ( `' F " x ) ) )
16 ffun 
 |-  ( F : X --> Y -> Fun F )
17 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
18 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( Y \ x ) ) = ( ( `' F " Y ) \ ( `' F " x ) ) )
19 10 16 17 18 4syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( `' F " ( Y \ x ) ) = ( ( `' F " Y ) \ ( `' F " x ) ) )
20 15 19 eqtr4d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( U. J \ ( `' F " x ) ) = ( `' F " ( Y \ x ) ) )
21 imaeq2 
 |-  ( y = ( Y \ x ) -> ( `' F " y ) = ( `' F " ( Y \ x ) ) )
22 21 eleq1d 
 |-  ( y = ( Y \ x ) -> ( ( `' F " y ) e. ( Clsd ` J ) <-> ( `' F " ( Y \ x ) ) e. ( Clsd ` J ) ) )
23 simplrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) )
24 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
25 24 ad3antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> Y = U. K )
26 25 difeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( Y \ x ) = ( U. K \ x ) )
27 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
28 27 ad3antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> K e. Top )
29 eqid 
 |-  U. K = U. K
30 29 opncld 
 |-  ( ( K e. Top /\ x e. K ) -> ( U. K \ x ) e. ( Clsd ` K ) )
31 28 30 sylancom 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( U. K \ x ) e. ( Clsd ` K ) )
32 26 31 eqeltrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( Y \ x ) e. ( Clsd ` K ) )
33 22 23 32 rspcdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( `' F " ( Y \ x ) ) e. ( Clsd ` J ) )
34 20 33 eqeltrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( U. J \ ( `' F " x ) ) e. ( Clsd ` J ) )
35 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
36 35 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> J e. Top )
37 cnvimass 
 |-  ( `' F " x ) C_ dom F
38 37 10 fssdm 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( `' F " x ) C_ X )
39 38 9 sseqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( `' F " x ) C_ U. J )
40 eqid 
 |-  U. J = U. J
41 40 isopn2 
 |-  ( ( J e. Top /\ ( `' F " x ) C_ U. J ) -> ( ( `' F " x ) e. J <-> ( U. J \ ( `' F " x ) ) e. ( Clsd ` J ) ) )
42 36 39 41 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( ( `' F " x ) e. J <-> ( U. J \ ( `' F " x ) ) e. ( Clsd ` J ) ) )
43 34 42 mpbird 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) /\ x e. K ) -> ( `' F " x ) e. J )
44 43 ralrimiva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) -> A. x e. K ( `' F " x ) e. J )
45 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
46 45 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. J ) ) )
47 7 44 46 mpbir2and 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) -> F e. ( J Cn K ) )
48 6 47 impbida 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) )