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 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )