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