Metamath Proof Explorer

Theorem cnpimaex

Description: Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006)

Ref Expression
Assertion cnpimaex ⊢ F ∈ J CnP K ⁡ P ∧ A ∈ K ∧ F ⁡ P ∈ A → ∃ x ∈ J P ∈ x ∧ F x ⊆ A

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 eqid ⊢ ⋃ K = ⋃ K
3 1 2 iscnp2 ⊢ F ∈ J CnP K ⁡ P ↔ J ∈ Top ∧ K ∈ Top ∧ P ∈ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
4 3 simprbi ⊢ F ∈ J CnP K ⁡ P → F : ⋃ J ⟶ ⋃ K ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
5 eleq2 ⊢ y = A → F ⁡ P ∈ y ↔ F ⁡ P ∈ A
6 sseq2 ⊢ y = A → F x ⊆ y ↔ F x ⊆ A
7 6 anbi2d ⊢ y = A → P ∈ x ∧ F x ⊆ y ↔ P ∈ x ∧ F x ⊆ A
8 7 rexbidv ⊢ y = A → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ ∃ x ∈ J P ∈ x ∧ F x ⊆ A
9 5 8 imbi12d ⊢ y = A → F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ F ⁡ P ∈ A → ∃ x ∈ J P ∈ x ∧ F x ⊆ A
10 9 rspccv ⊢ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → A ∈ K → F ⁡ P ∈ A → ∃ x ∈ J P ∈ x ∧ F x ⊆ A
11 4 10 simpl2im ⊢ F ∈ J CnP K ⁡ P → A ∈ K → F ⁡ P ∈ A → ∃ x ∈ J P ∈ x ∧ F x ⊆ A
12 11 3imp ⊢ F ∈ J CnP K ⁡ P ∧ A ∈ K ∧ F ⁡ P ∈ A → ∃ x ∈ J P ∈ x ∧ F x ⊆ A