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 ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → 𝒫 A Cn J = X A

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ f -1 x ⊆ dom ⁡ f
2 fdm ⊢ f : A ⟶ X → dom ⁡ f = A
3 2 adantl ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X ∧ f : A ⟶ X → dom ⁡ f = A
4 1 3 sseqtrid ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X ∧ f : A ⟶ X → f -1 x ⊆ A
5 elpw2g ⊢ A ∈ V → f -1 x ∈ 𝒫 A ↔ f -1 x ⊆ A
6 5 ad2antrr ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X ∧ f : A ⟶ X → f -1 x ∈ 𝒫 A ↔ f -1 x ⊆ A
7 4 6 mpbird ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X ∧ f : A ⟶ X → f -1 x ∈ 𝒫 A
8 7 ralrimivw ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X ∧ f : A ⟶ X → ∀ x ∈ J f -1 x ∈ 𝒫 A
9 8 ex ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → f : A ⟶ X → ∀ x ∈ J f -1 x ∈ 𝒫 A
10 9 pm4.71d ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → f : A ⟶ X ↔ f : A ⟶ X ∧ ∀ x ∈ J f -1 x ∈ 𝒫 A
11 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
12 id ⊢ A ∈ V → A ∈ V
13 elmapg ⊢ X ∈ J ∧ A ∈ V → f ∈ X A ↔ f : A ⟶ X
14 11 12 13 syl2anr ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → f ∈ X A ↔ f : A ⟶ X
15 distopon ⊢ A ∈ V → 𝒫 A ∈ TopOn ⁡ A
16 iscn ⊢ 𝒫 A ∈ TopOn ⁡ A ∧ J ∈ TopOn ⁡ X → f ∈ 𝒫 A Cn J ↔ f : A ⟶ X ∧ ∀ x ∈ J f -1 x ∈ 𝒫 A
17 15 16 sylan ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → f ∈ 𝒫 A Cn J ↔ f : A ⟶ X ∧ ∀ x ∈ J f -1 x ∈ 𝒫 A
18 10 14 17 3bitr4rd ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → f ∈ 𝒫 A Cn J ↔ f ∈ X A
19 18 eqrdv ⊢ A ∈ V ∧ J ∈ TopOn ⁡ X → 𝒫 A Cn J = X A