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