Theorem cnpdis

Description: If A is an isolated point in X (or equivalently, the singleton { A } is open in X ), then every function is continuous at A . (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Assertion	cnpdis	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) = ( 𝑌 ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		simplrl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → { 𝐴 } ∈ 𝐽 )
2		simpll3	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → 𝐴 ∈ 𝑋 )
3		snidg	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 } )
4	2 3	syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → 𝐴 ∈ { 𝐴 } )
5		simprr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 )
6		simplrr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → 𝑓 : 𝑋 ⟶ 𝑌 )
7		ffn	⊢ ( 𝑓 : 𝑋 ⟶ 𝑌 → 𝑓 Fn 𝑋 )
8		elpreima	⊢ ( 𝑓 Fn 𝑋 → ( 𝐴 ∈ ( ◡ 𝑓 “ 𝑥 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) )
9	6 7 8	3syl	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → ( 𝐴 ∈ ( ◡ 𝑓 “ 𝑥 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) )
10	2 5 9	mpbir2and	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → 𝐴 ∈ ( ◡ 𝑓 “ 𝑥 ) )
11	10	snssd	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → { 𝐴 } ⊆ ( ◡ 𝑓 “ 𝑥 ) )
12		eleq2	⊢ ( 𝑦 = { 𝐴 } → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ { 𝐴 } ) )
13		sseq1	⊢ ( 𝑦 = { 𝐴 } → ( 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ↔ { 𝐴 } ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
14	12 13	anbi12d	⊢ ( 𝑦 = { 𝐴 } → ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ↔ ( 𝐴 ∈ { 𝐴 } ∧ { 𝐴 } ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) )
15	14	rspcev	⊢ ( ( { 𝐴 } ∈ 𝐽 ∧ ( 𝐴 ∈ { 𝐴 } ∧ { 𝐴 } ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
16	1 4 11 15	syl12anc	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
17	16	expr	⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) )
18	17	ralrimiva	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( { 𝐴 } ∈ 𝐽 ∧ 𝑓 : 𝑋 ⟶ 𝑌 ) ) → ∀ 𝑥 ∈ 𝐾 ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) )
19	18	expr	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( 𝑓 : 𝑋 ⟶ 𝑌 → ∀ 𝑥 ∈ 𝐾 ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) )
20	19	pm4.71d	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( 𝑓 : 𝑋 ⟶ 𝑌 ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) ) )
21		simpl2	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
22		toponmax	⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
23	21 22	syl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → 𝑌 ∈ 𝐾 )
24		simpl1	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
25		toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
26	24 25	syl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → 𝑋 ∈ 𝐽 )
27	23 26	elmapd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
28		iscnp3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑓 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) ) )
29	28	adantr	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( 𝑓 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑥 → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) ) )
30	20 27 29	3bitr4rd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( 𝑓 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ) )
31	30	eqrdv	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ { 𝐴 } ∈ 𝐽 ) → ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) = ( 𝑌 ↑m 𝑋 ) )