Metamath Proof Explorer

Theorem tgcnp

Description: The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses tgcn.1 
|- ( ph -> J e. ( TopOn ` X ) )
tgcn.3 
|- ( ph -> K = ( topGen ` B ) )
tgcn.4 
|- ( ph -> K e. ( TopOn ` Y ) )
tgcnp.5 
|- ( ph -> P e. X )
Assertion tgcnp 
|- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tgcn.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 tgcn.3 
 |-  ( ph -> K = ( topGen ` B ) )
3 tgcn.4 
 |-  ( ph -> K e. ( TopOn ` Y ) )
4 tgcnp.5 
 |-  ( ph -> P e. X )
5 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
6 1 3 4 5 syl3anc 
 |-  ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
7 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
8 3 7 syl 
 |-  ( ph -> K e. Top )
9 2 8 eqeltrrd 
 |-  ( ph -> ( topGen ` B ) e. Top )
10 tgclb 
 |-  ( B e. TopBases <-> ( topGen ` B ) e. Top )
11 9 10 sylibr 
 |-  ( ph -> B e. TopBases )
12 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
13 11 12 syl 
 |-  ( ph -> B C_ ( topGen ` B ) )
14 13 2 sseqtrrd 
 |-  ( ph -> B C_ K )
15 ssralv 
 |-  ( B C_ K -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
16 14 15 syl 
 |-  ( ph -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) )
17 16 anim2d 
 |-  ( ph -> ( ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) -> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
18 6 17 sylbid 
 |-  ( ph -> ( F e. ( ( J CnP K ) ` P ) -> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
19 2 eleq2d 
 |-  ( ph -> ( z e. K <-> z e. ( topGen ` B ) ) )
20 19 biimpa 
 |-  ( ( ph /\ z e. K ) -> z e. ( topGen ` B ) )
21 tg2 
 |-  ( ( z e. ( topGen ` B ) /\ ( F ` P ) e. z ) -> E. y e. B ( ( F ` P ) e. y /\ y C_ z ) )
22 r19.29 
 |-  ( ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ E. y e. B ( ( F ` P ) e. y /\ y C_ z ) ) -> E. y e. B ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ ( ( F ` P ) e. y /\ y C_ z ) ) )
23 sstr 
 |-  ( ( ( F " x ) C_ y /\ y C_ z ) -> ( F " x ) C_ z )
24 23 expcom 
 |-  ( y C_ z -> ( ( F " x ) C_ y -> ( F " x ) C_ z ) )
25 24 anim2d 
 |-  ( y C_ z -> ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. x /\ ( F " x ) C_ z ) ) )
26 25 reximdv 
 |-  ( y C_ z -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) )
27 26 com12 
 |-  ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> ( y C_ z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) )
28 27 imim2i 
 |-  ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( ( F ` P ) e. y -> ( y C_ z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) )
29 28 imp32 
 |-  ( ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ ( ( F ` P ) e. y /\ y C_ z ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) )
30 29 rexlimivw 
 |-  ( E. y e. B ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ ( ( F ` P ) e. y /\ y C_ z ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) )
31 22 30 syl 
 |-  ( ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) /\ E. y e. B ( ( F ` P ) e. y /\ y C_ z ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) )
32 31 expcom 
 |-  ( E. y e. B ( ( F ` P ) e. y /\ y C_ z ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) )
33 21 32 syl 
 |-  ( ( z e. ( topGen ` B ) /\ ( F ` P ) e. z ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) )
34 33 ex 
 |-  ( z e. ( topGen ` B ) -> ( ( F ` P ) e. z -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) )
35 34 com23 
 |-  ( z e. ( topGen ` B ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) )
36 20 35 syl 
 |-  ( ( ph /\ z e. K ) -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) )
37 36 ralrimdva 
 |-  ( ph -> ( A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) -> A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) )
38 37 anim2d 
 |-  ( ph -> ( ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) -> ( F : X --> Y /\ A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) )
39 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) )
40 1 3 4 39 syl3anc 
 |-  ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. z e. K ( ( F ` P ) e. z -> E. x e. J ( P e. x /\ ( F " x ) C_ z ) ) ) ) )
41 38 40 sylibrd 
 |-  ( ph -> ( ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) -> F e. ( ( J CnP K ) ` P ) ) )
42 18 41 impbid 
 |-  ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )