Step | Hyp | Ref
| Expression |
1 | | prdsbas.p |
. . 3
⊢ 𝑃 = (𝑆Xs𝑅) |
2 | | eqid 2739 |
. . 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 17177 |
. . 3
⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))) |
8 | | eqid 2739 |
. . . 4
⊢
(+g‘𝑃) = (+g‘𝑃) |
9 | 1, 4, 5, 6, 3, 8 | prdsplusg 17178 |
. . 3
⊢ (𝜑 → (+g‘𝑃) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))) |
10 | | eqidd 2740 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))) |
11 | | eqidd 2740 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))) |
12 | | eqidd 2740 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))) |
13 | | eqidd 2740 |
. . 3
⊢ (𝜑 →
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅))) |
14 | | eqidd 2740 |
. . 3
⊢ (𝜑 → {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}) |
15 | | eqidd 2740 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))) |
16 | | eqidd 2740 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))) |
17 | | eqidd 2740 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))𝑐), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))𝑐), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))) |
18 | 1, 2, 3, 7, 9, 10,
11, 12, 13, 14, 15, 16, 17, 4, 5 | prdsval 17175 |
. 2
⊢ (𝜑 → 𝑃 = (({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))𝑐), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) |
19 | | prdsmulr.t |
. 2
⊢ · =
(.r‘𝑃) |
20 | | mulrid 17013 |
. 2
⊢
.r = Slot (.r‘ndx) |
21 | | ovssunirn 7320 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran
(.r‘(𝑅‘𝑥)) |
22 | 20 | strfvss 16897 |
. . . . . . . . . . . . 13
⊢
(.r‘(𝑅‘𝑥)) ⊆ ∪ ran
(𝑅‘𝑥) |
23 | | fvssunirn 6812 |
. . . . . . . . . . . . . 14
⊢ (𝑅‘𝑥) ⊆ ∪ ran
𝑅 |
24 | | rnss 5851 |
. . . . . . . . . . . . . 14
⊢ ((𝑅‘𝑥) ⊆ ∪ ran
𝑅 → ran (𝑅‘𝑥) ⊆ ran ∪
ran 𝑅) |
25 | | uniss 4848 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑅‘𝑥) ⊆ ran ∪
ran 𝑅 → ∪ ran (𝑅‘𝑥) ⊆ ∪ ran
∪ ran 𝑅) |
26 | 23, 24, 25 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ ∪ ran (𝑅‘𝑥) ⊆ ∪ ran
∪ ran 𝑅 |
27 | 22, 26 | sstri 3931 |
. . . . . . . . . . . 12
⊢
(.r‘(𝑅‘𝑥)) ⊆ ∪ ran
∪ ran 𝑅 |
28 | | rnss 5851 |
. . . . . . . . . . . 12
⊢
((.r‘(𝑅‘𝑥)) ⊆ ∪ ran
∪ ran 𝑅 → ran (.r‘(𝑅‘𝑥)) ⊆ ran ∪
ran ∪ ran 𝑅) |
29 | | uniss 4848 |
. . . . . . . . . . . 12
⊢ (ran
(.r‘(𝑅‘𝑥)) ⊆ ran ∪
ran ∪ ran 𝑅 → ∪ ran
(.r‘(𝑅‘𝑥)) ⊆ ∪ ran
∪ ran ∪ ran 𝑅) |
30 | 27, 28, 29 | mp2b 10 |
. . . . . . . . . . 11
⊢ ∪ ran (.r‘(𝑅‘𝑥)) ⊆ ∪ ran
∪ ran ∪ ran 𝑅 |
31 | 21, 30 | sstri 3931 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran
∪ ran ∪ ran 𝑅 |
32 | | ovex 7317 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ∈ V |
33 | 32 | elpw 4538 |
. . . . . . . . . 10
⊢ (((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↔ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ⊆ ∪ ran
∪ ran ∪ ran 𝑅) |
34 | 31, 33 | mpbir 230 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅) |
36 | 35 | fmpttd 6998 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))):𝐼⟶𝒫 ∪ ran ∪ ran ∪ ran 𝑅) |
37 | | rnexg 7760 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑊 → ran 𝑅 ∈ V) |
38 | | uniexg 7602 |
. . . . . . . . . . . 12
⊢ (ran
𝑅 ∈ V → ∪ ran 𝑅 ∈ V) |
39 | 5, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ ran 𝑅 ∈ V) |
40 | | rnexg 7760 |
. . . . . . . . . . 11
⊢ (∪ ran 𝑅 ∈ V → ran ∪ ran 𝑅 ∈ V) |
41 | | uniexg 7602 |
. . . . . . . . . . 11
⊢ (ran
∪ ran 𝑅 ∈ V → ∪ ran ∪ ran 𝑅 ∈ V) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran ∪ ran 𝑅 ∈ V) |
43 | | rnexg 7760 |
. . . . . . . . . 10
⊢ (∪ ran ∪ ran 𝑅 ∈ V → ran ∪ ran ∪ ran 𝑅 ∈ V) |
44 | | uniexg 7602 |
. . . . . . . . . 10
⊢ (ran
∪ ran ∪ ran 𝑅 ∈ V → ∪ ran ∪ ran ∪ ran 𝑅 ∈ V) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran ∪ ran ∪ ran 𝑅 ∈ V) |
46 | 45 | pwexd 5303 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ∈ V) |
47 | 5 | dmexd 7761 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑅 ∈ V) |
48 | 3, 47 | eqeltrrd 2841 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ V) |
49 | 46, 48 | elmapd 8638 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼) ↔ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))):𝐼⟶𝒫 ∪ ran ∪ ran ∪ ran 𝑅)) |
50 | 36, 49 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼)) |
51 | 50 | ralrimivw 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑔 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼)) |
52 | 51 | ralrimivw 3105 |
. . . 4
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼)) |
53 | | eqid 2739 |
. . . . 5
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) |
54 | 53 | fmpo 7917 |
. . . 4
⊢
(∀𝑓 ∈
𝐵 ∀𝑔 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼) ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))):(𝐵 × 𝐵)⟶(𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼)) |
55 | 52, 54 | sylib 217 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))):(𝐵 × 𝐵)⟶(𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼)) |
56 | 6 | fvexi 6797 |
. . . . 5
⊢ 𝐵 ∈ V |
57 | 56, 56 | xpex 7612 |
. . . 4
⊢ (𝐵 × 𝐵) ∈ V |
58 | | ovex 7317 |
. . . 4
⊢
(𝒫 ∪ ran ∪
ran ∪ ran 𝑅 ↑m 𝐼) ∈ V |
59 | | fex2 7789 |
. . . 4
⊢ (((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))):(𝐵 × 𝐵)⟶(𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼) ∧ (𝐵 × 𝐵) ∈ V ∧ (𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼) ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V) |
60 | 57, 58, 59 | mp3an23 1452 |
. . 3
⊢ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))):(𝐵 × 𝐵)⟶(𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V) |
61 | 55, 60 | syl 17 |
. 2
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V) |
62 | | snsstp3 4752 |
. . . 4
⊢
{〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ⊆ {〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} |
63 | | ssun1 4107 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ⊆ ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) |
64 | 62, 63 | sstri 3931 |
. . 3
⊢
{〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ⊆ ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) |
65 | | ssun1 4107 |
. . 3
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ⊆ (({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑃)〉, 〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))𝑐), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉})) |
66 | 64, 65 | sstri 3931 |
. 2
⊢
{〈(.r‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ⊆
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑃)〉, 〈(.r‘ndx),
(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠
‘(𝑅‘𝑥))(𝑔‘𝑥))))〉,
〈(·𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx),
(∏t‘(TopOpen ∘ 𝑅))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, <
))〉} ∪ {〈(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))〉, 〈(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))𝑐), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉})) |
67 | 18, 19, 20, 61, 66 | prdsbaslem 17173 |
1
⊢ (𝜑 → · = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))) |