Metamath Proof Explorer

Theorem cncls2

Description: Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cncls2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x

Proof

Step Hyp Ref Expression
1 cnf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Cn K → F : X ⟶ Y
2 1 3expia ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K → F : X ⟶ Y
3 elpwi ⊢ x ∈ 𝒫 Y → x ⊆ Y
4 3 adantl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ 𝒫 Y → x ⊆ Y
5 toponuni ⊢ K ∈ TopOn ⁡ Y → Y = ⋃ K
6 5 ad2antlr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ 𝒫 Y → Y = ⋃ K
7 4 6 sseqtrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ 𝒫 Y → x ⊆ ⋃ K
8 eqid ⊢ ⋃ K = ⋃ K
9 8 cncls2i ⊢ F ∈ J Cn K ∧ x ⊆ ⋃ K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x
10 9 expcom ⊢ x ⊆ ⋃ K → F ∈ J Cn K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x
11 7 10 syl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ 𝒫 Y → F ∈ J Cn K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x
12 11 ralrimdva ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K → ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x
13 2 12 jcad ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K → F : X ⟶ Y ∧ ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x
14 8 cldss2 ⊢ Clsd ⁡ K ⊆ 𝒫 ⋃ K
15 5 ad2antlr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → Y = ⋃ K
16 15 pweqd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → 𝒫 Y = 𝒫 ⋃ K
17 14 16 sseqtrrid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → Clsd ⁡ K ⊆ 𝒫 Y
18 17 sseld ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ Clsd ⁡ K → x ∈ 𝒫 Y
19 18 imim1d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ 𝒫 Y → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x → x ∈ Clsd ⁡ K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x
20 cldcls ⊢ x ∈ Clsd ⁡ K → cls ⁡ K ⁡ x = x
21 20 ad2antll ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → cls ⁡ K ⁡ x = x
22 21 imaeq2d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → F -1 cls ⁡ K ⁡ x = F -1 x
23 22 sseq2d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x ↔ cls ⁡ J ⁡ F -1 x ⊆ F -1 x
24 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
25 24 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → J ∈ Top
26 cnvimass ⊢ F -1 x ⊆ dom ⁡ F
27 fdm ⊢ F : X ⟶ Y → dom ⁡ F = X
28 27 ad2antrl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → dom ⁡ F = X
29 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
30 29 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → X = ⋃ J
31 28 30 eqtrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → dom ⁡ F = ⋃ J
32 26 31 sseqtrid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → F -1 x ⊆ ⋃ J
33 eqid ⊢ ⋃ J = ⋃ J
34 33 iscld4 ⊢ J ∈ Top ∧ F -1 x ⊆ ⋃ J → F -1 x ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ F -1 x ⊆ F -1 x
35 25 32 34 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → F -1 x ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ F -1 x ⊆ F -1 x
36 23 35 bitr4d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ Clsd ⁡ K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x ↔ F -1 x ∈ Clsd ⁡ J
37 36 expr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ Clsd ⁡ K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x ↔ F -1 x ∈ Clsd ⁡ J
38 37 pm5.74d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ Clsd ⁡ K → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x ↔ x ∈ Clsd ⁡ K → F -1 x ∈ Clsd ⁡ J
39 19 38 sylibd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ 𝒫 Y → cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x → x ∈ Clsd ⁡ K → F -1 x ∈ Clsd ⁡ J
40 39 ralimdv2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x → ∀ x ∈ Clsd ⁡ K F -1 x ∈ Clsd ⁡ J
41 40 imdistanda ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F : X ⟶ Y ∧ ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x → F : X ⟶ Y ∧ ∀ x ∈ Clsd ⁡ K F -1 x ∈ Clsd ⁡ J
42 iscncl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ Clsd ⁡ K F -1 x ∈ Clsd ⁡ J
43 41 42 sylibrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F : X ⟶ Y ∧ ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x → F ∈ J Cn K
44 13 43 impbid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ 𝒫 Y cls ⁡ J ⁡ F -1 x ⊆ F -1 cls ⁡ K ⁡ x