imasf1oxms

Description: The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	imasf1obl.u	$⊢ φ \to U = F “_{𝑠} R$
	imasf1obl.v	$⊢ φ \to V = {Base}_{R}$
	imasf1obl.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} B$
	imasf1oxms.r	$⊢ φ \to R \in ∞MetSp$
Assertion	imasf1oxms	$⊢ φ \to U \in ∞MetSp$

Proof

Step	Hyp	Ref	Expression
1		imasf1obl.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasf1obl.v	$⊢ φ \to V = {Base}_{R}$
3		imasf1obl.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} B$
4		imasf1oxms.r	$⊢ φ \to R \in ∞MetSp$
5		eqid	$⊢ {dist (R) ↾}_{(V \times V)} = {dist (R) ↾}_{(V \times V)}$
6		eqid	$⊢ dist (U) = dist (U)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8		eqid	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
9	7 8	xmsxmet	$⊢ R \in ∞MetSp \to {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R})$
10	4 9	syl	$⊢ φ \to {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R})$
11	2	sqxpeqd	$⊢ φ \to V \times V = {Base}_{R} \times {Base}_{R}$
12	11	reseq2d	$⊢ φ \to {dist (R) ↾}_{(V \times V)} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
13	2	fveq2d	$⊢ φ \to ∞Met (V) = ∞Met ({Base}_{R})$
14	10 12 13	3eltr4d	$⊢ φ \to {dist (R) ↾}_{(V \times V)} \in ∞Met (V)$
15	1 2 3 4 5 6 14	imasf1oxmet	$⊢ φ \to dist (U) \in ∞Met (B)$
16		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{onto}{⟶} B$
17	3 16	syl	$⊢ φ \to F : V \underset{onto}{⟶} B$
18	1 2 17 4	imasbas	$⊢ φ \to B = {Base}_{U}$
19	18	fveq2d	$⊢ φ \to ∞Met (B) = ∞Met ({Base}_{U})$
20	15 19	eleqtrd	$⊢ φ \to dist (U) \in ∞Met ({Base}_{U})$
21		ssid	$⊢ {Base}_{U} \subseteq {Base}_{U}$
22		xmetres2	$⊢ (dist (U) \in ∞Met ({Base}_{U}) \land {Base}_{U} \subseteq {Base}_{U}) \to {dist (U) ↾}_{({Base}_{U} \times {Base}_{U})} \in ∞Met ({Base}_{U})$
23	20 21 22	sylancl	$⊢ φ \to {dist (U) ↾}_{({Base}_{U} \times {Base}_{U})} \in ∞Met ({Base}_{U})$
24		eqid	$⊢ TopOpen (R) = TopOpen (R)$
25		eqid	$⊢ TopOpen (U) = TopOpen (U)$
26	1 2 17 4 24 25	imastopn	$⊢ φ \to TopOpen (U) = TopOpen (R) qTop F$
27	24 7 8	xmstopn	$⊢ R \in ∞MetSp \to TopOpen (R) = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
28	4 27	syl	$⊢ φ \to TopOpen (R) = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
29	12	fveq2d	$⊢ φ \to MetOpen ({dist (R) ↾}_{(V \times V)}) = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
30	28 29	eqtr4d	$⊢ φ \to TopOpen (R) = MetOpen ({dist (R) ↾}_{(V \times V)})$
31	30	oveq1d	$⊢ φ \to TopOpen (R) qTop F = MetOpen ({dist (R) ↾}_{(V \times V)}) qTop F$
32		blbas	$⊢ {dist (R) ↾}_{(V \times V)} \in ∞Met (V) \to ran ball ({dist (R) ↾}_{(V \times V)}) \in TopBases$
33	14 32	syl	$⊢ φ \to ran ball ({dist (R) ↾}_{(V \times V)}) \in TopBases$
34		unirnbl	$⊢ {dist (R) ↾}_{(V \times V)} \in ∞Met (V) \to ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) = V$
35		f1oeq2	$⊢ ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) = V \to (F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{1-1 onto}{⟶} B \leftrightarrow F : V \underset{1-1 onto}{⟶} B)$
36	14 34 35	3syl	$⊢ φ \to (F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{1-1 onto}{⟶} B \leftrightarrow F : V \underset{1-1 onto}{⟶} B)$
37	3 36	mpbird	$⊢ φ \to F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{1-1 onto}{⟶} B$
38		eqid	$⊢ ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) = ⋃ ran ball ({dist (R) ↾}_{(V \times V)})$
39	38	tgqtop	$⊢ (ran ball ({dist (R) ↾}_{(V \times V)}) \in TopBases \land F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{1-1 onto}{⟶} B) \to topGen (ran ball ({dist (R) ↾}_{(V \times V)})) qTop F = topGen (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F)$
40	33 37 39	syl2anc	$⊢ φ \to topGen (ran ball ({dist (R) ↾}_{(V \times V)})) qTop F = topGen (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F)$
41		eqid	$⊢ MetOpen ({dist (R) ↾}_{(V \times V)}) = MetOpen ({dist (R) ↾}_{(V \times V)})$
42	41	mopnval	$⊢ {dist (R) ↾}_{(V \times V)} \in ∞Met (V) \to MetOpen ({dist (R) ↾}_{(V \times V)}) = topGen (ran ball ({dist (R) ↾}_{(V \times V)}))$
43	14 42	syl	$⊢ φ \to MetOpen ({dist (R) ↾}_{(V \times V)}) = topGen (ran ball ({dist (R) ↾}_{(V \times V)}))$
44	43	oveq1d	$⊢ φ \to MetOpen ({dist (R) ↾}_{(V \times V)}) qTop F = topGen (ran ball ({dist (R) ↾}_{(V \times V)})) qTop F$
45		eqid	$⊢ MetOpen (dist (U)) = MetOpen (dist (U))$
46	45	mopnval	$⊢ dist (U) \in ∞Met (B) \to MetOpen (dist (U)) = topGen (ran ball (dist (U)))$
47	15 46	syl	$⊢ φ \to MetOpen (dist (U)) = topGen (ran ball (dist (U)))$
48		xmetf	$⊢ dist (U) \in ∞Met ({Base}_{U}) \to dist (U) : {Base}_{U} \times {Base}_{U} ⟶ ℝ^{*}$
49	20 48	syl	$⊢ φ \to dist (U) : {Base}_{U} \times {Base}_{U} ⟶ ℝ^{*}$
50		ffn	$⊢ dist (U) : {Base}_{U} \times {Base}_{U} ⟶ ℝ^{*} \to dist (U) Fn ({Base}_{U} \times {Base}_{U})$
51		fnresdm	$⊢ dist (U) Fn ({Base}_{U} \times {Base}_{U}) \to {dist (U) ↾}_{({Base}_{U} \times {Base}_{U})} = dist (U)$
52	49 50 51	3syl	$⊢ φ \to {dist (U) ↾}_{({Base}_{U} \times {Base}_{U})} = dist (U)$
53	52	fveq2d	$⊢ φ \to MetOpen ({dist (U) ↾}_{({Base}_{U} \times {Base}_{U})}) = MetOpen (dist (U))$
54	3	ad2antrr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F : V \underset{1-1 onto}{⟶} B$
55		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{1-1}{⟶} B$
56	54 55	syl	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F : V \underset{1-1}{⟶} B$
57		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
58		f1odm	$⊢ F : V \underset{1-1 onto}{⟶} B \to dom F = V$
59	54 58	syl	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to dom F = V$
60	57 59	sseqtrid	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F^{-1} [x] \subseteq V$
61	14	ad2antrr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to {dist (R) ↾}_{(V \times V)} \in ∞Met (V)$
62		simprl	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to y \in V$
63		simprr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{})) \to r \in ℝ^{}$
64		blssm	$⊢ ({dist (R) ↾}_{(V \times V)} \in ∞Met (V) \land y \in V \land r \in ℝ^{*}) \to y ball ({dist (R) ↾}_{(V \times V)}) r \subseteq V$
65	61 62 63 64	syl3anc	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to y ball ({dist (R) ↾}_{(V \times V)}) r \subseteq V$
66		f1imaeq	$⊢ (F : V \underset{1-1}{⟶} B \land (F^{-1} [x] \subseteq V \land y ball ({dist (R) ↾}_{(V \times V)}) r \subseteq V)) \to (F [F^{-1} [x]] = F [y ball ({dist (R) ↾}_{(V \times V)}) r] \leftrightarrow F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r)$
67	56 60 65 66	syl12anc	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to (F [F^{-1} [x]] = F [y ball ({dist (R) ↾}_{(V \times V)}) r] \leftrightarrow F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r)$
68	54 16	syl	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F : V \underset{onto}{⟶} B$
69		simplr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to x \subseteq B$
70		foimacnv	$⊢ (F : V \underset{onto}{⟶} B \land x \subseteq B) \to F [F^{-1} [x]] = x$
71	68 69 70	syl2anc	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F [F^{-1} [x]] = x$
72	1	ad2antrr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to U = F “_{𝑠} R$
73	2	ad2antrr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to V = {Base}_{R}$
74	4	ad2antrr	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to R \in ∞MetSp$
75	72 73 54 74 5 6 61 62 63	imasf1obl	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F (y) ball (dist (U)) r = F [y ball ({dist (R) ↾}_{(V \times V)}) r]$
76	75	eqcomd	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to F [y ball ({dist (R) ↾}_{(V \times V)}) r] = F (y) ball (dist (U)) r$
77	71 76	eqeq12d	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to (F [F^{-1} [x]] = F [y ball ({dist (R) ↾}_{(V \times V)}) r] \leftrightarrow x = F (y) ball (dist (U)) r)$
78	67 77	bitr3d	$⊢ ((φ \land x \subseteq B) \land (y \in V \land r \in ℝ^{*})) \to (F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r \leftrightarrow x = F (y) ball (dist (U)) r)$
79	78	2rexbidva	$⊢ (φ \land x \subseteq B) \to (\exists y \in V \exists r \in ℝ^{} F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r \leftrightarrow \exists y \in V \exists r \in ℝ^{} x = F (y) ball (dist (U)) r)$
80	3	adantr	$⊢ (φ \land x \subseteq B) \to F : V \underset{1-1 onto}{⟶} B$
81		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} B \to F Fn V$
82		oveq1	$⊢ z = F (y) \to z ball (dist (U)) r = F (y) ball (dist (U)) r$
83	82	eqeq2d	$⊢ z = F (y) \to (x = z ball (dist (U)) r \leftrightarrow x = F (y) ball (dist (U)) r)$
84	83	rexbidv	$⊢ z = F (y) \to (\exists r \in ℝ^{} x = z ball (dist (U)) r \leftrightarrow \exists r \in ℝ^{} x = F (y) ball (dist (U)) r)$
85	84	rexrn	$⊢ F Fn V \to (\exists z \in ran F \exists r \in ℝ^{} x = z ball (dist (U)) r \leftrightarrow \exists y \in V \exists r \in ℝ^{} x = F (y) ball (dist (U)) r)$
86	80 81 85	3syl	$⊢ (φ \land x \subseteq B) \to (\exists z \in ran F \exists r \in ℝ^{} x = z ball (dist (U)) r \leftrightarrow \exists y \in V \exists r \in ℝ^{} x = F (y) ball (dist (U)) r)$
87		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
88	80 16 87	3syl	$⊢ (φ \land x \subseteq B) \to ran F = B$
89	88	rexeqdv	$⊢ (φ \land x \subseteq B) \to (\exists z \in ran F \exists r \in ℝ^{} x = z ball (dist (U)) r \leftrightarrow \exists z \in B \exists r \in ℝ^{} x = z ball (dist (U)) r)$
90	79 86 89	3bitr2d	$⊢ (φ \land x \subseteq B) \to (\exists y \in V \exists r \in ℝ^{} F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r \leftrightarrow \exists z \in B \exists r \in ℝ^{} x = z ball (dist (U)) r)$
91	14	adantr	$⊢ (φ \land x \subseteq B) \to {dist (R) ↾}_{(V \times V)} \in ∞Met (V)$
92		blrn	$⊢ {dist (R) ↾}_{(V \times V)} \in ∞Met (V) \to (F^{-1} [x] \in ran ball ({dist (R) ↾}_{(V \times V)}) \leftrightarrow \exists y \in V \exists r \in ℝ^{*} F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r)$
93	91 92	syl	$⊢ (φ \land x \subseteq B) \to (F^{-1} [x] \in ran ball ({dist (R) ↾}_{(V \times V)}) \leftrightarrow \exists y \in V \exists r \in ℝ^{*} F^{-1} [x] = y ball ({dist (R) ↾}_{(V \times V)}) r)$
94	15	adantr	$⊢ (φ \land x \subseteq B) \to dist (U) \in ∞Met (B)$
95		blrn	$⊢ dist (U) \in ∞Met (B) \to (x \in ran ball (dist (U)) \leftrightarrow \exists z \in B \exists r \in ℝ^{*} x = z ball (dist (U)) r)$
96	94 95	syl	$⊢ (φ \land x \subseteq B) \to (x \in ran ball (dist (U)) \leftrightarrow \exists z \in B \exists r \in ℝ^{*} x = z ball (dist (U)) r)$
97	90 93 96	3bitr4d	$⊢ (φ \land x \subseteq B) \to (F^{-1} [x] \in ran ball ({dist (R) ↾}_{(V \times V)}) \leftrightarrow x \in ran ball (dist (U)))$
98	97	pm5.32da	$⊢ φ \to ((x \subseteq B \land F^{-1} [x] \in ran ball ({dist (R) ↾}_{(V \times V)})) \leftrightarrow (x \subseteq B \land x \in ran ball (dist (U))))$
99		f1ofo	$⊢ F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{1-1 onto}{⟶} B \to F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{onto}{⟶} B$
100	37 99	syl	$⊢ φ \to F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{onto}{⟶} B$
101	38	elqtop2	$⊢ (ran ball ({dist (R) ↾}_{(V \times V)}) \in TopBases \land F : ⋃ ran ball ({dist (R) ↾}_{(V \times V)}) \underset{onto}{⟶} B) \to (x \in (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F) \leftrightarrow (x \subseteq B \land F^{-1} [x] \in ran ball ({dist (R) ↾}_{(V \times V)})))$
102	33 100 101	syl2anc	$⊢ φ \to (x \in (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F) \leftrightarrow (x \subseteq B \land F^{-1} [x] \in ran ball ({dist (R) ↾}_{(V \times V)})))$
103		blf	$⊢ dist (U) \in ∞Met (B) \to ball (dist (U)) : B \times ℝ^{*} ⟶ 𝒫 B$
104		frn	$⊢ ball (dist (U)) : B \times ℝ^{*} ⟶ 𝒫 B \to ran ball (dist (U)) \subseteq 𝒫 B$
105	15 103 104	3syl	$⊢ φ \to ran ball (dist (U)) \subseteq 𝒫 B$
106	105	sseld	$⊢ φ \to (x \in ran ball (dist (U)) \to x \in 𝒫 B)$
107		elpwi	$⊢ x \in 𝒫 B \to x \subseteq B$
108	106 107	syl6	$⊢ φ \to (x \in ran ball (dist (U)) \to x \subseteq B)$
109	108	pm4.71rd	$⊢ φ \to (x \in ran ball (dist (U)) \leftrightarrow (x \subseteq B \land x \in ran ball (dist (U))))$
110	98 102 109	3bitr4d	$⊢ φ \to (x \in (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F) \leftrightarrow x \in ran ball (dist (U)))$
111	110	eqrdv	$⊢ φ \to ran ball ({dist (R) ↾}_{(V \times V)}) qTop F = ran ball (dist (U))$
112	111	fveq2d	$⊢ φ \to topGen (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F) = topGen (ran ball (dist (U)))$
113	47 53 112	3eqtr4d	$⊢ φ \to MetOpen ({dist (U) ↾}_{({Base}_{U} \times {Base}_{U})}) = topGen (ran ball ({dist (R) ↾}_{(V \times V)}) qTop F)$
114	40 44 113	3eqtr4d	$⊢ φ \to MetOpen ({dist (R) ↾}_{(V \times V)}) qTop F = MetOpen ({dist (U) ↾}_{({Base}_{U} \times {Base}_{U})})$
115	26 31 114	3eqtrd	$⊢ φ \to TopOpen (U) = MetOpen ({dist (U) ↾}_{({Base}_{U} \times {Base}_{U})})$
116		eqid	$⊢ {Base}_{U} = {Base}_{U}$
117		eqid	$⊢ {dist (U) ↾}_{({Base}_{U} \times {Base}_{U})} = {dist (U) ↾}_{({Base}_{U} \times {Base}_{U})}$
118	25 116 117	isxms2	$⊢ U \in ∞MetSp \leftrightarrow ({dist (U) ↾}_{({Base}_{U} \times {Base}_{U})} \in ∞Met ({Base}_{U}) \land TopOpen (U) = MetOpen ({dist (U) ↾}_{({Base}_{U} \times {Base}_{U})}))$
119	23 115 118	sylanbrc	$⊢ φ \to U \in ∞MetSp$

Metamath Proof Explorer

Theorem imasf1oxms

Proof