Metamath Proof Explorer

Theorem cnpnei

Description: A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009)

Ref Expression
Hypotheses cnpnei.1 ⊢X=⋃J
cnpnei.2 ⊢Y=⋃K
Assertion cnpnei ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F∈JCnPK⁡A↔∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A

Proof

Step Hyp Ref Expression
1 cnpnei.1 ⊢X=⋃J
2 cnpnei.2 ⊢Y=⋃K
3 cnvimass ⊢F-1y⊆dom⁡F
4 fdm ⊢F:X⟶Y→dom⁡F=X
5 3 4 sseqtrid ⊢F:X⟶Y→F-1y⊆X
6 5 3ad2ant3 ⊢J∈Top∧K∈Top∧F:X⟶Y→F-1y⊆X
7 6 ad2antrr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A→F-1y⊆X
8 neii2 ⊢K∈Top∧y∈nei⁡K⁡F⁡A→∃g∈KF⁡A⊆g∧g⊆y
9 8 3ad2antl2 ⊢J∈Top∧K∈Top∧F:X⟶Y∧y∈nei⁡K⁡F⁡A→∃g∈KF⁡A⊆g∧g⊆y
10 9 ad2ant2rl ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A→∃g∈KF⁡A⊆g∧g⊆y
11 simpll ⊢F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→F∈JCnPK⁡A
12 simprl ⊢F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→g∈K
13 fvex ⊢F⁡A∈V
14 13 snss ⊢F⁡A∈g↔F⁡A⊆g
15 14 biimpri ⊢F⁡A⊆g→F⁡A∈g
16 15 adantr ⊢F⁡A⊆g∧g⊆y→F⁡A∈g
17 16 ad2antll ⊢F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→F⁡A∈g
18 11 12 17 3jca ⊢F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→F∈JCnPK⁡A∧g∈K∧F⁡A∈g
19 18 adantll ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→F∈JCnPK⁡A∧g∈K∧F⁡A∈g
20 cnpimaex ⊢F∈JCnPK⁡A∧g∈K∧F⁡A∈g→∃o∈JA∈o∧Fo⊆g
21 19 20 syl ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→∃o∈JA∈o∧Fo⊆g
22 sstr2 ⊢Fo⊆g→g⊆y→Fo⊆y
23 22 com12 ⊢g⊆y→Fo⊆g→Fo⊆y
24 23 ad2antll ⊢g∈K∧F⁡A⊆g∧g⊆y→Fo⊆g→Fo⊆y
25 24 ad2antlr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y∧o∈J→Fo⊆g→Fo⊆y
26 ffun ⊢F:X⟶Y→Fun⁡F
27 26 3ad2ant3 ⊢J∈Top∧K∈Top∧F:X⟶Y→Fun⁡F
28 27 ad2antrr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A→Fun⁡F
29 28 ad2antrr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y∧o∈J→Fun⁡F
30 1 eltopss ⊢J∈Top∧o∈J→o⊆X
31 30 adantlr ⊢J∈Top∧F:X⟶Y∧o∈J→o⊆X
32 4 sseq2d ⊢F:X⟶Y→o⊆dom⁡F↔o⊆X
33 32 ad2antlr ⊢J∈Top∧F:X⟶Y∧o∈J→o⊆dom⁡F↔o⊆X
34 31 33 mpbird ⊢J∈Top∧F:X⟶Y∧o∈J→o⊆dom⁡F
35 34 3adantl2 ⊢J∈Top∧K∈Top∧F:X⟶Y∧o∈J→o⊆dom⁡F
36 35 adantlr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧o∈J→o⊆dom⁡F
37 36 ad4ant14 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y∧o∈J→o⊆dom⁡F
38 funimass3 ⊢Fun⁡F∧o⊆dom⁡F→Fo⊆y↔o⊆F-1y
39 29 37 38 syl2anc ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y∧o∈J→Fo⊆y↔o⊆F-1y
40 25 39 sylibd ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y∧o∈J→Fo⊆g→o⊆F-1y
41 40 anim2d ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y∧o∈J→A∈o∧Fo⊆g→A∈o∧o⊆F-1y
42 41 reximdva ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→∃o∈JA∈o∧Fo⊆g→∃o∈JA∈o∧o⊆F-1y
43 21 42 mpd ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A∧g∈K∧F⁡A⊆g∧g⊆y→∃o∈JA∈o∧o⊆F-1y
44 10 43 rexlimddv ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A→∃o∈JA∈o∧o⊆F-1y
45 1 isneip ⊢J∈Top∧A∈X→F-1y∈nei⁡J⁡A↔F-1y⊆X∧∃o∈JA∈o∧o⊆F-1y
46 45 3ad2antl1 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F-1y∈nei⁡J⁡A↔F-1y⊆X∧∃o∈JA∈o∧o⊆F-1y
47 46 adantr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A→F-1y∈nei⁡J⁡A↔F-1y⊆X∧∃o∈JA∈o∧o⊆F-1y
48 7 44 47 mpbir2and ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F∈JCnPK⁡A∧y∈nei⁡K⁡F⁡A→F-1y∈nei⁡J⁡A
49 48 exp32 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F∈JCnPK⁡A→y∈nei⁡K⁡F⁡A→F-1y∈nei⁡J⁡A
50 49 ralrimdv ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F∈JCnPK⁡A→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A
51 simpll3 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F:X⟶Y
52 opnneip ⊢K∈Top∧o∈K∧F⁡A∈o→o∈nei⁡K⁡F⁡A
53 imaeq2 ⊢y=o→F-1y=F-1o
54 53 eleq1d ⊢y=o→F-1y∈nei⁡J⁡A↔F-1o∈nei⁡J⁡A
55 54 rspcv ⊢o∈nei⁡K⁡F⁡A→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F-1o∈nei⁡J⁡A
56 52 55 syl ⊢K∈Top∧o∈K∧F⁡A∈o→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F-1o∈nei⁡J⁡A
57 56 3com23 ⊢K∈Top∧F⁡A∈o∧o∈K→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F-1o∈nei⁡J⁡A
58 57 3expb ⊢K∈Top∧F⁡A∈o∧o∈K→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F-1o∈nei⁡J⁡A
59 58 3ad2antl2 ⊢J∈Top∧K∈Top∧F:X⟶Y∧F⁡A∈o∧o∈K→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F-1o∈nei⁡J⁡A
60 59 adantlr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F-1o∈nei⁡J⁡A
61 neii2 ⊢J∈Top∧F-1o∈nei⁡J⁡A→∃g∈JA⊆g∧g⊆F-1o
62 61 ex ⊢J∈Top→F-1o∈nei⁡J⁡A→∃g∈JA⊆g∧g⊆F-1o
63 62 3ad2ant1 ⊢J∈Top∧K∈Top∧F:X⟶Y→F-1o∈nei⁡J⁡A→∃g∈JA⊆g∧g⊆F-1o
64 63 ad2antrr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K→F-1o∈nei⁡J⁡A→∃g∈JA⊆g∧g⊆F-1o
65 snssg ⊢A∈X→A∈g↔A⊆g
66 65 ad3antlr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K∧g∈J→A∈g↔A⊆g
67 27 ad3antrrr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K∧g∈J→Fun⁡F
68 1 eltopss ⊢J∈Top∧g∈J→g⊆X
69 68 3ad2antl1 ⊢J∈Top∧K∈Top∧F:X⟶Y∧g∈J→g⊆X
70 4 sseq2d ⊢F:X⟶Y→g⊆dom⁡F↔g⊆X
71 70 3ad2ant3 ⊢J∈Top∧K∈Top∧F:X⟶Y→g⊆dom⁡F↔g⊆X
72 71 biimpar ⊢J∈Top∧K∈Top∧F:X⟶Y∧g⊆X→g⊆dom⁡F
73 69 72 syldan ⊢J∈Top∧K∈Top∧F:X⟶Y∧g∈J→g⊆dom⁡F
74 73 ad4ant14 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K∧g∈J→g⊆dom⁡F
75 funimass3 ⊢Fun⁡F∧g⊆dom⁡F→Fg⊆o↔g⊆F-1o
76 67 74 75 syl2anc ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K∧g∈J→Fg⊆o↔g⊆F-1o
77 66 76 anbi12d ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K∧g∈J→A∈g∧Fg⊆o↔A⊆g∧g⊆F-1o
78 77 biimprd ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K∧g∈J→A⊆g∧g⊆F-1o→A∈g∧Fg⊆o
79 78 reximdva ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K→∃g∈JA⊆g∧g⊆F-1o→∃g∈JA∈g∧Fg⊆o
80 60 64 79 3syld ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧F⁡A∈o∧o∈K→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→∃g∈JA∈g∧Fg⊆o
81 80 exp32 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F⁡A∈o→o∈K→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→∃g∈JA∈g∧Fg⊆o
82 81 com24 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→o∈K→F⁡A∈o→∃g∈JA∈g∧Fg⊆o
83 82 imp ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→o∈K→F⁡A∈o→∃g∈JA∈g∧Fg⊆o
84 83 ralrimiv ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→∀o∈KF⁡A∈o→∃g∈JA∈g∧Fg⊆o
85 1 2 iscnp2 ⊢F∈JCnPK⁡A↔J∈Top∧K∈Top∧A∈X∧F:X⟶Y∧∀o∈KF⁡A∈o→∃g∈JA∈g∧Fg⊆o
86 85 baib ⊢J∈Top∧K∈Top∧A∈X→F∈JCnPK⁡A↔F:X⟶Y∧∀o∈KF⁡A∈o→∃g∈JA∈g∧Fg⊆o
87 86 3expa ⊢J∈Top∧K∈Top∧A∈X→F∈JCnPK⁡A↔F:X⟶Y∧∀o∈KF⁡A∈o→∃g∈JA∈g∧Fg⊆o
88 87 3adantl3 ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F∈JCnPK⁡A↔F:X⟶Y∧∀o∈KF⁡A∈o→∃g∈JA∈g∧Fg⊆o
89 88 adantr ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F∈JCnPK⁡A↔F:X⟶Y∧∀o∈KF⁡A∈o→∃g∈JA∈g∧Fg⊆o
90 51 84 89 mpbir2and ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X∧∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F∈JCnPK⁡A
91 90 ex ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A→F∈JCnPK⁡A
92 50 91 impbid ⊢J∈Top∧K∈Top∧F:X⟶Y∧A∈X→F∈JCnPK⁡A↔∀y∈nei⁡K⁡F⁡AF-1y∈nei⁡J⁡A