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

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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 cnpfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 CnP 𝐾 ) = ( 𝑣 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ) )
2 1 fveq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = ( ( 𝑣 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ) ‘ 𝑃 ) )
3 fveq2 ⊢ ( 𝑣 = 𝑃 → ( 𝑓 ‘ 𝑣 ) = ( 𝑓 ‘ 𝑃 ) )
4 3 eleq1d ⊢ ( 𝑣 = 𝑃 → ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 ↔ ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 ) )
5 eleq1 ⊢ ( 𝑣 = 𝑃 → ( 𝑣 ∈ 𝑥 ↔ 𝑃 ∈ 𝑥 ) )
6 5 anbi1d ⊢ ( 𝑣 = 𝑃 → ( ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) )
7 6 rexbidv ⊢ ( 𝑣 = 𝑃 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) )
8 4 7 imbi12d ⊢ ( 𝑣 = 𝑃 → ( ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
9 8 ralbidv ⊢ ( 𝑣 = 𝑃 → ( ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
10 9 rabbidv ⊢ ( 𝑣 = 𝑃 → { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )
11 eqid ⊢ ( 𝑣 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ) = ( 𝑣 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )
12 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
13 12 rabex ⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ∈ V
14 10 11 13 fvmpt ⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑣 ∈ 𝑋 ↦ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑣 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑣 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ) ‘ 𝑃 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )
15 2 14 sylan9eq ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )
16 15 3impa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )