Metamath Proof Explorer

Theorem cnntr

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

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

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 cnntri ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ⊆ ∪ 𝐾 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) )
10 9 expcom ⊢ ( 𝑥 ⊆ ∪ 𝐾 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
11 7 10 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝒫 𝑌 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
12 11 ralrimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ∀ 𝑥 ∈ 𝒫 𝑌 ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
13 2 12 jcad ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑌 ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
14 toponss ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ⊆ 𝑌 )
15 velpw ⊢ ( 𝑥 ∈ 𝒫 𝑌 ↔ 𝑥 ⊆ 𝑌 )
16 14 15 sylibr ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ 𝒫 𝑌 )
17 16 ex ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → ( 𝑥 ∈ 𝐾 → 𝑥 ∈ 𝒫 𝑌 ) )
18 17 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑥 ∈ 𝐾 → 𝑥 ∈ 𝒫 𝑌 ) )
19 18 imim1d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑥 ∈ 𝒫 𝑌 → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝑥 ∈ 𝐾 → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )
20 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
21 20 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐽 ∈ Top )
22 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
23 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
24 23 ad2antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → dom 𝐹 = 𝑋 )
25 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
26 25 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑋 = ∪ 𝐽 )
27 24 26 eqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → dom 𝐹 = ∪ 𝐽 )
28 22 27 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ 𝐽 )
29 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
30 29 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 ) )
31 21 28 30 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 ) )
32 eqss ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) = ( ◡ 𝐹 “ 𝑥 ) ↔ ( ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 ) ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
33 32 baib ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 ) → ( ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) = ( ◡ 𝐹 “ 𝑥 ) ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
34 31 33 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) = ( ◡ 𝐹 “ 𝑥 ) ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
35 29 isopn3 ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ 𝐽 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) = ( ◡ 𝐹 “ 𝑥 ) ) )
36 21 28 35 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) = ( ◡ 𝐹 “ 𝑥 ) ) )
37 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
38 37 ad3antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → 𝐾 ∈ Top )
39 isopn3i ⊢ ( ( 𝐾 ∈ Top ∧ 𝑥 ∈ 𝐾 ) → ( ( int ‘ 𝐾 ) ‘ 𝑥 ) = 𝑥 )
40 38 39 sylancom ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( int ‘ 𝐾 ) ‘ 𝑥 ) = 𝑥 )
41 40 imaeq2d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
42 41 sseq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) )
43 34 36 42 3bitr4rd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
44 43 pm5.74da ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑥 ∈ 𝐾 → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐾 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
45 19 44 sylibd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑥 ∈ 𝒫 𝑌 → ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝑥 ∈ 𝐾 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
46 45 ralimdv2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝒫 𝑌 ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
47 46 imdistanda ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑌 ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
48 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
49 47 48 sylibrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑌 ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) )
50 13 49 impbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝒫 𝑌 ( ◡ 𝐹 “ ( ( int ‘ 𝐾 ) ‘ 𝑥 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑥 ) ) ) ) )