Metamath Proof Explorer

Theorem tgcn

Description: The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-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 ) )
Assertion tgcn 
|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )

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 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
5 1 3 4 syl2anc 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
6 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
7 3 6 syl 
 |-  ( ph -> K e. Top )
8 2 7 eqeltrrd 
 |-  ( ph -> ( topGen ` B ) e. Top )
9 tgclb 
 |-  ( B e. TopBases <-> ( topGen ` B ) e. Top )
10 8 9 sylibr 
 |-  ( ph -> B e. TopBases )
11 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
12 10 11 syl 
 |-  ( ph -> B C_ ( topGen ` B ) )
13 12 2 sseqtrrd 
 |-  ( ph -> B C_ K )
14 ssralv 
 |-  ( B C_ K -> ( A. y e. K ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
15 13 14 syl 
 |-  ( ph -> ( A. y e. K ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
16 2 eleq2d 
 |-  ( ph -> ( x e. K <-> x e. ( topGen ` B ) ) )
17 eltg3 
 |-  ( B e. TopBases -> ( x e. ( topGen ` B ) <-> E. z ( z C_ B /\ x = U. z ) ) )
18 10 17 syl 
 |-  ( ph -> ( x e. ( topGen ` B ) <-> E. z ( z C_ B /\ x = U. z ) ) )
19 16 18 bitrd 
 |-  ( ph -> ( x e. K <-> E. z ( z C_ B /\ x = U. z ) ) )
20 ssralv 
 |-  ( z C_ B -> ( A. y e. B ( `' F " y ) e. J -> A. y e. z ( `' F " y ) e. J ) )
21 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
22 1 21 syl 
 |-  ( ph -> J e. Top )
23 iunopn 
 |-  ( ( J e. Top /\ A. y e. z ( `' F " y ) e. J ) -> U_ y e. z ( `' F " y ) e. J )
24 23 ex 
 |-  ( J e. Top -> ( A. y e. z ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
25 22 24 syl 
 |-  ( ph -> ( A. y e. z ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
26 20 25 sylan9r 
 |-  ( ( ph /\ z C_ B ) -> ( A. y e. B ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) )
27 imaeq2 
 |-  ( x = U. z -> ( `' F " x ) = ( `' F " U. z ) )
28 imauni 
 |-  ( `' F " U. z ) = U_ y e. z ( `' F " y )
29 27 28 eqtrdi 
 |-  ( x = U. z -> ( `' F " x ) = U_ y e. z ( `' F " y ) )
30 29 eleq1d 
 |-  ( x = U. z -> ( ( `' F " x ) e. J <-> U_ y e. z ( `' F " y ) e. J ) )
31 30 imbi2d 
 |-  ( x = U. z -> ( ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) <-> ( A. y e. B ( `' F " y ) e. J -> U_ y e. z ( `' F " y ) e. J ) ) )
32 26 31 syl5ibrcom 
 |-  ( ( ph /\ z C_ B ) -> ( x = U. z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
33 32 expimpd 
 |-  ( ph -> ( ( z C_ B /\ x = U. z ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
34 33 exlimdv 
 |-  ( ph -> ( E. z ( z C_ B /\ x = U. z ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
35 19 34 sylbid 
 |-  ( ph -> ( x e. K -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
36 35 imp 
 |-  ( ( ph /\ x e. K ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) )
37 36 ralrimdva 
 |-  ( ph -> ( A. y e. B ( `' F " y ) e. J -> A. x e. K ( `' F " x ) e. J ) )
38 imaeq2 
 |-  ( x = y -> ( `' F " x ) = ( `' F " y ) )
39 38 eleq1d 
 |-  ( x = y -> ( ( `' F " x ) e. J <-> ( `' F " y ) e. J ) )
40 39 cbvralvw 
 |-  ( A. x e. K ( `' F " x ) e. J <-> A. y e. K ( `' F " y ) e. J )
41 37 40 syl6ib 
 |-  ( ph -> ( A. y e. B ( `' F " y ) e. J -> A. y e. K ( `' F " y ) e. J ) )
42 15 41 impbid 
 |-  ( ph -> ( A. y e. K ( `' F " y ) e. J <-> A. y e. B ( `' F " y ) e. J ) )
43 42 anbi2d 
 |-  ( ph -> ( ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
44 5 43 bitrd 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )