ismtybndlem

		Ref	Expression
	Assertion	ismtybndlem	$⊢ (N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in Bnd (X) \to N \in Bnd (Y))$

Proof

Step	Hyp	Ref	Expression
1		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 z \in X \forall w \in X z M w = F (z) N F (w)))$
2	1	biimp3a	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (F : X \underset{1-1 onto}{⟶} Y \land \forall z \in X \forall w \in X z M w = F (z) N F (w))$
3	2	simpld	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to F : X \underset{1-1 onto}{⟶} Y$
4		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
5		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
6	3 4 5	3syl	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to F^{-1} : Y ⟶ X$
7	6	ffvelrnda	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land y \in Y) \to F^{-1} (y) \in X$
8		oveq1	$⊢ x = F^{-1} (y) \to x ball (M) r = F^{-1} (y) ball (M) r$
9	8	eqeq2d	$⊢ x = F^{-1} (y) \to (X = x ball (M) r \leftrightarrow X = F^{-1} (y) ball (M) r)$
10	9	rexbidv	$⊢ x = F^{-1} (y) \to (\exists r \in ℝ^{+} X = x ball (M) r \leftrightarrow \exists r \in ℝ^{+} X = F^{-1} (y) ball (M) r)$
11	10	rspcv	$⊢ F^{-1} (y) \in X \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to \exists r \in ℝ^{+} X = F^{-1} (y) ball (M) r)$
12	7 11	syl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land y \in Y) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to \exists r \in ℝ^{+} X = F^{-1} (y) ball (M) r)$
13		imaeq2	$⊢ X = F^{-1} (y) ball (M) r \to F [X] = F [F^{-1} (y) ball (M) r]$
14		f1ofo	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{onto}{⟶} Y$
15		foima	$⊢ F : X \underset{onto}{⟶} Y \to F [X] = Y$
16	3 14 15	3syl	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to F [X] = Y$
17	16	adantr	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to F [X] = Y$
18		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
19	18	adantl	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land r \in ℝ^{+}) \to r \in ℝ^{*}$
20	7 19	anim12dan	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to (F^{-1} (y) \in X \land r \in ℝ^{*})$
21		ismtyima	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (F^{-1} (y) \in X \land r \in ℝ^{*})) \to F [F^{-1} (y) ball (M) r] = F (F^{-1} (y)) ball (N) r$
22	20 21	syldan	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to F [F^{-1} (y) ball (M) r] = F (F^{-1} (y)) ball (N) r$
23		simpl	$⊢ (y \in Y \land r \in ℝ^{+}) \to y \in Y$
24		f1ocnvfv2	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land y \in Y) \to F (F^{-1} (y)) = y$
25	3 23 24	syl2an	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to F (F^{-1} (y)) = y$
26	25	oveq1d	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to F (F^{-1} (y)) ball (N) r = y ball (N) r$
27	22 26	eqtrd	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to F [F^{-1} (y) ball (M) r] = y ball (N) r$
28	17 27	eqeq12d	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to (F [X] = F [F^{-1} (y) ball (M) r] \leftrightarrow Y = y ball (N) r)$
29	13 28	syl5ib	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land (y \in Y \land r \in ℝ^{+})) \to (X = F^{-1} (y) ball (M) r \to Y = y ball (N) r)$
30	29	anassrs	$⊢ (((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land y \in Y) \land r \in ℝ^{+}) \to (X = F^{-1} (y) ball (M) r \to Y = y ball (N) r)$
31	30	reximdva	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land y \in Y) \to (\exists r \in ℝ^{+} X = F^{-1} (y) ball (M) r \to \exists r \in ℝ^{+} Y = y ball (N) r)$
32	12 31	syld	$⊢ ((M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \land y \in Y) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to \exists r \in ℝ^{+} Y = y ball (N) r)$
33	32	ralrimdva	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to \forall y \in Y \exists r \in ℝ^{+} Y = y ball (N) r)$
34		simp2	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to N \in ∞Met (Y)$
35	33 34	jctild	$⊢ (M \in ∞Met (X) \land N \in ∞Met (Y) \land F \in (M Ismty N)) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to (N \in ∞Met (Y) \land \forall y \in Y \exists r \in ℝ^{+} Y = y ball (N) r))$
36	35	3expib	$⊢ M \in ∞Met (X) \to ((N \in ∞Met (Y) \land F \in (M Ismty N)) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to (N \in ∞Met (Y) \land \forall y \in Y \exists r \in ℝ^{+} Y = y ball (N) r)))$
37	36	com12	$⊢ (N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in ∞Met (X) \to (\forall x \in X \exists r \in ℝ^{+} X = x ball (M) r \to (N \in ∞Met (Y) \land \forall y \in Y \exists r \in ℝ^{+} Y = y ball (N) r)))$
38	37	impd	$⊢ (N \in ∞Met (Y) \land F \in (M Ismty N)) \to ((M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r) \to (N \in ∞Met (Y) \land \forall y \in Y \exists r \in ℝ^{+} Y = y ball (N) r))$
39		isbndx	$⊢ M \in Bnd (X) \leftrightarrow (M \in ∞Met (X) \land \forall x \in X \exists r \in ℝ^{+} X = x ball (M) r)$
40		isbndx	$⊢ N \in Bnd (Y) \leftrightarrow (N \in ∞Met (Y) \land \forall y \in Y \exists r \in ℝ^{+} Y = y ball (N) r)$
41	38 39 40	3imtr4g	$⊢ (N \in ∞Met (Y) \land F \in (M Ismty N)) \to (M \in Bnd (X) \to N \in Bnd (Y))$

Metamath Proof Explorer

Theorem ismtybndlem

Proof