Metamath Proof Explorer

Theorem subbascn

Description: The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses subbascn.1 
|- ( ph -> J e. ( TopOn ` X ) )
subbascn.2 
|- ( ph -> B e. V )
subbascn.3 
|- ( ph -> K = ( topGen ` ( fi ` B ) ) )
subbascn.4 
|- ( ph -> K e. ( TopOn ` Y ) )
Assertion subbascn 
|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )

Proof

Step Hyp Ref Expression
1 subbascn.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 subbascn.2 
 |-  ( ph -> B e. V )
3 subbascn.3 
 |-  ( ph -> K = ( topGen ` ( fi ` B ) ) )
4 subbascn.4 
 |-  ( ph -> K e. ( TopOn ` Y ) )
5 1 3 4 tgcn 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( fi ` B ) ( `' F " y ) e. J ) ) )
6 2 adantr 
 |-  ( ( ph /\ F : X --> Y ) -> B e. V )
7 ssfii 
 |-  ( B e. V -> B C_ ( fi ` B ) )
8 ssralv 
 |-  ( B C_ ( fi ` B ) -> ( A. y e. ( fi ` B ) ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
9 6 7 8 3syl 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. y e. ( fi ` B ) ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) )
10 vex 
 |-  x e. _V
11 elfi 
 |-  ( ( x e. _V /\ B e. V ) -> ( x e. ( fi ` B ) <-> E. z e. ( ~P B i^i Fin ) x = |^| z ) )
12 10 6 11 sylancr 
 |-  ( ( ph /\ F : X --> Y ) -> ( x e. ( fi ` B ) <-> E. z e. ( ~P B i^i Fin ) x = |^| z ) )
13 simpr2 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> x = |^| z )
14 13 imaeq2d 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " x ) = ( `' F " |^| z ) )
15 ffun 
 |-  ( F : X --> Y -> Fun F )
16 15 ad2antlr 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> Fun F )
17 13 10 eqeltrrdi 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> |^| z e. _V )
18 intex 
 |-  ( z =/= (/) <-> |^| z e. _V )
19 17 18 sylibr 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z =/= (/) )
20 intpreima 
 |-  ( ( Fun F /\ z =/= (/) ) -> ( `' F " |^| z ) = |^|_ y e. z ( `' F " y ) )
21 16 19 20 syl2anc 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " |^| z ) = |^|_ y e. z ( `' F " y ) )
22 14 21 eqtrd 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " x ) = |^|_ y e. z ( `' F " y ) )
23 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
24 1 23 syl 
 |-  ( ph -> J e. Top )
25 24 ad2antrr 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> J e. Top )
26 simpr1 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z e. ( ~P B i^i Fin ) )
27 26 elin2d 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z e. Fin )
28 26 elin1d 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z e. ~P B )
29 28 elpwid 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z C_ B )
30 simpr3 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> A. y e. B ( `' F " y ) e. J )
31 ssralv 
 |-  ( z C_ B -> ( A. y e. B ( `' F " y ) e. J -> A. y e. z ( `' F " y ) e. J ) )
32 29 30 31 sylc 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> A. y e. z ( `' F " y ) e. J )
33 iinopn 
 |-  ( ( J e. Top /\ ( z e. Fin /\ z =/= (/) /\ A. y e. z ( `' F " y ) e. J ) ) -> |^|_ y e. z ( `' F " y ) e. J )
34 25 27 19 32 33 syl13anc 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> |^|_ y e. z ( `' F " y ) e. J )
35 22 34 eqeltrd 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " x ) e. J )
36 35 3exp2 
 |-  ( ( ph /\ F : X --> Y ) -> ( z e. ( ~P B i^i Fin ) -> ( x = |^| z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) ) )
37 36 rexlimdv 
 |-  ( ( ph /\ F : X --> Y ) -> ( E. z e. ( ~P B i^i Fin ) x = |^| z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
38 12 37 sylbid 
 |-  ( ( ph /\ F : X --> Y ) -> ( x e. ( fi ` B ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) )
39 38 com23 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. y e. B ( `' F " y ) e. J -> ( x e. ( fi ` B ) -> ( `' F " x ) e. J ) ) )
40 39 ralrimdv 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. y e. B ( `' F " y ) e. J -> A. x e. ( fi ` B ) ( `' F " x ) e. J ) )
41 imaeq2 
 |-  ( y = x -> ( `' F " y ) = ( `' F " x ) )
42 41 eleq1d 
 |-  ( y = x -> ( ( `' F " y ) e. J <-> ( `' F " x ) e. J ) )
43 42 cbvralvw 
 |-  ( A. y e. ( fi ` B ) ( `' F " y ) e. J <-> A. x e. ( fi ` B ) ( `' F " x ) e. J )
44 40 43 imbitrrdi 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. y e. B ( `' F " y ) e. J -> A. y e. ( fi ` B ) ( `' F " y ) e. J ) )
45 9 44 impbid 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. y e. ( fi ` B ) ( `' F " y ) e. J <-> A. y e. B ( `' F " y ) e. J ) )
46 45 pm5.32da 
 |-  ( ph -> ( ( F : X --> Y /\ A. y e. ( fi ` B ) ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
47 5 46 bitrd 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )