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