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 ∈ J CnP K ⁡ A ↔ ∀ y ∈ nei ⁡ K ⁡ F ⁡ A F -1 y ∈ nei ⁡ J ⁡ A

Proof

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