Step | Hyp | Ref
| Expression |
1 | | prdsbas.p |
. . 3
⊢ 𝑃 = (𝑆Xs𝑅) |
2 | | eqid 2795 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | prdsbas.i |
. . 3
⊢ (𝜑 → dom 𝑅 = 𝐼) |
4 | | prdsbas.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
5 | | prdsbas.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑊) |
6 | | prdsbas.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
7 | 1, 4, 5, 6, 3 | prdsbas 16564 |
. . 3
⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))) |
8 | | eqid 2795 |
. . . 4
⊢
(+g‘𝑃) = (+g‘𝑃) |
9 | 1, 4, 5, 6, 3, 8 | prdsplusg 16565 |
. . 3
⊢ (𝜑 → (+g‘𝑃) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))) |
10 | | eqid 2795 |
. . . 4
⊢
(.r‘𝑃) = (.r‘𝑃) |
11 | 1, 4, 5, 6, 3, 10 | prdsmulr 16566 |
. . 3
⊢ (𝜑 → (.r‘𝑃) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))) |
12 | | eqid 2795 |
. . . 4
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
13 | 1, 4, 5, 6, 3, 2, 12 | prdsvsca 16567 |
. . 3
⊢ (𝜑 → (
·𝑠 ‘𝑃) = (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))) |
14 | | eqidd 2796 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))) |
15 | | eqidd 2796 |
. . 3
⊢ (𝜑 →
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅))) |
16 | | eqid 2795 |
. . . 4
⊢
(le‘𝑃) =
(le‘𝑃) |
17 | 1, 4, 5, 6, 3, 16 | prdsle 16569 |
. . 3
⊢ (𝜑 → (le‘𝑃) = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}) |
18 | | eqidd 2796 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))) |
19 | | eqidd 2796 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))) |
20 | | eqidd 2796 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))) |
21 | 1, 2, 3, 7, 9, 11,
13, 14, 15, 17, 18, 19, 20, 4, 5 | prdsval 16562 |
. 2
⊢ (𝜑 → 𝑃 = (({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑃)〉, 〈(.r‘ndx),
(.r‘𝑃)〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑃)〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx), (le‘𝑃)〉, 〈(dist‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) |
22 | | prdsds.l |
. 2
⊢ 𝐷 = (dist‘𝑃) |
23 | | dsid 16510 |
. 2
⊢ dist =
Slot (dist‘ndx) |
24 | | df-sup 8757 |
. . . . . . 7
⊢ sup((ran
(𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ) =
∪ {𝑦 ∈ ℝ* ∣
(∀𝑧 ∈ (ran
(𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} |
25 | | xrex 12241 |
. . . . . . . . 9
⊢
ℝ* ∈ V |
26 | 25 | uniex 7328 |
. . . . . . . 8
⊢ ∪ ℝ* ∈ V |
27 | | ssrab2 3981 |
. . . . . . . . 9
⊢ {𝑦 ∈ ℝ*
∣ (∀𝑧 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ⊆
ℝ* |
28 | 27 | unissi 4772 |
. . . . . . . 8
⊢ ∪ {𝑦
∈ ℝ* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ⊆ ∪
ℝ* |
29 | 26, 28 | elpwi2 5145 |
. . . . . . 7
⊢ ∪ {𝑦
∈ ℝ* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ∈ 𝒫 ∪ ℝ* |
30 | 24, 29 | eqeltri 2879 |
. . . . . 6
⊢ sup((ran
(𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ 𝒫 ∪
ℝ* |
31 | 30 | rgen2w 3118 |
. . . . 5
⊢
∀𝑓 ∈
𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ 𝒫 ∪
ℝ* |
32 | | eqid 2795 |
. . . . . 6
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
33 | 32 | fmpo 7627 |
. . . . 5
⊢
(∀𝑓 ∈
𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ 𝒫 ∪ ℝ* ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶𝒫 ∪ ℝ*) |
34 | 31, 33 | mpbi 231 |
. . . 4
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶𝒫 ∪ ℝ* |
35 | 6 | fvexi 6557 |
. . . . 5
⊢ 𝐵 ∈ V |
36 | 35, 35 | xpex 7338 |
. . . 4
⊢ (𝐵 × 𝐵) ∈ V |
37 | 26 | pwex 5177 |
. . . 4
⊢ 𝒫
∪ ℝ* ∈ V |
38 | | fex2 7499 |
. . . 4
⊢ (((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶𝒫 ∪ ℝ* ∧ (𝐵 × 𝐵) ∈ V ∧ 𝒫 ∪ ℝ* ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
∈ V) |
39 | 34, 36, 37, 38 | mp3an 1453 |
. . 3
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
∈ V |
40 | 39 | a1i 11 |
. 2
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
∈ V) |
41 | | snsstp3 4662 |
. . . 4
⊢
{〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ⊆ {〈(TopSet‘ndx), (∏t‘(TopOpen
∘ 𝑅))〉,
〈(le‘ndx), (le‘𝑃)〉, 〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} |
42 | | ssun1 4073 |
. . . 4
⊢
{〈(TopSet‘ndx), (∏t‘(TopOpen ∘
𝑅))〉,
〈(le‘ndx), (le‘𝑃)〉, 〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ⊆ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx),
(le‘𝑃)〉,
〈(dist‘ndx), (𝑓
∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}) |
43 | 41, 42 | sstri 3902 |
. . 3
⊢
{〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ⊆ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx),
(le‘𝑃)〉,
〈(dist‘ndx), (𝑓
∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}) |
44 | | ssun2 4074 |
. . 3
⊢
({〈(TopSet‘ndx), (∏t‘(TopOpen ∘
𝑅))〉,
〈(le‘ndx), (le‘𝑃)〉, 〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}) ⊆
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑃)〉, 〈(.r‘ndx),
(.r‘𝑃)〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑃)〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx), (le‘𝑃)〉, 〈(dist‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉})) |
45 | 43, 44 | sstri 3902 |
. 2
⊢
{〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ⊆ (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑃)〉, 〈(.r‘ndx),
(.r‘𝑃)〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (
·𝑠 ‘𝑃)〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx), (le‘𝑃)〉, 〈(dist‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉})) |
46 | 21, 22, 23, 40, 45 | prdsvallem 16561 |
1
⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))) |