# 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 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
tgcn.3 ${⊢}{\phi }\to {K}=\mathrm{topGen}\left({B}\right)$
tgcn.4 ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
tgcnp.5 ${⊢}{\phi }\to {P}\in {X}$
Assertion tgcnp ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 tgcn.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
2 tgcn.3 ${⊢}{\phi }\to {K}=\mathrm{topGen}\left({B}\right)$
3 tgcn.4 ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({Y}\right)$
4 tgcnp.5 ${⊢}{\phi }\to {P}\in {X}$
5 iscnp ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\wedge {P}\in {X}\right)\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$
6 1 3 4 5 syl3anc ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$
7 topontop ${⊢}{K}\in \mathrm{TopOn}\left({Y}\right)\to {K}\in \mathrm{Top}$
8 3 7 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
9 2 8 eqeltrrd ${⊢}{\phi }\to \mathrm{topGen}\left({B}\right)\in \mathrm{Top}$
10 tgclb ${⊢}{B}\in \mathrm{TopBases}↔\mathrm{topGen}\left({B}\right)\in \mathrm{Top}$
11 9 10 sylibr ${⊢}{\phi }\to {B}\in \mathrm{TopBases}$
12 bastg ${⊢}{B}\in \mathrm{TopBases}\to {B}\subseteq \mathrm{topGen}\left({B}\right)$
13 11 12 syl ${⊢}{\phi }\to {B}\subseteq \mathrm{topGen}\left({B}\right)$
14 13 2 sseqtrrd ${⊢}{\phi }\to {B}\subseteq {K}$
15 ssralv ${⊢}{B}\subseteq {K}\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)$
16 14 15 syl ${⊢}{\phi }\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)$
17 16 anim2d ${⊢}{\phi }\to \left(\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\to \left({F}:{X}⟶{Y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$
18 6 17 sylbid ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\to \left({F}:{X}⟶{Y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$
19 2 eleq2d ${⊢}{\phi }\to \left({z}\in {K}↔{z}\in \mathrm{topGen}\left({B}\right)\right)$
20 19 biimpa ${⊢}\left({\phi }\wedge {z}\in {K}\right)\to {z}\in \mathrm{topGen}\left({B}\right)$
21 tg2 ${⊢}\left({z}\in \mathrm{topGen}\left({B}\right)\wedge {F}\left({P}\right)\in {z}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)$
22 r19.29 ${⊢}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\wedge \left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)\right)$
23 sstr ${⊢}\left({F}\left[{x}\right]\subseteq {y}\wedge {y}\subseteq {z}\right)\to {F}\left[{x}\right]\subseteq {z}$
24 23 expcom ${⊢}{y}\subseteq {z}\to \left({F}\left[{x}\right]\subseteq {y}\to {F}\left[{x}\right]\subseteq {z}\right)$
25 24 anim2d ${⊢}{y}\subseteq {z}\to \left(\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\to \left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)$
26 25 reximdv ${⊢}{y}\subseteq {z}\to \left(\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)$
27 26 com12 ${⊢}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\to \left({y}\subseteq {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)$
28 27 imim2i ${⊢}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \left({F}\left({P}\right)\in {y}\to \left({y}\subseteq {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)$
29 28 imp32 ${⊢}\left(\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\wedge \left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)$
30 29 rexlimivw ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\wedge \left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)$
31 22 30 syl ${⊢}\left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\wedge \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)$
32 31 expcom ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\wedge {y}\subseteq {z}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)$
33 21 32 syl ${⊢}\left({z}\in \mathrm{topGen}\left({B}\right)\wedge {F}\left({P}\right)\in {z}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)$
34 33 ex ${⊢}{z}\in \mathrm{topGen}\left({B}\right)\to \left({F}\left({P}\right)\in {z}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)$
35 34 com23 ${⊢}{z}\in \mathrm{topGen}\left({B}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \left({F}\left({P}\right)\in {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)$
36 20 35 syl ${⊢}\left({\phi }\wedge {z}\in {K}\right)\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \left({F}\left({P}\right)\in {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)$
37 36 ralrimdva ${⊢}{\phi }\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\to \forall {z}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)$
38 37 anim2d ${⊢}{\phi }\to \left(\left({F}:{X}⟶{Y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\to \left({F}:{X}⟶{Y}\wedge \forall {z}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)\right)$
39 iscnp ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\wedge {P}\in {X}\right)\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {z}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)\right)$
40 1 3 4 39 syl3anc ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {z}\in {K}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {z}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {z}\right)\right)\right)\right)$
41 38 40 sylibrd ${⊢}{\phi }\to \left(\left({F}:{X}⟶{Y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\to {F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\right)$
42 18 41 impbid ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({P}\right)\in {y}\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {F}\left[{x}\right]\subseteq {y}\right)\right)\right)\right)$