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 ffvelrn ( ( 𝐹 : 𝑌𝑋𝑤𝑌 ) → ( 𝐹𝑤 ) ∈ 𝑋 )
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 𝐾 ) )