This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnpimaex

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

Ref Expression
Assertion cnpimaex ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
3 1 2 iscnp2 ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽 ) ∧ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
4 3 simprbi ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
5 eleq2 ⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) )
6 sseq2 ⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )
7 6 anbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )
8 7 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) )
9 5 8 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) ) )
10 9 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( 𝐴 ∈ 𝐾 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) ) )
11 4 10 simpl2im ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐴 ∈ 𝐾 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) ) ) )
12 11 3imp ⊢ ( ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ 𝐾 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) )