ismtyhmeolem

	Ref	Expression
Hypotheses	ismtyhmeo.1	$⊢ J = MetOpen (M)$
	ismtyhmeo.2	$⊢ K = MetOpen (N)$
	ismtyhmeolem.3	$⊢ φ \to M \in ∞Met (X)$
	ismtyhmeolem.4	$⊢ φ \to N \in ∞Met (Y)$
	ismtyhmeolem.5	$⊢ φ \to F \in (M Ismty N)$
Assertion	ismtyhmeolem	$⊢ φ \to F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ismtyhmeo.1	$⊢ J = MetOpen (M)$
2		ismtyhmeo.2	$⊢ K = MetOpen (N)$
3		ismtyhmeolem.3	$⊢ φ \to M \in ∞Met (X)$
4		ismtyhmeolem.4	$⊢ φ \to N \in ∞Met (Y)$
5		ismtyhmeolem.5	$⊢ φ \to F \in (M Ismty N)$
6		isismty	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$
7	3 4 6	syl2anc	$⊢ φ \to (F \in (M Ismty N) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y)))$
8	5 7	mpbid	$⊢ φ \to (F : X \underset{1-1 onto}{⟶} Y \land \forall x \in X \forall y \in X x M y = F (x) N F (y))$
9	8	simpld	$⊢ φ \to F : X \underset{1-1 onto}{⟶} Y$
10		f1of	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X ⟶ Y$
11	9 10	syl	$⊢ φ \to F : X ⟶ Y$
12	4	adantr	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to N \in ∞Met (Y)$
13	3	adantr	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to M \in ∞Met (X)$
14		ismtycnv	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y)) \to (F \in (M Ismty N) \to F^{-1} \in (N Ismty M))$
15	3 4 14	syl2anc	$⊢ φ \to (F \in (M Ismty N) \to F^{-1} \in (N Ismty M))$
16	5 15	mpd	$⊢ φ \to F^{-1} \in (N Ismty M)$
17	16	adantr	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to F^{-1} \in (N Ismty M)$
18		simprl	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to w \in Y$
19		simprr	$⊢ (φ \land (w \in Y \land r \in ℝ^{})) \to r \in ℝ^{}$
20		ismtyima	$⊢ ((N \in ∞Met (Y) \land M \in ∞Met (X) \land F^{-1} \in (N Ismty M)) \land (w \in Y \land r \in ℝ^{*})) \to F^{-1} [w ball (N) r] = F^{-1} (w) ball (M) r$
21	12 13 17 18 19 20	syl32anc	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to F^{-1} [w ball (N) r] = F^{-1} (w) ball (M) r$
22		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
23		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
24	9 22 23	3syl	$⊢ φ \to F^{-1} : Y ⟶ X$
25		simpl	$⊢ (w \in Y \land r \in ℝ^{*}) \to w \in Y$
26		ffvelcdm	$⊢ (F^{-1} : Y ⟶ X \land w \in Y) \to F^{-1} (w) \in X$
27	24 25 26	syl2an	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to F^{-1} (w) \in X$
28	1	blopn	$⊢ (M \in ∞Met (X) \land F^{-1} (w) \in X \land r \in ℝ^{*}) \to F^{-1} (w) ball (M) r \in J$
29	13 27 19 28	syl3anc	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to F^{-1} (w) ball (M) r \in J$
30	21 29	eqeltrd	$⊢ (φ \land (w \in Y \land r \in ℝ^{*})) \to F^{-1} [w ball (N) r] \in J$
31	30	ralrimivva	$⊢ φ \to \forall w \in Y \forall r \in ℝ^{*} F^{-1} [w ball (N) r] \in J$
32		fveq2	$⊢ z = ⟨w, r⟩ \to 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⟩ \to ball (N) (z) = w ball (N) r$
35	34	imaeq2d	$⊢ z = ⟨w, r⟩ \to F^{-1} [ball (N) (z)] = F^{-1} [w ball (N) r]$
36	35	eleq1d	$⊢ z = ⟨w, r⟩ \to (F^{-1} [ball (N) (z)] \in J \leftrightarrow F^{-1} [w ball (N) r] \in J)$
37	36	ralxp	$⊢ \forall z \in (Y \times ℝ^{}) F^{-1} [ball (N) (z)] \in J \leftrightarrow \forall w \in Y \forall r \in ℝ^{} F^{-1} [w ball (N) r] \in J$
38	31 37	sylibr	$⊢ φ \to \forall z \in (Y \times ℝ^{*}) F^{-1} [ball (N) (z)] \in J$
39		blf	$⊢ N \in ∞Met (Y) \to ball (N) : Y \times ℝ^{*} ⟶ 𝒫 Y$
40		ffn	$⊢ ball (N) : Y \times ℝ^{} ⟶ 𝒫 Y \to ball (N) Fn (Y \times ℝ^{})$
41		imaeq2	$⊢ u = ball (N) (z) \to F^{-1} [u] = F^{-1} [ball (N) (z)]$
42	41	eleq1d	$⊢ u = ball (N) (z) \to (F^{-1} [u] \in J \leftrightarrow F^{-1} [ball (N) (z)] \in J)$
43	42	ralrn	$⊢ ball (N) Fn (Y \times ℝ^{}) \to (\forall u \in ran ball (N) F^{-1} [u] \in J \leftrightarrow \forall z \in (Y \times ℝ^{}) F^{-1} [ball (N) (z)] \in J)$
44	4 39 40 43	4syl	$⊢ φ \to (\forall u \in ran ball (N) F^{-1} [u] \in J \leftrightarrow \forall z \in (Y \times ℝ^{*}) F^{-1} [ball (N) (z)] \in J)$
45	38 44	mpbird	$⊢ φ \to \forall u \in ran ball (N) F^{-1} [u] \in J$
46	1	mopntopon	$⊢ M \in ∞Met (X) \to J \in TopOn (X)$
47	3 46	syl	$⊢ φ \to J \in TopOn (X)$
48	2	mopnval	$⊢ N \in ∞Met (Y) \to K = topGen (ran ball (N))$
49	4 48	syl	$⊢ φ \to K = topGen (ran ball (N))$
50	2	mopntopon	$⊢ N \in ∞Met (Y) \to K \in TopOn (Y)$
51	4 50	syl	$⊢ φ \to K \in TopOn (Y)$
52	47 49 51	tgcn	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall u \in ran ball (N) F^{-1} [u] \in J))$
53	11 45 52	mpbir2and	$⊢ φ \to F \in (J Cn K)$

Metamath Proof Explorer

Theorem ismtyhmeolem

Proof