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