Metamath Proof Explorer

Theorem cnpdis

Description: If A is an isolated point in X (or equivalently, the singleton { A } is open in X ), then every function is continuous at A . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion cnpdis 
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( ( J CnP K ) ` A ) = ( Y ^m X ) )

Proof

Step Hyp Ref Expression
1 simplrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> { A } e. J )
2 simpll3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> A e. X )
3 snidg 
 |-  ( A e. X -> A e. { A } )
4 2 3 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> A e. { A } )
5 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> ( f ` A ) e. x )
6 simplrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> f : X --> Y )
7 ffn 
 |-  ( f : X --> Y -> f Fn X )
8 elpreima 
 |-  ( f Fn X -> ( A e. ( `' f " x ) <-> ( A e. X /\ ( f ` A ) e. x ) ) )
9 6 7 8 3syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> ( A e. ( `' f " x ) <-> ( A e. X /\ ( f ` A ) e. x ) ) )
10 2 5 9 mpbir2and 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> A e. ( `' f " x ) )
11 10 snssd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> { A } C_ ( `' f " x ) )
12 eleq2 
 |-  ( y = { A } -> ( A e. y <-> A e. { A } ) )
13 sseq1 
 |-  ( y = { A } -> ( y C_ ( `' f " x ) <-> { A } C_ ( `' f " x ) ) )
14 12 13 anbi12d 
 |-  ( y = { A } -> ( ( A e. y /\ y C_ ( `' f " x ) ) <-> ( A e. { A } /\ { A } C_ ( `' f " x ) ) ) )
15 14 rspcev 
 |-  ( ( { A } e. J /\ ( A e. { A } /\ { A } C_ ( `' f " x ) ) ) -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) )
16 1 4 11 15 syl12anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ ( x e. K /\ ( f ` A ) e. x ) ) -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) )
17 16 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) /\ x e. K ) -> ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) )
18 17 ralrimiva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ ( { A } e. J /\ f : X --> Y ) ) -> A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) )
19 18 expr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f : X --> Y -> A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) )
20 19 pm4.71d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f : X --> Y <-> ( f : X --> Y /\ A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) )
21 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> K e. ( TopOn ` Y ) )
22 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
23 21 22 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> Y e. K )
24 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> J e. ( TopOn ` X ) )
25 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
26 24 25 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> X e. J )
27 23 26 elmapd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f e. ( Y ^m X ) <-> f : X --> Y ) )
28 iscnp3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( f e. ( ( J CnP K ) ` A ) <-> ( f : X --> Y /\ A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) )
29 28 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f e. ( ( J CnP K ) ` A ) <-> ( f : X --> Y /\ A. x e. K ( ( f ` A ) e. x -> E. y e. J ( A e. y /\ y C_ ( `' f " x ) ) ) ) ) )
30 20 27 29 3bitr4rd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( f e. ( ( J CnP K ) ` A ) <-> f e. ( Y ^m X ) ) )
31 30 eqrdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( ( J CnP K ) ` A ) = ( Y ^m X ) )