Metamath Proof Explorer

Theorem cncls

Description: Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cncls ( ( 𝐽 ∈ ( 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 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑋 = ∪ 𝐽 )
7 4 6 sseqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑥 ⊆ ∪ 𝐽 )
8 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
9 8 cnclsi ⊢ ( ( 𝐹 ∈ ( 𝐽 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 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
15 14 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝑋 ∈ 𝐽 )
16 cnvimass ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹
17 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
18 17 ad2antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → dom 𝐹 = 𝑋 )
19 16 18 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
20 15 19 sselpwd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝒫 𝑋 )
21 fveq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) )
22 21 imaeq2d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) = ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) )
23 imaeq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) )
24 23 fveq2d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) = ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) )
25 22 24 sseq12d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) ↔ ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
26 25 rspcv ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝒫 𝑋 → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
27 20 26 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) )
28 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
29 28 ad3antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝐾 ∈ Top )
30 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑌 → 𝑦 ⊆ 𝑌 )
31 30 adantl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝑦 ⊆ 𝑌 )
32 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
33 32 ad3antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝑌 = ∪ 𝐾 )
34 31 33 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝑦 ⊆ ∪ 𝐾 )
35 ffun ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
36 35 ad2antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → Fun 𝐹 )
37 funimacnv ⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = ( 𝑦 ∩ ran 𝐹 ) )
38 36 37 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = ( 𝑦 ∩ ran 𝐹 ) )
39 inss1 ⊢ ( 𝑦 ∩ ran 𝐹 ) ⊆ 𝑦
40 38 39 eqsstrdi ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ 𝑦 )
41 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
42 41 clsss ⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾 ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ 𝑦 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) )
43 29 34 40 42 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) )
44 sstr2 ⊢ ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) → ( ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) )
45 43 44 syl5com ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) → ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) )
46 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
47 46 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝐽 ∈ Top )
48 5 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → 𝑋 = ∪ 𝐽 )
49 18 48 eqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → dom 𝐹 = ∪ 𝐽 )
50 16 49 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ ∪ 𝐽 )
51 8 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑦 ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ∪ 𝐽 )
52 47 50 51 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ∪ 𝐽 )
53 52 49 sseqtrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ dom 𝐹 )
54 funimass3 ⊢ ( ( Fun 𝐹 ∧ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
55 36 53 54 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
56 45 55 sylibd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
57 27 56 syld ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ 𝒫 𝑌 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
58 57 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) → ∀ 𝑦 ∈ 𝒫 𝑌 ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) )
59 58 imdistanda ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝒫 𝑌 ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) )
60 cncls2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝒫 𝑌 ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑦 ) ) ) ) )
61 59 60 sylibrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) )
62 13 61 impbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝐹 “ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( ( cls ‘ 𝐾 ) ‘ ( 𝐹 “ 𝑥 ) ) ) ) )