| 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 2737 | . . . . 5
⊢
((dist‘𝑅)
↾ (𝑉 × 𝑉)) = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) | 
| 6 |  | eqid 2737 | . . . . 5
⊢
(dist‘𝑈) =
(dist‘𝑈) | 
| 7 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 8 |  | eqid 2737 | . . . . . . . 8
⊢
((dist‘𝑅)
↾ ((Base‘𝑅)
× (Base‘𝑅))) =
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) | 
| 9 | 7, 8 | xmsxmet 24466 | . . . . . . 7
⊢ (𝑅 ∈ ∞MetSp →
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅))) | 
| 10 | 4, 9 | syl 17 | . . . . . 6
⊢ (𝜑 → ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅))) | 
| 11 | 2 | sqxpeqd 5717 | . . . . . . 7
⊢ (𝜑 → (𝑉 × 𝑉) = ((Base‘𝑅) × (Base‘𝑅))) | 
| 12 | 11 | reseq2d 5997 | . . . . . 6
⊢ (𝜑 → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))) | 
| 13 | 2 | fveq2d 6910 | . . . . . 6
⊢ (𝜑 → (∞Met‘𝑉) =
(∞Met‘(Base‘𝑅))) | 
| 14 | 10, 12, 13 | 3eltr4d 2856 | . . . . 5
⊢ (𝜑 → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉)) | 
| 15 | 1, 2, 3, 4, 5, 6, 14 | imasf1oxmet 24385 | . . . 4
⊢ (𝜑 → (dist‘𝑈) ∈ (∞Met‘𝐵)) | 
| 16 |  | f1ofo 6855 | . . . . . . 7
⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–onto→𝐵) | 
| 17 | 3, 16 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) | 
| 18 | 1, 2, 17, 4 | imasbas 17557 | . . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝑈)) | 
| 19 | 18 | fveq2d 6910 | . . . 4
⊢ (𝜑 → (∞Met‘𝐵) =
(∞Met‘(Base‘𝑈))) | 
| 20 | 15, 19 | eleqtrd 2843 | . . 3
⊢ (𝜑 → (dist‘𝑈) ∈
(∞Met‘(Base‘𝑈))) | 
| 21 |  | ssid 4006 | . . 3
⊢
(Base‘𝑈)
⊆ (Base‘𝑈) | 
| 22 |  | xmetres2 24371 | . . 3
⊢
(((dist‘𝑈)
∈ (∞Met‘(Base‘𝑈)) ∧ (Base‘𝑈) ⊆ (Base‘𝑈)) → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) ∈
(∞Met‘(Base‘𝑈))) | 
| 23 | 20, 21, 22 | sylancl 586 | . 2
⊢ (𝜑 → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) ∈
(∞Met‘(Base‘𝑈))) | 
| 24 |  | eqid 2737 | . . . 4
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) | 
| 25 |  | eqid 2737 | . . . 4
⊢
(TopOpen‘𝑈) =
(TopOpen‘𝑈) | 
| 26 | 1, 2, 17, 4, 24, 25 | imastopn 23728 | . . 3
⊢ (𝜑 → (TopOpen‘𝑈) = ((TopOpen‘𝑅) qTop 𝐹)) | 
| 27 | 24, 7, 8 | xmstopn 24461 | . . . . . 6
⊢ (𝑅 ∈ ∞MetSp →
(TopOpen‘𝑅) =
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) | 
| 28 | 4, 27 | syl 17 | . . . . 5
⊢ (𝜑 → (TopOpen‘𝑅) =
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) | 
| 29 | 12 | fveq2d 6910 | . . . . 5
⊢ (𝜑 →
(MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) | 
| 30 | 28, 29 | eqtr4d 2780 | . . . 4
⊢ (𝜑 → (TopOpen‘𝑅) =
(MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))) | 
| 31 | 30 | oveq1d 7446 | . . 3
⊢ (𝜑 → ((TopOpen‘𝑅) qTop 𝐹) = ((MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹)) | 
| 32 |  | blbas 24440 | . . . . . 6
⊢
(((dist‘𝑅)
↾ (𝑉 × 𝑉)) ∈
(∞Met‘𝑉) →
ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ∈ TopBases) | 
| 33 | 14, 32 | syl 17 | . . . . 5
⊢ (𝜑 → ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) ∈
TopBases) | 
| 34 |  | unirnbl 24430 | . . . . . . 7
⊢
(((dist‘𝑅)
↾ (𝑉 × 𝑉)) ∈
(∞Met‘𝑉) →
∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = 𝑉) | 
| 35 |  | f1oeq2 6837 | . . . . . . 7
⊢ (∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = 𝑉 → (𝐹:∪ ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))–1-1-onto→𝐵 ↔ 𝐹:𝑉–1-1-onto→𝐵)) | 
| 36 | 14, 34, 35 | 3syl 18 | . . . . . 6
⊢ (𝜑 → (𝐹:∪ ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))–1-1-onto→𝐵 ↔ 𝐹:𝑉–1-1-onto→𝐵)) | 
| 37 | 3, 36 | mpbird 257 | . . . . 5
⊢ (𝜑 → 𝐹:∪ ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))–1-1-onto→𝐵) | 
| 38 |  | eqid 2737 | . . . . . 6
⊢ ∪ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = ∪ ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) | 
| 39 | 38 | tgqtop 23720 | . . . . 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 584 | . . . 4
⊢ (𝜑 → ((topGen‘ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))) qTop 𝐹) = (topGen‘(ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) qTop 𝐹))) | 
| 41 |  | eqid 2737 | . . . . . . 7
⊢
(MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) | 
| 42 | 41 | mopnval 24448 | . . . . . 6
⊢
(((dist‘𝑅)
↾ (𝑉 × 𝑉)) ∈
(∞Met‘𝑉) →
(MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (topGen‘ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))))) | 
| 43 | 14, 42 | syl 17 | . . . . 5
⊢ (𝜑 →
(MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) = (topGen‘ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))))) | 
| 44 | 43 | oveq1d 7446 | . . . 4
⊢ (𝜑 →
((MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) = ((topGen‘ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))) qTop 𝐹)) | 
| 45 |  | eqid 2737 | . . . . . . 7
⊢
(MetOpen‘(dist‘𝑈)) = (MetOpen‘(dist‘𝑈)) | 
| 46 | 45 | mopnval 24448 | . . . . . 6
⊢
((dist‘𝑈)
∈ (∞Met‘𝐵)
→ (MetOpen‘(dist‘𝑈)) = (topGen‘ran
(ball‘(dist‘𝑈)))) | 
| 47 | 15, 46 | syl 17 | . . . . 5
⊢ (𝜑 →
(MetOpen‘(dist‘𝑈)) = (topGen‘ran
(ball‘(dist‘𝑈)))) | 
| 48 |  | xmetf 24339 | . . . . . . . 8
⊢
((dist‘𝑈)
∈ (∞Met‘(Base‘𝑈)) → (dist‘𝑈):((Base‘𝑈) × (Base‘𝑈))⟶ℝ*) | 
| 49 | 20, 48 | syl 17 | . . . . . . 7
⊢ (𝜑 → (dist‘𝑈):((Base‘𝑈) × (Base‘𝑈))⟶ℝ*) | 
| 50 |  | ffn 6736 | . . . . . . 7
⊢
((dist‘𝑈):((Base‘𝑈) × (Base‘𝑈))⟶ℝ* →
(dist‘𝑈) Fn
((Base‘𝑈) ×
(Base‘𝑈))) | 
| 51 |  | fnresdm 6687 | . . . . . . 7
⊢
((dist‘𝑈) Fn
((Base‘𝑈) ×
(Base‘𝑈)) →
((dist‘𝑈) ↾
((Base‘𝑈) ×
(Base‘𝑈))) =
(dist‘𝑈)) | 
| 52 | 49, 50, 51 | 3syl 18 | . . . . . 6
⊢ (𝜑 → ((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))) = (dist‘𝑈)) | 
| 53 | 52 | fveq2d 6910 | . . . . 5
⊢ (𝜑 →
(MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))) = (MetOpen‘(dist‘𝑈))) | 
| 54 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝐹:𝑉–1-1-onto→𝐵) | 
| 55 |  | f1of1 6847 | . . . . . . . . . . . . . . 15
⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹:𝑉–1-1→𝐵) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝐹:𝑉–1-1→𝐵) | 
| 57 |  | cnvimass 6100 | . . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 | 
| 58 |  | f1odm 6852 | . . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑉–1-1-onto→𝐵 → dom 𝐹 = 𝑉) | 
| 59 | 54, 58 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → dom
𝐹 = 𝑉) | 
| 60 | 57, 59 | sseqtrid 4026 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → (◡𝐹 “ 𝑥) ⊆ 𝑉) | 
| 61 | 14 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) →
((dist‘𝑅) ↾
(𝑉 × 𝑉)) ∈
(∞Met‘𝑉)) | 
| 62 |  | simprl 771 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝑦 ∈ 𝑉) | 
| 63 |  | simprr 773 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝑟 ∈
ℝ*) | 
| 64 |  | blssm 24428 | . . . . . . . . . . . . . . 15
⊢
((((dist‘𝑅)
↾ (𝑉 × 𝑉)) ∈
(∞Met‘𝑉) ∧
𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ⊆ 𝑉) | 
| 65 | 61, 62, 63, 64 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ⊆ 𝑉) | 
| 66 |  | f1imaeq 7285 | . . . . . . . . . . . . . 14
⊢ ((𝐹:𝑉–1-1→𝐵 ∧ ((◡𝐹 “ 𝑥) ⊆ 𝑉 ∧ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ⊆ 𝑉)) → ((𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) ↔ (◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟))) | 
| 67 | 56, 60, 65, 66 | syl12anc 837 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → ((𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) ↔ (◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟))) | 
| 68 | 54, 16 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝐹:𝑉–onto→𝐵) | 
| 69 |  | simplr 769 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝑥 ⊆ 𝐵) | 
| 70 |  | foimacnv 6865 | . . . . . . . . . . . . . . 15
⊢ ((𝐹:𝑉–onto→𝐵 ∧ 𝑥 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) | 
| 71 | 68, 69, 70 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) | 
| 72 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝑈 = (𝐹 “s 𝑅)) | 
| 73 | 2 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝑉 = (Base‘𝑅)) | 
| 74 | 4 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → 𝑅 ∈
∞MetSp) | 
| 75 | 72, 73, 54, 74, 5, 6, 61, 62, 63 | imasf1obl 24501 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟))) | 
| 76 | 75 | eqcomd 2743 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)) | 
| 77 | 71, 76 | eqeq12d 2753 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → ((𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟)) ↔ 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 78 | 67, 77 | bitr3d 281 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐵) ∧ (𝑦 ∈ 𝑉 ∧ 𝑟 ∈ ℝ*)) → ((◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ↔ 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 79 | 78 | 2rexbidva 3220 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* (◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 80 | 3 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝐹:𝑉–1-1-onto→𝐵) | 
| 81 |  | f1ofn 6849 | . . . . . . . . . . . 12
⊢ (𝐹:𝑉–1-1-onto→𝐵 → 𝐹 Fn 𝑉) | 
| 82 |  | oveq1 7438 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑦) → (𝑧(ball‘(dist‘𝑈))𝑟) = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟)) | 
| 83 | 82 | eqeq2d 2748 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (𝐹‘𝑦) → (𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 84 | 83 | rexbidv 3179 | . . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹‘𝑦) → (∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑟 ∈ ℝ* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 85 | 84 | rexrn 7107 | . . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑉 → (∃𝑧 ∈ ran 𝐹∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 86 | 80, 81, 85 | 3syl 18 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑧 ∈ ran 𝐹∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* 𝑥 = ((𝐹‘𝑦)(ball‘(dist‘𝑈))𝑟))) | 
| 87 |  | forn 6823 | . . . . . . . . . . . . 13
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) | 
| 88 | 80, 16, 87 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ran 𝐹 = 𝐵) | 
| 89 | 88 | rexeqdv 3327 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑧 ∈ ran 𝐹∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟))) | 
| 90 | 79, 86, 89 | 3bitr2d 307 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* (◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟))) | 
| 91 | 14 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) ∈ (∞Met‘𝑉)) | 
| 92 |  | blrn 24419 | . . . . . . . . . . 11
⊢
(((dist‘𝑅)
↾ (𝑉 × 𝑉)) ∈
(∞Met‘𝑉) →
((◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* (◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟))) | 
| 93 | 91, 92 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ((◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ↔ ∃𝑦 ∈ 𝑉 ∃𝑟 ∈ ℝ* (◡𝐹 “ 𝑥) = (𝑦(ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))𝑟))) | 
| 94 | 15 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (dist‘𝑈) ∈ (∞Met‘𝐵)) | 
| 95 |  | blrn 24419 | . . . . . . . . . . 11
⊢
((dist‘𝑈)
∈ (∞Met‘𝐵)
→ (𝑥 ∈ ran
(ball‘(dist‘𝑈))
↔ ∃𝑧 ∈
𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟))) | 
| 96 | 94, 95 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝑥 ∈ ran (ball‘(dist‘𝑈)) ↔ ∃𝑧 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑧(ball‘(dist‘𝑈))𝑟))) | 
| 97 | 90, 93, 96 | 3bitr4d 311 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → ((◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) ↔ 𝑥 ∈ ran (ball‘(dist‘𝑈)))) | 
| 98 | 97 | pm5.32da 579 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ⊆ 𝐵 ∧ (◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran (ball‘(dist‘𝑈))))) | 
| 99 |  | f1ofo 6855 | . . . . . . . . . 10
⊢ (𝐹:∪
ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–1-1-onto→𝐵 → 𝐹:∪ ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))–onto→𝐵) | 
| 100 | 37, 99 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:∪ ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉)))–onto→𝐵) | 
| 101 | 38 | elqtop2 23709 | . . . . . . . . 9
⊢ ((ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) ∈ TopBases ∧ 𝐹:∪
ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))–onto→𝐵) → (𝑥 ∈ (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) ↔ (𝑥 ⊆ 𝐵 ∧ (◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))))) | 
| 102 | 33, 100, 101 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) ↔ (𝑥 ⊆ 𝐵 ∧ (◡𝐹 “ 𝑥) ∈ ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉)))))) | 
| 103 |  | blf 24417 | . . . . . . . . . . . 12
⊢
((dist‘𝑈)
∈ (∞Met‘𝐵)
→ (ball‘(dist‘𝑈)):(𝐵 ×
ℝ*)⟶𝒫 𝐵) | 
| 104 |  | frn 6743 | . . . . . . . . . . . 12
⊢
((ball‘(dist‘𝑈)):(𝐵 ×
ℝ*)⟶𝒫 𝐵 → ran (ball‘(dist‘𝑈)) ⊆ 𝒫 𝐵) | 
| 105 | 15, 103, 104 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → ran
(ball‘(dist‘𝑈))
⊆ 𝒫 𝐵) | 
| 106 | 105 | sseld 3982 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ran (ball‘(dist‘𝑈)) → 𝑥 ∈ 𝒫 𝐵)) | 
| 107 |  | elpwi 4607 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵) | 
| 108 | 106, 107 | syl6 35 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ran (ball‘(dist‘𝑈)) → 𝑥 ⊆ 𝐵)) | 
| 109 | 108 | pm4.71rd 562 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ran (ball‘(dist‘𝑈)) ↔ (𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ ran (ball‘(dist‘𝑈))))) | 
| 110 | 98, 102, 109 | 3bitr4d 311 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (ran (ball‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) ↔ 𝑥 ∈ ran (ball‘(dist‘𝑈)))) | 
| 111 | 110 | eqrdv 2735 | . . . . . 6
⊢ (𝜑 → (ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) qTop 𝐹) = ran (ball‘(dist‘𝑈))) | 
| 112 | 111 | fveq2d 6910 | . . . . 5
⊢ (𝜑 → (topGen‘(ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) qTop 𝐹)) = (topGen‘ran
(ball‘(dist‘𝑈)))) | 
| 113 | 47, 53, 112 | 3eqtr4d 2787 | . . . 4
⊢ (𝜑 →
(MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))) = (topGen‘(ran
(ball‘((dist‘𝑅)
↾ (𝑉 × 𝑉))) qTop 𝐹))) | 
| 114 | 40, 44, 113 | 3eqtr4d 2787 | . . 3
⊢ (𝜑 →
((MetOpen‘((dist‘𝑅) ↾ (𝑉 × 𝑉))) qTop 𝐹) = (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))))) | 
| 115 | 26, 31, 114 | 3eqtrd 2781 | . 2
⊢ (𝜑 → (TopOpen‘𝑈) =
(MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈))))) | 
| 116 |  | eqid 2737 | . . 3
⊢
(Base‘𝑈) =
(Base‘𝑈) | 
| 117 |  | eqid 2737 | . . 3
⊢
((dist‘𝑈)
↾ ((Base‘𝑈)
× (Base‘𝑈))) =
((dist‘𝑈) ↾
((Base‘𝑈) ×
(Base‘𝑈))) | 
| 118 | 25, 116, 117 | isxms2 24458 | . 2
⊢ (𝑈 ∈ ∞MetSp ↔
(((dist‘𝑈) ↾
((Base‘𝑈) ×
(Base‘𝑈))) ∈
(∞Met‘(Base‘𝑈)) ∧ (TopOpen‘𝑈) = (MetOpen‘((dist‘𝑈) ↾ ((Base‘𝑈) × (Base‘𝑈)))))) | 
| 119 | 23, 115, 118 | sylanbrc 583 | 1
⊢ (𝜑 → 𝑈 ∈ ∞MetSp) |