Metamath Proof Explorer

Theorem cnindis

Description: Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnindis ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J Cn ∅ A = A X

Proof

Step Hyp Ref Expression
1 elpri ⊢ x ∈ ∅ A → x = ∅ ∨ x = A
2 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
3 2 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → J ∈ Top
4 0opn ⊢ J ∈ Top → ∅ ∈ J
5 3 4 syl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → ∅ ∈ J
6 imaeq2 ⊢ x = ∅ → f -1 x = f -1 ∅
7 ima0 ⊢ f -1 ∅ = ∅
8 6 7 eqtrdi ⊢ x = ∅ → f -1 x = ∅
9 8 eleq1d ⊢ x = ∅ → f -1 x ∈ J ↔ ∅ ∈ J
10 5 9 syl5ibrcom ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → x = ∅ → f -1 x ∈ J
11 fimacnv ⊢ f : X ⟶ A → f -1 A = X
12 11 adantl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → f -1 A = X
13 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
14 13 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → X ∈ J
15 12 14 eqeltrd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → f -1 A ∈ J
16 imaeq2 ⊢ x = A → f -1 x = f -1 A
17 16 eleq1d ⊢ x = A → f -1 x ∈ J ↔ f -1 A ∈ J
18 15 17 syl5ibrcom ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → x = A → f -1 x ∈ J
19 10 18 jaod ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → x = ∅ ∨ x = A → f -1 x ∈ J
20 1 19 syl5 ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → x ∈ ∅ A → f -1 x ∈ J
21 20 ralrimiv ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V ∧ f : X ⟶ A → ∀ x ∈ ∅ A f -1 x ∈ J
22 21 ex ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → f : X ⟶ A → ∀ x ∈ ∅ A f -1 x ∈ J
23 22 pm4.71d ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → f : X ⟶ A ↔ f : X ⟶ A ∧ ∀ x ∈ ∅ A f -1 x ∈ J
24 id ⊢ A ∈ V → A ∈ V
25 elmapg ⊢ A ∈ V ∧ X ∈ J → f ∈ A X ↔ f : X ⟶ A
26 24 13 25 syl2anr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → f ∈ A X ↔ f : X ⟶ A
27 indistopon ⊢ A ∈ V → ∅ A ∈ TopOn ⁡ A
28 iscn ⊢ J ∈ TopOn ⁡ X ∧ ∅ A ∈ TopOn ⁡ A → f ∈ J Cn ∅ A ↔ f : X ⟶ A ∧ ∀ x ∈ ∅ A f -1 x ∈ J
29 27 28 sylan2 ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → f ∈ J Cn ∅ A ↔ f : X ⟶ A ∧ ∀ x ∈ ∅ A f -1 x ∈ J
30 23 26 29 3bitr4rd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → f ∈ J Cn ∅ A ↔ f ∈ A X
31 30 eqrdv ⊢ J ∈ TopOn ⁡ X ∧ A ∈ V → J Cn ∅ A = A X