Metamath Proof Explorer

Theorem cncnpi

Description: A continuous function is continuous at all points. One direction of Theorem 7.2(g) of Munkres p. 107. (Contributed by Raph Levien, 20-Nov-2006) (Proof shortened by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypothesis cnsscnp.1 
|- X = U. J
Assertion cncnpi 
|- ( ( F e. ( J Cn K ) /\ A e. X ) -> F e. ( ( J CnP K ) ` A ) )

Proof

Step Hyp Ref Expression
1 cnsscnp.1 
 |-  X = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> U. K )
4 3 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> F : X --> U. K )
5 cnima 
 |-  ( ( F e. ( J Cn K ) /\ y e. K ) -> ( `' F " y ) e. J )
6 5 ad2ant2r 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> ( `' F " y ) e. J )
7 simpr 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> A e. X )
8 7 adantr 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> A e. X )
9 simprr 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> ( F ` A ) e. y )
10 3 ad2antrr 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> F : X --> U. K )
11 ffn 
 |-  ( F : X --> U. K -> F Fn X )
12 elpreima 
 |-  ( F Fn X -> ( A e. ( `' F " y ) <-> ( A e. X /\ ( F ` A ) e. y ) ) )
13 10 11 12 3syl 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> ( A e. ( `' F " y ) <-> ( A e. X /\ ( F ` A ) e. y ) ) )
14 8 9 13 mpbir2and 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> A e. ( `' F " y ) )
15 eqimss 
 |-  ( x = ( `' F " y ) -> x C_ ( `' F " y ) )
16 15 biantrud 
 |-  ( x = ( `' F " y ) -> ( A e. x <-> ( A e. x /\ x C_ ( `' F " y ) ) ) )
17 eleq2 
 |-  ( x = ( `' F " y ) -> ( A e. x <-> A e. ( `' F " y ) ) )
18 16 17 bitr3d 
 |-  ( x = ( `' F " y ) -> ( ( A e. x /\ x C_ ( `' F " y ) ) <-> A e. ( `' F " y ) ) )
19 18 rspcev 
 |-  ( ( ( `' F " y ) e. J /\ A e. ( `' F " y ) ) -> E. x e. J ( A e. x /\ x C_ ( `' F " y ) ) )
20 6 14 19 syl2anc 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ ( y e. K /\ ( F ` A ) e. y ) ) -> E. x e. J ( A e. x /\ x C_ ( `' F " y ) ) )
21 20 expr 
 |-  ( ( ( F e. ( J Cn K ) /\ A e. X ) /\ y e. K ) -> ( ( F ` A ) e. y -> E. x e. J ( A e. x /\ x C_ ( `' F " y ) ) ) )
22 21 ralrimiva 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> A. y e. K ( ( F ` A ) e. y -> E. x e. J ( A e. x /\ x C_ ( `' F " y ) ) ) )
23 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
24 23 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> J e. Top )
25 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
26 24 25 sylib 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> J e. ( TopOn ` X ) )
27 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
28 27 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> K e. Top )
29 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
30 28 29 sylib 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> K e. ( TopOn ` U. K ) )
31 iscnp3 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> U. K /\ A. y e. K ( ( F ` A ) e. y -> E. x e. J ( A e. x /\ x C_ ( `' F " y ) ) ) ) ) )
32 26 30 7 31 syl3anc 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> U. K /\ A. y e. K ( ( F ` A ) e. y -> E. x e. J ( A e. x /\ x C_ ( `' F " y ) ) ) ) ) )
33 4 22 32 mpbir2and 
 |-  ( ( F e. ( J Cn K ) /\ A e. X ) -> F e. ( ( J CnP K ) ` A ) )