Metamath Proof Explorer

Theorem cnnei

Description: Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018)

Ref Expression
Hypotheses cnnei.x ⊢ X = ⋃ J
cnnei.y ⊢ Y = ⋃ K
Assertion cnnei ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y → F ∈ J Cn K ↔ ∀ p ∈ X ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w

Proof

Step Hyp Ref Expression
1 cnnei.x ⊢ X = ⋃ J
2 cnnei.y ⊢ Y = ⋃ K
3 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
4 2 toptopon ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ Y
5 3 4 anbi12i ⊢ J ∈ Top ∧ K ∈ Top ↔ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y
6 cncnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ p ∈ X F ∈ J CnP K ⁡ p
7 6 baibd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → F ∈ J Cn K ↔ ∀ p ∈ X F ∈ J CnP K ⁡ p
8 5 7 sylanb ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y → F ∈ J Cn K ↔ ∀ p ∈ X F ∈ J CnP K ⁡ p
9 5 anbi1i ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y ↔ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y
10 iscnp4 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ p ∈ X → F ∈ J CnP K ⁡ p ↔ F : X ⟶ Y ∧ ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
11 10 3expa ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ p ∈ X → F ∈ J CnP K ⁡ p ↔ F : X ⟶ Y ∧ ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
12 11 baibd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ p ∈ X ∧ F : X ⟶ Y → F ∈ J CnP K ⁡ p ↔ ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
13 12 an32s ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ p ∈ X → F ∈ J CnP K ⁡ p ↔ ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
14 9 13 sylanb ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y ∧ p ∈ X → F ∈ J CnP K ⁡ p ↔ ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
15 14 ralbidva ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y → ∀ p ∈ X F ∈ J CnP K ⁡ p ↔ ∀ p ∈ X ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
16 8 15 bitrd ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y → F ∈ J Cn K ↔ ∀ p ∈ X ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w
17 16 3impa ⊢ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y → F ∈ J Cn K ↔ ∀ p ∈ X ∀ w ∈ nei ⁡ K ⁡ F ⁡ p ∃ v ∈ nei ⁡ J ⁡ p F v ⊆ w