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)

		Ref	Expression
	Assertion	df-prds	$⊢ ⨉_{𝑠} = (s \in V, r \in V ⟼ ⦋ \underset{x \in dom r}{⨉} {Base}_{r (x)} / v ⦌ ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (c h 2^{nd} (a)), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})))$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-prds

Detailed syntax breakdown