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

Metamath Proof Explorer

Theorem cndis

Description: Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cndis ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝐴 Cn 𝐽 ) = ( 𝑋 ↑m 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ ( ◡ 𝑓 “ 𝑥 ) ⊆ dom 𝑓
2 fdm ⊢ ( 𝑓 : 𝐴 ⟶ 𝑋 → dom 𝑓 = 𝐴 )
3 2 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑓 : 𝐴 ⟶ 𝑋 ) → dom 𝑓 = 𝐴 )
4 1 3 sseqtrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑓 : 𝐴 ⟶ 𝑋 ) → ( ◡ 𝑓 “ 𝑥 ) ⊆ 𝐴 )
5 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ↔ ( ◡ 𝑓 “ 𝑥 ) ⊆ 𝐴 ) )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑓 : 𝐴 ⟶ 𝑋 ) → ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ↔ ( ◡ 𝑓 “ 𝑥 ) ⊆ 𝐴 ) )
7 4 6 mpbird ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑓 : 𝐴 ⟶ 𝑋 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 )
8 7 ralrimivw ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑓 : 𝐴 ⟶ 𝑋 ) → ∀ 𝑥 ∈ 𝐽 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 )
9 8 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑓 : 𝐴 ⟶ 𝑋 → ∀ 𝑥 ∈ 𝐽 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ) )
10 9 pm4.71d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑓 : 𝐴 ⟶ 𝑋 ↔ ( 𝑓 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ) ) )
11 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
12 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
13 elmapg ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑓 ∈ ( 𝑋 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝑋 ) )
14 11 12 13 syl2anr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑓 ∈ ( 𝑋 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝑋 ) )
15 distopon ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) )
16 iscn ⊢ ( ( 𝒫 𝐴 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑓 ∈ ( 𝒫 𝐴 Cn 𝐽 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ) ) )
17 15 16 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑓 ∈ ( 𝒫 𝐴 Cn 𝐽 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝒫 𝐴 ) ) )
18 10 14 17 3bitr4rd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑓 ∈ ( 𝒫 𝐴 Cn 𝐽 ) ↔ 𝑓 ∈ ( 𝑋 ↑m 𝐴 ) ) )
19 18 eqrdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝐴 Cn 𝐽 ) = ( 𝑋 ↑m 𝐴 ) )