Theorem iscnp

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	iscnp	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnpval	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } )
2	1	eleq2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ) )
3		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑃 ) = ( 𝐹 ‘ 𝑃 ) )
4	3	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ) )
5		imaeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ 𝑥 ) = ( 𝐹 “ 𝑥 ) )
6	5	sseq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ↔ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) )
7	6	anbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ↔ ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )
8	7	rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) )
9	4 8	imbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
10	9	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
11	10	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ↔ ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
12		toponmax	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
13		toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
14		elmapg	⊢ ( ( 𝑌 ∈ 𝐾 ∧ 𝑋 ∈ 𝐽 ) → ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
15	12 13 14	syl2anr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
16	15	anbi1d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
17	11 16	syl5bb	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
18	17	3adant3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ( 𝑓 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝑦 ) ) } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
19	2 18	bitrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )