Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢ (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
2 | | eqid 2738 |
. . . 4
⊢
(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
3 | | prdsbnd.v |
. . . 4
⊢ 𝑉 = (Base‘(𝑅‘𝑥)) |
4 | | prdsbnd.e |
. . . 4
⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) |
5 | | eqid 2738 |
. . . 4
⊢
(dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
6 | | prdsbnd.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
7 | | prdsbnd.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ Fin) |
8 | | fvexd 6689 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
9 | | prdstotbnd.m |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉)) |
10 | | totbndmet 35553 |
. . . . 5
⊢ (𝐸 ∈ (TotBnd‘𝑉) → 𝐸 ∈ (Met‘𝑉)) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsmet 23123 |
. . 3
⊢ (𝜑 → (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) ∈ (Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
13 | | prdsbnd.d |
. . . 4
⊢ 𝐷 = (dist‘𝑌) |
14 | | prdsbnd.y |
. . . . . 6
⊢ 𝑌 = (𝑆Xs𝑅) |
15 | | prdsbnd.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) |
16 | | dffn5 6728 |
. . . . . . . 8
⊢ (𝑅 Fn 𝐼 ↔ 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
17 | 15, 16 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
18 | 17 | oveq2d 7186 |
. . . . . 6
⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
19 | 14, 18 | syl5eq 2785 |
. . . . 5
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))) |
20 | 19 | fveq2d 6678 |
. . . 4
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
21 | 13, 20 | syl5eq 2785 |
. . 3
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
22 | | prdsbnd.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑌) |
23 | 19 | fveq2d 6678 |
. . . . 5
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
24 | 22, 23 | syl5eq 2785 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))))) |
25 | 24 | fveq2d 6678 |
. . 3
⊢ (𝜑 → (Met‘𝐵) =
(Met‘(Base‘(𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)))))) |
26 | 12, 21, 25 | 3eltr4d 2848 |
. 2
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
27 | 7 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐼 ∈ Fin) |
28 | | istotbnd3 35552 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ (TotBnd‘𝑉) ↔ (𝐸 ∈ (Met‘𝑉) ∧ ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
29 | 28 | simprbi 500 |
. . . . . . . . . 10
⊢ (𝐸 ∈ (TotBnd‘𝑉) → ∀𝑟 ∈ ℝ+
∃𝑤 ∈ (𝒫
𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) |
30 | 9, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ (𝒫 𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) |
31 | 30 | r19.21bi 3121 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈ (𝒫
𝑉 ∩ Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) |
32 | | df-rex 3059 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
(𝒫 𝑉 ∩
Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
33 | | rexv 3423 |
. . . . . . . . 9
⊢
(∃𝑤 ∈ V
(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ∃𝑤(𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
34 | 32, 33 | bitr4i 281 |
. . . . . . . 8
⊢
(∃𝑤 ∈
(𝒫 𝑉 ∩
Fin)∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
35 | 31, 34 | sylib 221 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
36 | 35 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
37 | 36 | ralrimiva 3096 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) |
38 | | eleq1 2820 |
. . . . . . 7
⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ↔ (𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin))) |
39 | | iuneq1 4897 |
. . . . . . . 8
⊢ (𝑤 = (𝑓‘𝑥) → ∪
𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟)) |
40 | 39 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑤 = (𝑓‘𝑥) → (∪
𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉 ↔ ∪
𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉)) |
41 | 38, 40 | anbi12d 634 |
. . . . . 6
⊢ (𝑤 = (𝑓‘𝑥) → ((𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉) ↔ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) |
42 | 41 | ac6sfi 8836 |
. . . . 5
⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V (𝑤 ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ 𝑤 (𝑧(ball‘𝐸)𝑟) = 𝑉)) → ∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) |
43 | 27, 37, 42 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑓(𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) |
44 | | elfpw 8899 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ↔ ((𝑓‘𝑥) ⊆ 𝑉 ∧ (𝑓‘𝑥) ∈ Fin)) |
45 | 44 | simplbi 501 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓‘𝑥) ⊆ 𝑉) |
46 | 45 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓‘𝑥) ⊆ 𝑉) |
47 | 46 | ralimi 3075 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝑉) |
48 | 47 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝑉) |
49 | | ss2ixp 8520 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐼 (𝑓‘𝑥) ⊆ 𝑉 → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ X𝑥 ∈ 𝐼 𝑉) |
50 | 48, 49 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ X𝑥 ∈ 𝐼 𝑉) |
51 | | fnfi 8778 |
. . . . . . . . . . 11
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → 𝑅 ∈ Fin) |
52 | 15, 7, 51 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Fin) |
53 | 15 | fndmd 6442 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑅 = 𝐼) |
54 | 14, 6, 52, 22, 53 | prdsbas 16833 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))) |
55 | 3 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑥 ∈
𝐼 𝑉 = (Base‘(𝑅‘𝑥)) |
56 | | ixpeq2 8521 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐼 𝑉 = (Base‘(𝑅‘𝑥)) → X𝑥 ∈ 𝐼 𝑉 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
⊢ X𝑥 ∈
𝐼 𝑉 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)) |
58 | 54, 57 | eqtr4di 2791 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝑉) |
59 | 58 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 = X𝑥 ∈ 𝐼 𝑉) |
60 | 50, 59 | sseqtrrd 3918 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ 𝐵) |
61 | 27 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐼 ∈ Fin) |
62 | 44 | simprbi 500 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) → (𝑓‘𝑥) ∈ Fin) |
63 | 62 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (𝑓‘𝑥) ∈ Fin) |
64 | 63 | ralimi 3075 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin) |
65 | 64 | ad2antll 729 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin) |
66 | | ixpfi 8894 |
. . . . . . 7
⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin) → X𝑥 ∈
𝐼 (𝑓‘𝑥) ∈ Fin) |
67 | 61, 65, 66 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin) |
68 | | elfpw 8899 |
. . . . . 6
⊢ (X𝑥 ∈
𝐼 (𝑓‘𝑥) ∈ (𝒫 𝐵 ∩ Fin) ↔ (X𝑥 ∈
𝐼 (𝑓‘𝑥) ⊆ 𝐵 ∧ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ Fin)) |
69 | 60, 67, 68 | sylanbrc 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ (𝒫 𝐵 ∩ Fin)) |
70 | | metxmet 23087 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (Met‘𝐵) → 𝐷 ∈ (∞Met‘𝐵)) |
71 | 26, 70 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) |
72 | | rpxr 12481 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
73 | | blssm 23171 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
74 | 73 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
75 | 74 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) ∧ 𝑦 ∈ 𝐵) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
76 | 75 | ralrimiva 3096 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑟 ∈ ℝ*) →
∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
77 | 71, 72, 76 | syl2an 599 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
78 | 77 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
79 | | ssralv 3943 |
. . . . . . . 8
⊢ (X𝑥 ∈
𝐼 (𝑓‘𝑥) ⊆ 𝐵 → (∀𝑦 ∈ 𝐵 (𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 → ∀𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵)) |
80 | 60, 78, 79 | sylc 65 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∀𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
81 | | iunss 4931 |
. . . . . . 7
⊢ (∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵 ↔ ∀𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
82 | 80, 81 | sylibr 237 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ⊆ 𝐵) |
83 | 61 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → 𝐼 ∈ Fin) |
84 | 59 | eleq2d 2818 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 ↔ 𝑔 ∈ X𝑥 ∈ 𝐼 𝑉)) |
85 | | vex 3402 |
. . . . . . . . . . . . . . . 16
⊢ 𝑔 ∈ V |
86 | 85 | elixp 8514 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ X𝑥 ∈
𝐼 𝑉 ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉)) |
87 | 86 | simprbi 500 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ X𝑥 ∈
𝐼 𝑉 → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) |
88 | | df-rex 3059 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑧 ∈
(𝑓‘𝑥)(𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧(𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) |
89 | | eliun 4885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔‘𝑥) ∈ ∪
𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ (𝑓‘𝑥)(𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) |
90 | | rexv 3423 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑧 ∈ V
(𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ∃𝑧(𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) |
91 | 88, 89, 90 | 3bitr4i 306 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔‘𝑥) ∈ ∪
𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) ↔ ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) |
92 | | eleq2 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔‘𝑥) ∈ ∪
𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) ↔ (𝑔‘𝑥) ∈ 𝑉)) |
93 | 91, 92 | bitr3id 288 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → (∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ (𝑔‘𝑥) ∈ 𝑉)) |
94 | 93 | biimprd 251 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉 → ((𝑔‘𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))) |
95 | 94 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → ((𝑔‘𝑥) ∈ 𝑉 → ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))) |
96 | 95 | ral2imi 3071 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉) → (∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))) |
97 | 96 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))) |
98 | 87, 97 | syl5 34 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ X𝑥 ∈ 𝐼 𝑉 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))) |
99 | 84, 98 | sylbid 243 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)))) |
100 | 99 | imp 410 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) |
101 | | eleq1 2820 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦‘𝑥) → (𝑧 ∈ (𝑓‘𝑥) ↔ (𝑦‘𝑥) ∈ (𝑓‘𝑥))) |
102 | | oveq1 7177 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦‘𝑥) → (𝑧(ball‘𝐸)𝑟) = ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
103 | 102 | eleq2d 2818 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦‘𝑥) → ((𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟) ↔ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) |
104 | 101, 103 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑦‘𝑥) → ((𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟)) ↔ ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) |
105 | 104 | ac6sfi 8836 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ Fin ∧ ∀𝑥 ∈ 𝐼 ∃𝑧 ∈ V (𝑧 ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ (𝑧(ball‘𝐸)𝑟))) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) |
106 | 83, 100, 105 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) |
107 | | ffn 6504 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦:𝐼⟶V → 𝑦 Fn 𝐼) |
108 | | simpl 486 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → (𝑦‘𝑥) ∈ (𝑓‘𝑥)) |
109 | 108 | ralimi 3075 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ (𝑓‘𝑥)) |
110 | 107, 109 | anim12i 616 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → (𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ (𝑓‘𝑥))) |
111 | | vex 3402 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
112 | 111 | elixp 8514 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ X𝑥 ∈
𝐼 (𝑓‘𝑥) ↔ (𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ (𝑓‘𝑥))) |
113 | 110, 112 | sylibr 237 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → 𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥)) |
114 | 113 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥)) |
115 | 84 | biimpa 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ X𝑥 ∈ 𝐼 𝑉) |
116 | | ixpfn 8513 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ X𝑥 ∈
𝐼 𝑉 → 𝑔 Fn 𝐼) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → 𝑔 Fn 𝐼) |
118 | 117 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑔 Fn 𝐼) |
119 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
120 | 119 | ralimi 3075 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
121 | 120 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
122 | 85 | elixp 8514 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ X𝑥 ∈
𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) |
123 | 118, 121,
122 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
124 | | simp-4l 783 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝜑) |
125 | 50 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → X𝑥 ∈ 𝐼 (𝑓‘𝑥) ⊆ X𝑥 ∈ 𝐼 𝑉) |
126 | 125, 114 | sseldd 3878 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑦 ∈ X𝑥 ∈ 𝐼 𝑉) |
127 | 124, 58 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝐵 = X𝑥 ∈ 𝐼 𝑉) |
128 | 126, 127 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑦 ∈ 𝐵) |
129 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑟 ∈ ℝ+) |
130 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥)) |
131 | 130 | cbvmptv 5133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)) = (𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥)) |
132 | 131 | oveq2i 7181 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))) = (𝑆Xs(𝑥 ∈ 𝐼 ↦ (𝑅‘𝑥))) |
133 | 19, 132 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
134 | 133 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
135 | 13, 134 | syl5eq 2785 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
136 | 135 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ball‘𝐷) =
(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))) |
137 | 136 | oveqdr 7198 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟)) |
138 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
139 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) = (dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))) |
140 | 6 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑆 ∈ 𝑊) |
141 | 7 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐼 ∈ Fin) |
142 | | fvexd 6689 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → (𝑅‘𝑥) ∈ V) |
143 | | metxmet 23087 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉)) |
144 | 11, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
145 | 144 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
146 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ 𝐵) |
147 | 133 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
148 | 22, 147 | syl5eq 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
149 | 148 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝐵 = (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
150 | 146, 149 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑦 ∈ (Base‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦))))) |
151 | 72 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ*) |
152 | | rpgt0 12484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
153 | 152 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → 0 <
𝑟) |
154 | 132, 138,
3, 4, 139, 140, 141, 142, 145, 150, 151, 153 | prdsbl 23244 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘(dist‘(𝑆Xs(𝑦 ∈ 𝐼 ↦ (𝑅‘𝑦)))))𝑟) = X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
155 | 137, 154 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+)) → (𝑦(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
156 | 124, 128,
129, 155 | syl12anc 836 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → (𝑦(ball‘𝐷)𝑟) = X𝑥 ∈ 𝐼 ((𝑦‘𝑥)(ball‘𝐸)𝑟)) |
157 | 123, 156 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)) |
158 | 114, 157 | jca 515 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ ℝ+)
∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) ∧ (𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟)))) → (𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))) |
159 | 158 | ex 416 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ((𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → (𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))) |
160 | 159 | eximdv 1924 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → ∃𝑦(𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟)))) |
161 | | df-rex 3059 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
X 𝑥
∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦(𝑦 ∈ X𝑥 ∈ 𝐼 (𝑓‘𝑥) ∧ 𝑔 ∈ (𝑦(ball‘𝐷)𝑟))) |
162 | 160, 161 | syl6ibr 255 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → (∃𝑦(𝑦:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑦‘𝑥) ∈ (𝑓‘𝑥) ∧ (𝑔‘𝑥) ∈ ((𝑦‘𝑥)(ball‘𝐸)𝑟))) → ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))) |
163 | 106, 162 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) ∧ 𝑔 ∈ 𝐵) → ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)) |
164 | 163 | ex 416 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 → ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟))) |
165 | | eliun 4885 |
. . . . . . . 8
⊢ (𝑔 ∈ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)𝑔 ∈ (𝑦(ball‘𝐷)𝑟)) |
166 | 164, 165 | syl6ibr 255 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → (𝑔 ∈ 𝐵 → 𝑔 ∈ ∪
𝑦 ∈ X 𝑥 ∈
𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟))) |
167 | 166 | ssrdv 3883 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → 𝐵 ⊆ ∪
𝑦 ∈ X 𝑥 ∈
𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟)) |
168 | 82, 167 | eqssd 3894 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵) |
169 | | iuneq1 4897 |
. . . . . . 7
⊢ (𝑣 = X𝑥 ∈ 𝐼 (𝑓‘𝑥) → ∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = ∪ 𝑦 ∈ X
𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟)) |
170 | 169 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑣 = X𝑥 ∈ 𝐼 (𝑓‘𝑥) → (∪
𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵 ↔ ∪
𝑦 ∈ X 𝑥 ∈
𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵)) |
171 | 170 | rspcev 3526 |
. . . . 5
⊢ ((X𝑥 ∈
𝐼 (𝑓‘𝑥) ∈ (𝒫 𝐵 ∩ Fin) ∧ ∪ 𝑦 ∈ X 𝑥 ∈ 𝐼 (𝑓‘𝑥)(𝑦(ball‘𝐷)𝑟) = 𝐵) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵) |
172 | 69, 168, 171 | syl2anc 587 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑓:𝐼⟶V ∧ ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ (𝒫 𝑉 ∩ Fin) ∧ ∪ 𝑧 ∈ (𝑓‘𝑥)(𝑧(ball‘𝐸)𝑟) = 𝑉))) → ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵) |
173 | 43, 172 | exlimddv 1942 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑣 ∈ (𝒫
𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵) |
174 | 173 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵) |
175 | | istotbnd3 35552 |
. 2
⊢ (𝐷 ∈ (TotBnd‘𝐵) ↔ (𝐷 ∈ (Met‘𝐵) ∧ ∀𝑟 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝐵 ∩ Fin)∪ 𝑦 ∈ 𝑣 (𝑦(ball‘𝐷)𝑟) = 𝐵)) |
176 | 26, 174, 175 | sylanbrc 586 |
1
⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵)) |