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 biimpri ⊢ F ⁡ A ⊆ g → F ⁡ A ∈ g
16 15 adantr ⊢ F ⁡ A ⊆ g ∧ g ⊆ y → F ⁡ A ∈ g
17 16 ad2antll ⊢ F ∈ J CnP K ⁡ A ∧ y ∈ nei ⁡ K ⁡ F ⁡ A ∧ g ∈ K ∧ F ⁡ A ⊆ g ∧ g ⊆ y → F ⁡ A ∈ g
18 11 12 17 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
19 18 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
20 cnpimaex ⊢ F ∈ J CnP K ⁡ A ∧ g ∈ K ∧ F ⁡ A ∈ g → ∃ o ∈ J A ∈ o ∧ F o ⊆ g
21 19 20 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
22 sstr2 ⊢ F o ⊆ g → g ⊆ y → F o ⊆ y
23 22 com12 ⊢ g ⊆ y → F o ⊆ g → F o ⊆ y
24 23 ad2antll ⊢ g ∈ K ∧ F ⁡ A ⊆ g ∧ g ⊆ y → F o ⊆ g → F o ⊆ y
25 24 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
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 ∈ J CnP K ⁡ A ∧ y ∈ nei ⁡ K ⁡ F ⁡ A → Fun ⁡ F
29 28 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
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 ∈ J CnP K ⁡ 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 → F o ⊆ y ↔ o ⊆ F -1 y
39 29 37 38 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
40 25 39 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
41 40 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
42 41 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
43 21 42 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
44 10 43 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
45 1 isneip ⊢ J ∈ Top ∧ A ∈ X → F -1 y ∈ nei ⁡ J ⁡ A ↔ F -1 y ⊆ X ∧ ∃ o ∈ J A ∈ o ∧ o ⊆ F -1 y
46 45 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
47 46 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
48 7 44 47 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
49 48 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
50 49 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
51 simpll3 ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y ∧ A ∈ X ∧ ∀ y ∈ nei ⁡ K ⁡ F ⁡ A F -1 y ∈ 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 -1 y = F -1 o
54 53 eleq1d ⊢ y = o → F -1 y ∈ nei ⁡ J ⁡ A ↔ F -1 o ∈ nei ⁡ J ⁡ A
55 54 rspcv ⊢ o ∈ nei ⁡ K ⁡ F ⁡ A → ∀ y ∈ nei ⁡ K ⁡ F ⁡ A F -1 y ∈ nei ⁡ J ⁡ A → F -1 o ∈ nei ⁡ J ⁡ A
56 52 55 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
57 56 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
58 57 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
59 58 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
60 59 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
61 neii2 ⊢ J ∈ Top ∧ F -1 o ∈ nei ⁡ J ⁡ A → ∃ g ∈ J A ⊆ g ∧ g ⊆ F -1 o
62 61 ex ⊢ J ∈ Top → F -1 o ∈ nei ⁡ J ⁡ A → ∃ g ∈ J A ⊆ g ∧ g ⊆ F -1 o
63 62 3ad2ant1 ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y → F -1 o ∈ nei ⁡ J ⁡ A → ∃ g ∈ J A ⊆ g ∧ g ⊆ F -1 o
64 63 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
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 → F g ⊆ o ↔ g ⊆ F -1 o
76 67 74 75 syl2anc ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y ∧ A ∈ X ∧ F ⁡ A ∈ o ∧ o ∈ K ∧ g ∈ J → F g ⊆ o ↔ g ⊆ F -1 o
77 66 76 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
78 77 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
79 78 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
80 60 64 79 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
81 80 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
82 81 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
83 82 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
84 83 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
85 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
86 85 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
87 86 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
88 87 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
89 88 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
90 51 84 89 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
91 90 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
92 50 91 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