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 ffvelrn 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