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 ⊢ J = MetOpen ⁡ M
ismtyhmeo.2 ⊢ K = MetOpen ⁡ N
ismtyhmeolem.3 ⊢ φ → M ∈ ∞Met ⁡ X
ismtyhmeolem.4 ⊢ φ → N ∈ ∞Met ⁡ Y
ismtyhmeolem.5 ⊢ φ → F ∈ M Ismty N
Assertion ismtyhmeolem ⊢ φ → F ∈ J Cn K

Proof

Step Hyp Ref Expression
1 ismtyhmeo.1 ⊢ J = MetOpen ⁡ M
2 ismtyhmeo.2 ⊢ K = MetOpen ⁡ N
3 ismtyhmeolem.3 ⊢ φ → M ∈ ∞Met ⁡ X
4 ismtyhmeolem.4 ⊢ φ → N ∈ ∞Met ⁡ Y
5 ismtyhmeolem.5 ⊢ φ → F ∈ M Ismty N
6 isismty ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F ∈ M Ismty N ↔ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y
7 3 4 6 syl2anc ⊢ φ → F ∈ M Ismty N ↔ F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y
8 5 7 mpbid ⊢ φ → F : X ⟶ 1-1 onto Y ∧ ∀ x ∈ X ∀ y ∈ X x M y = F ⁡ x N F ⁡ y
9 8 simpld ⊢ φ → F : X ⟶ 1-1 onto Y
10 f1of ⊢ F : X ⟶ 1-1 onto Y → F : X ⟶ Y
11 9 10 syl ⊢ φ → F : X ⟶ Y
12 4 adantr ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → N ∈ ∞Met ⁡ Y
13 3 adantr ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → M ∈ ∞Met ⁡ X
14 ismtycnv ⊢ M ∈ ∞Met ⁡ X ∧ N ∈ ∞Met ⁡ Y → F ∈ M Ismty N → F -1 ∈ N Ismty M
15 3 4 14 syl2anc ⊢ φ → F ∈ M Ismty N → F -1 ∈ N Ismty M
16 5 15 mpd ⊢ φ → F -1 ∈ N Ismty M
17 16 adantr ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → F -1 ∈ N Ismty M
18 simprl ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → w ∈ Y
19 simprr ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → r ∈ ℝ *
20 ismtyima ⊢ N ∈ ∞Met ⁡ Y ∧ M ∈ ∞Met ⁡ X ∧ F -1 ∈ N Ismty M ∧ w ∈ Y ∧ r ∈ ℝ * → F -1 w ball ⁡ N r = F -1 ⁡ w ball ⁡ M r
21 12 13 17 18 19 20 syl32anc ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → F -1 w ball ⁡ N r = F -1 ⁡ w ball ⁡ M r
22 f1ocnv ⊢ F : X ⟶ 1-1 onto Y → F -1 : Y ⟶ 1-1 onto X
23 f1of ⊢ F -1 : Y ⟶ 1-1 onto X → F -1 : Y ⟶ X
24 9 22 23 3syl ⊢ φ → F -1 : Y ⟶ X
25 simpl ⊢ w ∈ Y ∧ r ∈ ℝ * → w ∈ Y
26 ffvelcdm ⊢ F -1 : Y ⟶ X ∧ w ∈ Y → F -1 ⁡ w ∈ X
27 24 25 26 syl2an ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → F -1 ⁡ w ∈ X
28 1 blopn ⊢ M ∈ ∞Met ⁡ X ∧ F -1 ⁡ w ∈ X ∧ r ∈ ℝ * → F -1 ⁡ w ball ⁡ M r ∈ J
29 13 27 19 28 syl3anc ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → F -1 ⁡ w ball ⁡ M r ∈ J
30 21 29 eqeltrd ⊢ φ ∧ w ∈ Y ∧ r ∈ ℝ * → F -1 w ball ⁡ N r ∈ J
31 30 ralrimivva ⊢ φ → ∀ w ∈ Y ∀ r ∈ ℝ * F -1 w ball ⁡ N r ∈ J
32 fveq2 ⊢ z = w r → ball ⁡ N ⁡ z = ball ⁡ N ⁡ w r
33 df-ov ⊢ w ball ⁡ N r = ball ⁡ N ⁡ w r
34 32 33 eqtr4di ⊢ z = w r → ball ⁡ N ⁡ z = w ball ⁡ N r
35 34 imaeq2d ⊢ z = w r → F -1 ball ⁡ N ⁡ z = F -1 w ball ⁡ N r
36 35 eleq1d ⊢ z = w r → F -1 ball ⁡ N ⁡ z ∈ J ↔ F -1 w ball ⁡ N r ∈ J
37 36 ralxp ⊢ ∀ z ∈ Y × ℝ * F -1 ball ⁡ N ⁡ z ∈ J ↔ ∀ w ∈ Y ∀ r ∈ ℝ * F -1 w ball ⁡ N r ∈ J
38 31 37 sylibr ⊢ φ → ∀ z ∈ Y × ℝ * F -1 ball ⁡ N ⁡ z ∈ J
39 blf ⊢ N ∈ ∞Met ⁡ Y → ball ⁡ N : Y × ℝ * ⟶ 𝒫 Y
40 ffn ⊢ ball ⁡ N : Y × ℝ * ⟶ 𝒫 Y → ball ⁡ N Fn Y × ℝ *
41 imaeq2 ⊢ u = ball ⁡ N ⁡ z → F -1 u = F -1 ball ⁡ N ⁡ z
42 41 eleq1d ⊢ u = ball ⁡ N ⁡ z → F -1 u ∈ J ↔ F -1 ball ⁡ N ⁡ z ∈ J
43 42 ralrn ⊢ ball ⁡ N Fn Y × ℝ * → ∀ u ∈ ran ⁡ ball ⁡ N F -1 u ∈ J ↔ ∀ z ∈ Y × ℝ * F -1 ball ⁡ N ⁡ z ∈ J
44 4 39 40 43 4syl ⊢ φ → ∀ u ∈ ran ⁡ ball ⁡ N F -1 u ∈ J ↔ ∀ z ∈ Y × ℝ * F -1 ball ⁡ N ⁡ z ∈ J
45 38 44 mpbird ⊢ φ → ∀ u ∈ ran ⁡ ball ⁡ N F -1 u ∈ J
46 1 mopntopon ⊢ M ∈ ∞Met ⁡ X → J ∈ TopOn ⁡ X
47 3 46 syl ⊢ φ → J ∈ TopOn ⁡ X
48 2 mopnval ⊢ N ∈ ∞Met ⁡ Y → K = topGen ⁡ ran ⁡ ball ⁡ N
49 4 48 syl ⊢ φ → K = topGen ⁡ ran ⁡ ball ⁡ N
50 2 mopntopon ⊢ N ∈ ∞Met ⁡ Y → K ∈ TopOn ⁡ Y
51 4 50 syl ⊢ φ → K ∈ TopOn ⁡ Y
52 47 49 51 tgcn ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ u ∈ ran ⁡ ball ⁡ N F -1 u ∈ J
53 11 45 52 mpbir2and ⊢ φ → F ∈ J Cn K