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

Metamath Proof Explorer

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 𝑋 ) )