Metamath Proof Explorer

Theorem cncls2

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

Ref Expression
Assertion cncls2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑌 ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑥 ) ) ) ) )

Proof

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