Metamath Proof Explorer


Definition df-prds

Description: Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Thierry Arnoux, 15-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Assertion df-prds Xs = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) / 𝑣 ( 𝑓𝑣 , 𝑔𝑣X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) / ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprds Xs
1 vs 𝑠
2 cvv V
3 vr 𝑟
4 vx 𝑥
5 3 cv 𝑟
6 5 cdm dom 𝑟
7 cbs Base
8 4 cv 𝑥
9 8 5 cfv ( 𝑟𝑥 )
10 9 7 cfv ( Base ‘ ( 𝑟𝑥 ) )
11 4 6 10 cixp X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) )
12 vv 𝑣
13 vf 𝑓
14 12 cv 𝑣
15 vg 𝑔
16 13 cv 𝑓
17 8 16 cfv ( 𝑓𝑥 )
18 chom Hom
19 9 18 cfv ( Hom ‘ ( 𝑟𝑥 ) )
20 15 cv 𝑔
21 8 20 cfv ( 𝑔𝑥 )
22 17 21 19 co ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
23 4 6 22 cixp X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
24 13 15 14 14 23 cmpo ( 𝑓𝑣 , 𝑔𝑣X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
25 vh
26 cnx ndx
27 26 7 cfv ( Base ‘ ndx )
28 27 14 cop ⟨ ( Base ‘ ndx ) , 𝑣
29 cplusg +g
30 26 29 cfv ( +g ‘ ndx )
31 9 29 cfv ( +g ‘ ( 𝑟𝑥 ) )
32 17 21 31 co ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
33 4 6 32 cmpt ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
34 13 15 14 14 33 cmpo ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) )
35 30 34 cop ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩
36 cmulr .r
37 26 36 cfv ( .r ‘ ndx )
38 9 36 cfv ( .r ‘ ( 𝑟𝑥 ) )
39 17 21 38 co ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
40 4 6 39 cmpt ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
41 13 15 14 14 40 cmpo ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) )
42 37 41 cop ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩
43 28 35 42 ctp { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ }
44 csca Scalar
45 26 44 cfv ( Scalar ‘ ndx )
46 1 cv 𝑠
47 45 46 cop ⟨ ( Scalar ‘ ndx ) , 𝑠
48 cvsca ·𝑠
49 26 48 cfv ( ·𝑠 ‘ ndx )
50 46 7 cfv ( Base ‘ 𝑠 )
51 9 48 cfv ( ·𝑠 ‘ ( 𝑟𝑥 ) )
52 16 21 51 co ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
53 4 6 52 cmpt ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
54 13 15 50 14 53 cmpo ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) )
55 49 54 cop ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩
56 cip ·𝑖
57 26 56 cfv ( ·𝑖 ‘ ndx )
58 cgsu Σg
59 9 56 cfv ( ·𝑖 ‘ ( 𝑟𝑥 ) )
60 17 21 59 co ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
61 4 6 60 cmpt ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
62 46 61 58 co ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) )
63 13 15 14 14 62 cmpo ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) )
64 57 63 cop ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩
65 47 55 64 ctp { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ }
66 43 65 cun ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } )
67 cts TopSet
68 26 67 cfv ( TopSet ‘ ndx )
69 cpt t
70 ctopn TopOpen
71 70 5 ccom ( TopOpen ∘ 𝑟 )
72 71 69 cfv ( ∏t ‘ ( TopOpen ∘ 𝑟 ) )
73 68 72 cop ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩
74 cple le
75 26 74 cfv ( le ‘ ndx )
76 16 20 cpr { 𝑓 , 𝑔 }
77 76 14 wss { 𝑓 , 𝑔 } ⊆ 𝑣
78 9 74 cfv ( le ‘ ( 𝑟𝑥 ) )
79 17 21 78 wbr ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 )
80 79 4 6 wral 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 )
81 77 80 wa ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
82 81 13 15 copab { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) }
83 75 82 cop ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩
84 cds dist
85 26 84 cfv ( dist ‘ ndx )
86 9 84 cfv ( dist ‘ ( 𝑟𝑥 ) )
87 17 21 86 co ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) )
88 4 6 87 cmpt ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
89 88 crn ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) )
90 cc0 0
91 90 csn { 0 }
92 89 91 cun ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } )
93 cxr *
94 clt <
95 92 93 94 csup sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < )
96 13 15 14 14 95 cmpo ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
97 85 96 cop ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩
98 73 83 97 ctp { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ }
99 26 18 cfv ( Hom ‘ ndx )
100 25 cv
101 99 100 cop ⟨ ( Hom ‘ ndx ) ,
102 cco comp
103 26 102 cfv ( comp ‘ ndx )
104 va 𝑎
105 14 14 cxp ( 𝑣 × 𝑣 )
106 vc 𝑐
107 vd 𝑑
108 c2nd 2nd
109 104 cv 𝑎
110 109 108 cfv ( 2nd𝑎 )
111 106 cv 𝑐
112 110 111 100 co ( ( 2nd𝑎 ) 𝑐 )
113 ve 𝑒
114 109 100 cfv ( 𝑎 )
115 107 cv 𝑑
116 8 115 cfv ( 𝑑𝑥 )
117 c1st 1st
118 109 117 cfv ( 1st𝑎 )
119 8 118 cfv ( ( 1st𝑎 ) ‘ 𝑥 )
120 8 110 cfv ( ( 2nd𝑎 ) ‘ 𝑥 )
121 119 120 cop ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩
122 9 102 cfv ( comp ‘ ( 𝑟𝑥 ) )
123 8 111 cfv ( 𝑐𝑥 )
124 121 123 122 co ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) )
125 113 cv 𝑒
126 8 125 cfv ( 𝑒𝑥 )
127 116 126 124 co ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) )
128 4 6 127 cmpt ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) )
129 107 113 112 114 128 cmpo ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) )
130 104 106 105 14 129 cmpo ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) )
131 103 130 cop ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩
132 101 131 cpr { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ }
133 98 132 cun ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } )
134 66 133 cun ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
135 25 24 134 csb ( 𝑓𝑣 , 𝑔𝑣X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) / ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
136 12 11 135 csb X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) / 𝑣 ( 𝑓𝑣 , 𝑔𝑣X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) / ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) )
137 1 3 2 2 136 cmpo ( 𝑠 ∈ V , 𝑟 ∈ V ↦ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) / 𝑣 ( 𝑓𝑣 , 𝑔𝑣X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) / ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ) )
138 0 137 wceq Xs = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟𝑥 ) ) / 𝑣 ( 𝑓𝑣 , 𝑔𝑣X 𝑥 ∈ dom 𝑟 ( ( 𝑓𝑥 ) ( Hom ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) / ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( +g ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( .r ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ ( 𝑠 Σg ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( ·𝑖 ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓𝑥 ) ( le ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓𝑣 , 𝑔𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓𝑥 ) ( dist ‘ ( 𝑟𝑥 ) ) ( 𝑔𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐𝑣 ↦ ( 𝑑 ∈ ( ( 2nd𝑎 ) 𝑐 ) , 𝑒 ∈ ( 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑𝑥 ) ( ⟨ ( ( 1st𝑎 ) ‘ 𝑥 ) , ( ( 2nd𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟𝑥 ) ) ( 𝑐𝑥 ) ) ( 𝑒𝑥 ) ) ) ) ) ⟩ } ) ) )