imasf1oxms - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imasf1oxms		Structured version Visualization version GIF version

Theorem imasf1oxms 24716

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

**Hypotheses**
Ref	Expression
imasf1obl.u	⊢ (𝜑 → 𝑈 = (𝐹 “_s 𝑅))
imasf1obl.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
imasf1obl.f	⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)
imasf1oxms.r	⊢ (𝜑 → 𝑅 ∈ ∞MetSp)

**Assertion**
Ref	Expression
imasf1oxms	⊢ (𝜑 → 𝑈 ∈ ∞MetSp)

Proof of Theorem imasf1oxms Dummy variables 𝑥 𝑟 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasf1obl.u	. . . . 5 ⊢ (𝜑 → 𝑈 = (𝐹 “_s 𝑅))
2		imasf1obl.v	. . . . 5 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		imasf1obl.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)
4		imasf1oxms.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ∞MetSp)
5		eqid 2762	. . . . 5 ⊢ ((dist‘𝑅) ↾ (𝑉 × 𝑉)) = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
6		eqid 2762	. . . . 5 ⊢ (dist‘𝑈) = (dist‘𝑈)
7		eqid 2762	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
8		eqid 2762	. . . . . . . 8 ⊢ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
9	7, 8	xmsxmet 24683	. . . . . . 7 ⊢ (𝑅 ∈ ∞MetSp → ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) ∈ (∞Met‘(Base‘𝑅)))
10	4, 9	syl 18	. . . . . 6 ⊢ (𝜑 → ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) ∈ (∞Met‘(Base‘𝑅)))
11	2	sqxpeqd 5691	. . . . . . 7 ⊢ (𝜑 → (𝑉 × 𝑉) = ((Base‘𝑅) × (Base‘𝑅)))
12	11	reseq2d 5976	. . . . . 6 ⊢ (𝜑 → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))
13	2	fveq2d 6886	. . . . . 6 ⊢ (𝜑 → (∞Met‘𝑉) = (∞Met‘(Base‘𝑅)))
14	10, 12, 13	3eltr4d 2877	. . . . 5 ⊢ (𝜑 → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉))
15	1, 2, 3, 4, 5, 6, 14	imasf1oxmet 24602	. . . 4 ⊢ (𝜑 → (dist‘𝑈) ∈ (∞Met‘𝐵))
16		f1ofo 6829	. . . . . . 7 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵)
17	3, 16	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
18	1, 2, 17, 4	imasbas 17602	. . . . 5 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
19	18	fveq2d 6886	. . . 4 ⊢ (𝜑 → (∞Met‘𝐵) = (∞Met‘(Base‘𝑈)))
20	15, 19	eleqtrd 2864	. . 3 ⊢ (𝜑 → (dist‘𝑈) ∈ (∞Met‘(Base‘𝑈)))
21		ssid 3956	. . 3 ⊢ (Base‘𝑈) ⊆ (Base‘𝑈)
22		xmetres2 24588	. . 3 ⊢ (((dist‘𝑈) ∈ (∞Met‘(Base‘𝑈)) ∧ (Base‘𝑈) ⊆ (Base‘𝑈)) → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) ∈ (∞Met‘(Base‘𝑈)))
23	20, 21, 22	sylancl 598	. 2 ⊢ (𝜑 → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) ∈ (∞Met‘(Base‘𝑈)))
24		eqid 2762	. . . 4 ⊢ (TopOpen‘𝑅) = (TopOpen‘𝑅)
25		eqid 2762	. . . 4 ⊢ (TopOpen‘𝑈) = (TopOpen‘𝑈)
26	1, 2, 17, 4, 24, 25	imastopn 23947	. . 3 ⊢ (𝜑 → (TopOpen‘𝑈) = ((TopOpen‘𝑅) qTop 𝐹))
27	24, 7, 8	xmstopn 24678	. . . . . 6 ⊢ (𝑅 ∈ ∞MetSp → (TopOpen‘𝑅) = (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))
28	4, 27	syl 18	. . . . 5 ⊢ (𝜑 → (TopOpen‘𝑅) = (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))
29	12	fveq2d 6886	. . . . 5 ⊢ (𝜑 → (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))
30	28, 29	eqtr4d 2800	. . . 4 ⊢ (𝜑 → (TopOpen‘𝑅) = (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))))
31	30	oveq1d 7431	. . 3 ⊢ (𝜑 → ((TopOpen‘𝑅) qTop 𝐹) = ((MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹))
32		blbas 24657	. . . . . 6 ⊢ (((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉) → ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ∈ TopBases)
33	14, 32	syl 18	. . . . 5 ⊢ (𝜑 → ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ∈ TopBases)
34		unirnbl 24647	. . . . . . 7 ⊢ (((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉) → ∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = 𝑉)
35		f1oeq2 6810	. . . . . . 7 ⊢ (∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = 𝑉 → (𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–1-1-onto→𝐵 ↔ 𝐹:𝑉–1-1-onto→𝐵))
36	14, 34, 35	3syl 19	. . . . . 6 ⊢ (𝜑 → (𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–1-1-onto→𝐵 ↔ 𝐹:𝑉–1-1-onto→𝐵))
37	3, 36	mpbird 260	. . . . 5 ⊢ (𝜑 → 𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–1-1-onto→𝐵)
38		eqid 2762	. . . . . 6 ⊢ ∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = ∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))
39	38	tgqtop 23939	. . . . 5 ⊢ ((ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ∈ TopBases ∧ 𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–1-1-onto→𝐵) → ((topGen‘ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))) qTop 𝐹) = (topGen‘(ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹)))
40	33, 37, 39	syl2anc 596	. . . 4 ⊢ (𝜑 → ((topGen‘ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))) qTop 𝐹) = (topGen‘(ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹)))
41		eqid 2762	. . . . . . 7 ⊢ (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))
42	41	mopnval 24665	. . . . . 6 ⊢ (((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉) → (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (topGen‘ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))))
43	14, 42	syl 18	. . . . 5 ⊢ (𝜑 → (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (topGen‘ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))))
44	43	oveq1d 7431	. . . 4 ⊢ (𝜑 → ((MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) = ((topGen‘ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))) qTop 𝐹))
45		eqid 2762	. . . . . . 7 ⊢ (MetOpen‘(dist‘𝑈)) = (MetOpen‘(dist‘𝑈))
46	45	mopnval 24665	. . . . . 6 ⊢ ((dist‘𝑈) ∈ (∞Met‘𝐵) → (MetOpen‘(dist‘𝑈)) = (topGen‘ran (ball‘(dist‘𝑈))))
47	15, 46	syl 18	. . . . 5 ⊢ (𝜑 → (MetOpen‘(dist‘𝑈)) = (topGen‘ran (ball‘(dist‘𝑈))))
48		xmetf 24556	. . . . . . . 8 ⊢ ((dist‘𝑈) ∈ (∞Met‘(Base‘𝑈)) → (dist‘𝑈):((Base‘𝑈) × (Base‘𝑈))⟶ℝ^*)
49	20, 48	syl 18	. . . . . . 7 ⊢ (𝜑 → (dist‘𝑈):((Base‘𝑈) × (Base‘𝑈))⟶ℝ^*)
50		ffn 6706	. . . . . . 7 ⊢ ((dist‘𝑈):((Base‘𝑈) × (Base‘𝑈))⟶ℝ^* → (dist‘𝑈) Fn ((Base‘𝑈) × (Base‘𝑈)))
51		fnresdm 6655	. . . . . . 7 ⊢ ((dist‘𝑈) Fn ((Base‘𝑈) × (Base‘𝑈)) → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) = (dist‘𝑈))
52	49, 50, 51	3syl 19	. . . . . 6 ⊢ (𝜑 → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) = (dist‘𝑈))
53	52	fveq2d 6886	. . . . 5 ⊢ (𝜑 → (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))) = (MetOpen‘(dist‘𝑈)))
54	3	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝐹:𝑉–1-1-onto→𝐵)
55		f1of1 6820	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵)
56	54, 55	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝐹:𝑉–1-1→𝐵)
57		cnvimass 6082	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
58		f1odm 6825	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → dom 𝐹 = 𝑉)
59	54, 58	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → dom 𝐹 = 𝑉)
60	57, 59	sseqtrid 3976	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → (^◡𝐹 “ 𝑥) ⊆ 𝑉)
61	14	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉))
62		simprl 783	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝑦 ∈ 𝑉)
63		simprr 785	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^)) → 𝑟 ∈ ℝ^)
64		blssm 24645	. . . . . . . . . . . . . . 15 ⊢ ((((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉) ∧ 𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ⊆ 𝑉)
65	61, 62, 63, 64	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ⊆ 𝑉)
66		f1imaeq 7265	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((^◡𝐹 “ 𝑥) ⊆ 𝑉 ∧ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ⊆ 𝑉)) → ((𝐹 “ (^◡𝐹 “ 𝑥)) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) ↔ (^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)))
67	56, 60, 65, 66	syl12anc 850	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → ((𝐹 “ (^◡𝐹 “ 𝑥)) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) ↔ (^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)))
68	54, 16	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝐹:𝑉–onto→𝐵)
69		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝑥 ⊆ 𝐵)
70		foimacnv 6839	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉–onto→𝐵 ∧ 𝑥 ⊆ 𝐵) → (𝐹 “ (^◡𝐹 “ 𝑥)) = 𝑥)
71	68, 69, 70	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → (𝐹 “ (^◡𝐹 “ 𝑥)) = 𝑥)
72	1	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝑈 = (𝐹 “_s 𝑅))
73	2	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝑉 = (Base‘𝑅))
74	4	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → 𝑅 ∈ ∞MetSp)
75	72, 73, 54, 74, 5, 6, 61, 62, 63	imasf1obl 24715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)))
76	75	eqcomd 2768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))
77	71, 76	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → ((𝐹 “ (^◡𝐹 “ 𝑥)) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) ↔ 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
78	67, 77	bitr3d 284	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ^*)) → ((^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ↔ 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
79	78	2rexbidva 3227	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* (^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
80	3	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝐹:𝑉–1-1-onto→𝐵)
81		f1ofn 6822	. . . . . . . . . . . 12 ⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹 Fn 𝑉)
82		oveq1 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑦) → (𝑧(ball‘(dist‘𝑈))𝑟) = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))
83	82	eqeq2d 2773	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝐹‘𝑦) → (𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
84	83	rexbidv 3188	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝐹‘𝑦) → (∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑟 ∈ ℝ^* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
85	84	rexrn 7083	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝑉 → (∃𝑧 ∈ ran 𝐹∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
86	80, 81, 85	3syl 19	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑧 ∈ ran 𝐹∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)))
87		forn 6796	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
88	80, 16, 87	3syl 19	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ran 𝐹 = 𝐵)
89	88	rexeqdv 3322	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑧 ∈ ran 𝐹∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟)))
90	79, 86, 89	3bitr2d 310	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* (^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟)))
91	14	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉))
92		blrn 24636	. . . . . . . . . . 11 ⊢ (((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉) → ((^◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* (^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)))
93	91, 92	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ((^◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ^* (^◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)))
94	15	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (dist‘𝑈) ∈ (∞Met‘𝐵))
95		blrn 24636	. . . . . . . . . . 11 ⊢ ((dist‘𝑈) ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘(dist‘𝑈)) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟)))
96	94, 95	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝑥 ∈ ran (ball‘(dist‘𝑈)) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ^* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟)))
97	90, 93, 96	3bitr4d 314	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ((^◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ↔ 𝑥 ∈ ran (ball‘(dist‘𝑈))))
98	97	pm5.32da 590	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ (^◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran (ball‘(dist‘𝑈)))))
99		f1ofo 6829	. . . . . . . . . 10 ⊢ (𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–1-1-onto→𝐵 → 𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–onto→𝐵)
100	37, 99	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–onto→𝐵)
101	38	elqtop2 23928	. . . . . . . . 9 ⊢ ((ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ∈ TopBases ∧ 𝐹:∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–onto→𝐵) → (𝑥 ∈ (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) ↔ (𝑥 ⊆ 𝐵 ∧ (^◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))))))
102	33, 100, 101	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) ↔ (𝑥 ⊆ 𝐵 ∧ (^◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))))))
103		blf 24634	. . . . . . . . . . . 12 ⊢ ((dist‘𝑈) ∈ (∞Met‘𝐵) → (ball‘(dist‘𝑈)):(𝐵 × ℝ^*)⟶𝒫 𝐵)
104		frn 6714	. . . . . . . . . . . 12 ⊢ ((ball‘(dist‘𝑈)):(𝐵 × ℝ^*)⟶𝒫 𝐵 → ran (ball‘(dist‘𝑈)) ⊆ 𝒫 𝐵)
105	15, 103, 104	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → ran (ball‘(dist‘𝑈)) ⊆ 𝒫 𝐵)
106	105	sseld 3933	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘(dist‘𝑈)) → 𝑥 ∈ 𝒫 𝐵))
107		elpwi 4567	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵)
108	106, 107	syl6 36	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘(dist‘𝑈)) → 𝑥 ⊆ 𝐵))
109	108	pm4.71rd 572	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ran (ball‘(dist‘𝑈)) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran (ball‘(dist‘𝑈)))))
110	98, 102, 109	3bitr4d 314	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) ↔ 𝑥 ∈ ran (ball‘(dist‘𝑈))))
111	110	eqrdv 2760	. . . . . 6 ⊢ (𝜑 → (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) = ran (ball‘(dist‘𝑈)))
112	111	fveq2d 6886	. . . . 5 ⊢ (𝜑 → (topGen‘(ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹)) = (topGen‘ran (ball‘(dist‘𝑈))))
113	47, 53, 112	3eqtr4d 2807	. . . 4 ⊢ (𝜑 → (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))) = (topGen‘(ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹)))
114	40, 44, 113	3eqtr4d 2807	. . 3 ⊢ (𝜑 → ((MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) = (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))))
115	26, 31, 114	3eqtrd 2801	. 2 ⊢ (𝜑 → (TopOpen‘𝑈) = (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))))
116		eqid 2762	. . 3 ⊢ (Base‘𝑈) = (Base‘𝑈)
117		eqid 2762	. . 3 ⊢ ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) = ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))
118	25, 116, 117	isxms2 24675	. 2 ⊢ (𝑈 ∈ ∞MetSp ↔ (((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) ∈ (∞Met‘(Base‘𝑈)) ∧ (TopOpen‘𝑈) = (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))))))
119	23, 115, 118	sylanbrc 595	1 ⊢ (𝜑 → 𝑈 ∈ ∞MetSp)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∃wrex 3088 ⊆ wss 3902 𝒫 cpw 4560 ∪ cuni 4870 × cxp 5657 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7416 ℝ^*cxr 11269 Basecbs 17305 distcds 17355 TopOpenctopn 17510 topGenctg 17526 qTop cqtop 17593 “_s cimas 17594 ∞Metcxmet 21571 ballcbl 21573 MetOpencmopn 21576 TopBasesctb 23171 ∞MetSpcxms 24544

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13045 df-xneg 13165 df-xadd 13166 df-xmul 13167 df-fz 13564 df-fzo 13712 df-seq 14068 df-hash 14397 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-rest 17511 df-topn 17512 df-0g 17530 df-gsum 17531 df-topgen 17532 df-xrs 17592 df-qtop 17597 df-imas 17598 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18823 df-mnd 18839 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-bl 21581 df-mopn 21582 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-xms 24547

This theorem is used by: imasf1oms 24717 xpsxms 24761

W3C validator