Metamath Proof Explorer

Theorem cnpval

Description: The set of all functions from topology J to topology K that are continuous at a point P . (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Assertion cnpval ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → J CnP K ⁡ P = f ∈ Y X | ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y

Proof

Step Hyp Ref Expression
1 cnpfval ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → J CnP K = v ∈ X ⟼ f ∈ Y X | ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y
2 1 fveq1d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → J CnP K ⁡ P = v ∈ X ⟼ f ∈ Y X | ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y ⁡ P
3 fveq2 ⊢ v = P → f ⁡ v = f ⁡ P
4 3 eleq1d ⊢ v = P → f ⁡ v ∈ y ↔ f ⁡ P ∈ y
5 eleq1 ⊢ v = P → v ∈ x ↔ P ∈ x
6 5 anbi1d ⊢ v = P → v ∈ x ∧ f x ⊆ y ↔ P ∈ x ∧ f x ⊆ y
7 6 rexbidv ⊢ v = P → ∃ x ∈ J v ∈ x ∧ f x ⊆ y ↔ ∃ x ∈ J P ∈ x ∧ f x ⊆ y
8 4 7 imbi12d ⊢ v = P → f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y ↔ f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y
9 8 ralbidv ⊢ v = P → ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y ↔ ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y
10 9 rabbidv ⊢ v = P → f ∈ Y X | ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y = f ∈ Y X | ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y
11 eqid ⊢ v ∈ X ⟼ f ∈ Y X | ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y = v ∈ X ⟼ f ∈ Y X | ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y
12 ovex ⊢ Y X ∈ V
13 12 rabex ⊢ f ∈ Y X | ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y ∈ V
14 10 11 13 fvmpt ⊢ P ∈ X → v ∈ X ⟼ f ∈ Y X | ∀ y ∈ K f ⁡ v ∈ y → ∃ x ∈ J v ∈ x ∧ f x ⊆ y ⁡ P = f ∈ Y X | ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y
15 2 14 sylan9eq ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → J CnP K ⁡ P = f ∈ Y X | ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y
16 15 3impa ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → J CnP K ⁡ P = f ∈ Y X | ∀ y ∈ K f ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ f x ⊆ y