Metamath Proof Explorer

Theorem ismtyhmeolem

Description: Lemma for ismtyhmeo . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses ismtyhmeo.1 ⊢ 𝐽 = ( MetOpen ‘ 𝑀 )
ismtyhmeo.2 ⊢ 𝐾 = ( MetOpen ‘ 𝑁 )
ismtyhmeolem.3 ⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
ismtyhmeolem.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
ismtyhmeolem.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) )
Assertion ismtyhmeolem ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ismtyhmeo.1 ⊢ 𝐽 = ( MetOpen ‘ 𝑀 )
2 ismtyhmeo.2 ⊢ 𝐾 = ( MetOpen ‘ 𝑁 )
3 ismtyhmeolem.3 ⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
4 ismtyhmeolem.4 ⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
5 ismtyhmeolem.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) )
6 isismty ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
7 3 4 6 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) ↔ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) ) )
8 5 7 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑁 ( 𝐹 ‘ 𝑦 ) ) ) )
9 8 simpld ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
10 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
11 9 10 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
12 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
14 ismtycnv ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) )
15 3 4 14 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑀 Ismty 𝑁 ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) )
16 5 15 mpd ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → 𝑤 ∈ 𝑌 )
19 simprr ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → 𝑟 ∈ ℝ* )
20 ismtyima ⊢ ( ( ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ◡ 𝐹 ∈ ( 𝑁 Ismty 𝑀 ) ) ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) = ( ( ◡ 𝐹 ‘ 𝑤 ) ( ball ‘ 𝑀 ) 𝑟 ) )
21 12 13 17 18 19 20 syl32anc ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) = ( ( ◡ 𝐹 ‘ 𝑤 ) ( ball ‘ 𝑀 ) 𝑟 ) )
22 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
23 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
24 9 22 23 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
25 simpl ⊢ ( ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) → 𝑤 ∈ 𝑌 )
26 ffvelcdm ⊢ ( ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑤 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑤 ) ∈ 𝑋 )
27 24 25 26 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → ( ◡ 𝐹 ‘ 𝑤 ) ∈ 𝑋 )
28 1 blopn ⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ◡ 𝐹 ‘ 𝑤 ) ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( ( ◡ 𝐹 ‘ 𝑤 ) ( ball ‘ 𝑀 ) 𝑟 ) ∈ 𝐽 )
29 13 27 19 28 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → ( ( ◡ 𝐹 ‘ 𝑤 ) ( ball ‘ 𝑀 ) 𝑟 ) ∈ 𝐽 )
30 21 29 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑌 ∧ 𝑟 ∈ ℝ* ) ) → ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) ∈ 𝐽 )
31 30 ralrimivva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑌 ∀ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) ∈ 𝐽 )
32 fveq2 ⊢ ( 𝑧 = ⟨ 𝑤 , 𝑟 ⟩ → ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) = ( ( ball ‘ 𝑁 ) ‘ ⟨ 𝑤 , 𝑟 ⟩ ) )
33 df-ov ⊢ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) = ( ( ball ‘ 𝑁 ) ‘ ⟨ 𝑤 , 𝑟 ⟩ )
34 32 33 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑤 , 𝑟 ⟩ → ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) = ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) )
35 34 imaeq2d ⊢ ( 𝑧 = ⟨ 𝑤 , 𝑟 ⟩ → ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) = ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) )
36 35 eleq1d ⊢ ( 𝑧 = ⟨ 𝑤 , 𝑟 ⟩ → ( ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) ∈ 𝐽 ) )
37 36 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝑌 × ℝ* ) ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) ∈ 𝐽 ↔ ∀ 𝑤 ∈ 𝑌 ∀ 𝑟 ∈ ℝ* ( ◡ 𝐹 “ ( 𝑤 ( ball ‘ 𝑁 ) 𝑟 ) ) ∈ 𝐽 )
38 31 37 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 × ℝ* ) ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) ∈ 𝐽 )
39 blf ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → ( ball ‘ 𝑁 ) : ( 𝑌 × ℝ* ) ⟶ 𝒫 𝑌 )
40 ffn ⊢ ( ( ball ‘ 𝑁 ) : ( 𝑌 × ℝ* ) ⟶ 𝒫 𝑌 → ( ball ‘ 𝑁 ) Fn ( 𝑌 × ℝ* ) )
41 imaeq2 ⊢ ( 𝑢 = ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) → ( ◡ 𝐹 “ 𝑢 ) = ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) )
42 41 eleq1d ⊢ ( 𝑢 = ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) → ( ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) ∈ 𝐽 ) )
43 42 ralrn ⊢ ( ( ball ‘ 𝑁 ) Fn ( 𝑌 × ℝ* ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝑁 ) ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 ↔ ∀ 𝑧 ∈ ( 𝑌 × ℝ* ) ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) ∈ 𝐽 ) )
44 4 39 40 43 4syl ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝑁 ) ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 ↔ ∀ 𝑧 ∈ ( 𝑌 × ℝ* ) ( ◡ 𝐹 “ ( ( ball ‘ 𝑁 ) ‘ 𝑧 ) ) ∈ 𝐽 ) )
45 38 44 mpbird ⊢ ( 𝜑 → ∀ 𝑢 ∈ ran ( ball ‘ 𝑁 ) ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 )
46 1 mopntopon ⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
47 3 46 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
48 2 mopnval ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝑁 ) ) )
49 4 48 syl ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝑁 ) ) )
50 2 mopntopon ⊢ ( 𝑁 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
51 4 50 syl ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
52 47 49 51 tgcn ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ ran ( ball ‘ 𝑁 ) ( ◡ 𝐹 “ 𝑢 ) ∈ 𝐽 ) ) )
53 11 45 52 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )