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 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )