Definition df-imas 17680

Description: Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly 𝑓 must either be injective or satisfy the well-definedness condition 𝑓(𝑎) = 𝑓(𝑐) ∧ 𝑓(𝑏) = 𝑓(𝑑) → 𝑓(𝑎 + 𝑏) = 𝑓(𝑐 + 𝑑) for each relevant operation.

Note that although we call this an "image" by association to df-ima 5664, in order to keep the definition simple we consider only the case when the domain of 𝐹 is equal to the base set of 𝑅. Other cases can be achieved by restricting 𝐹 (with df-res 5663) and/or 𝑅 ( with df-ress 17409) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)

Assertion

Ref

Expression

df-imas

⊢ “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))

Distinct variable group:   𝑓,𝑔,ℎ,𝑖,𝑛,𝑝,𝑞,𝑟,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-imas

Step	Hyp	Ref	Expression
1		cimas 17676	. 2 class “s
2		vf	. . 3 setvar 𝑓
3		vr	. . 3 setvar 𝑟
4		cvv 3451	. . 3 class V
5		vv	. . . 4 setvar 𝑣
6	3	cv 1569	. . . . 5 class 𝑟
7		cbs 17387	. . . . 5 class Base
8	6, 7	cfv 6538	. . . 4 class (Base‘𝑟)
9		cnx 17371	. . . . . . . . 9 class ndx
10	9, 7	cfv 6538	. . . . . . . 8 class (Base‘ndx)
11	2	cv 1569	. . . . . . . . 9 class 𝑓
12	11	crn 5652	. . . . . . . 8 class ran 𝑓
13	10, 12	cop 4590	. . . . . . 7 class ⟨(Base‘ndx), ran 𝑓⟩
14		cplusg 17428	. . . . . . . . 9 class +g
15	9, 14	cfv 6538	. . . . . . . 8 class (+g‘ndx)
16		vp	. . . . . . . . 9 setvar 𝑝
17	5	cv 1569	. . . . . . . . 9 class 𝑣
18		vq	. . . . . . . . . 10 setvar 𝑞
19	16	cv 1569	. . . . . . . . . . . . . 14 class 𝑝
20	19, 11	cfv 6538	. . . . . . . . . . . . 13 class (𝑓‘𝑝)
21	18	cv 1569	. . . . . . . . . . . . . 14 class 𝑞
22	21, 11	cfv 6538	. . . . . . . . . . . . 13 class (𝑓‘𝑞)
23	20, 22	cop 4590	. . . . . . . . . . . 12 class ⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩
24	6, 14	cfv 6538	. . . . . . . . . . . . . 14 class (+g‘𝑟)
25	19, 21, 24	co 7420	. . . . . . . . . . . . 13 class (𝑝(+g‘𝑟)𝑞)
26	25, 11	cfv 6538	. . . . . . . . . . . 12 class (𝑓‘(𝑝(+g‘𝑟)𝑞))
27	23, 26	cop 4590	. . . . . . . . . . 11 class ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩
28	27	csn 4584	. . . . . . . . . 10 class {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}
29	18, 17, 28	ciun 4951	. . . . . . . . 9 class ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}
30	16, 17, 29	ciun 4951	. . . . . . . 8 class ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}
31	15, 30	cop 4590	. . . . . . 7 class ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩
32		cmulr 17429	. . . . . . . . 9 class .r
33	9, 32	cfv 6538	. . . . . . . 8 class (.r‘ndx)
34	6, 32	cfv 6538	. . . . . . . . . . . . . 14 class (.r‘𝑟)
35	19, 21, 34	co 7420	. . . . . . . . . . . . 13 class (𝑝(.r‘𝑟)𝑞)
36	35, 11	cfv 6538	. . . . . . . . . . . 12 class (𝑓‘(𝑝(.r‘𝑟)𝑞))
37	23, 36	cop 4590	. . . . . . . . . . 11 class ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩
38	37	csn 4584	. . . . . . . . . 10 class {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}
39	18, 17, 38	ciun 4951	. . . . . . . . 9 class ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}
40	16, 17, 39	ciun 4951	. . . . . . . 8 class ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}
41	33, 40	cop 4590	. . . . . . 7 class ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩
42	13, 31, 41	ctp 4588	. . . . . 6 class {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩}
43		csca 17431	. . . . . . . . 9 class Scalar
44	9, 43	cfv 6538	. . . . . . . 8 class (Scalar‘ndx)
45	6, 43	cfv 6538	. . . . . . . 8 class (Scalar‘𝑟)
46	44, 45	cop 4590	. . . . . . 7 class ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩
47		cvsca 17432	. . . . . . . . 9 class ·𝑠
48	9, 47	cfv 6538	. . . . . . . 8 class ( ·𝑠 ‘ndx)
49		vx	. . . . . . . . . 10 setvar 𝑥
50	45, 7	cfv 6538	. . . . . . . . . 10 class (Base‘(Scalar‘𝑟))
51	22	csn 4584	. . . . . . . . . 10 class {(𝑓‘𝑞)}
52	6, 47	cfv 6538	. . . . . . . . . . . 12 class ( ·𝑠 ‘𝑟)
53	19, 21, 52	co 7420	. . . . . . . . . . 11 class (𝑝( ·𝑠 ‘𝑟)𝑞)
54	53, 11	cfv 6538	. . . . . . . . . 10 class (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))
55	16, 49, 50, 51, 54	cmpo 7422	. . . . . . . . 9 class (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))
56	18, 17, 55	ciun 4951	. . . . . . . 8 class ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))
57	48, 56	cop 4590	. . . . . . 7 class ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩
58		cip 17433	. . . . . . . . 9 class ·𝑖
59	9, 58	cfv 6538	. . . . . . . 8 class (·𝑖‘ndx)
60	6, 58	cfv 6538	. . . . . . . . . . . . 13 class (·𝑖‘𝑟)
61	19, 21, 60	co 7420	. . . . . . . . . . . 12 class (𝑝(·𝑖‘𝑟)𝑞)
62	23, 61	cop 4590	. . . . . . . . . . 11 class ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩
63	62	csn 4584	. . . . . . . . . 10 class {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}
64	18, 17, 63	ciun 4951	. . . . . . . . 9 class ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}
65	16, 17, 64	ciun 4951	. . . . . . . 8 class ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}
66	59, 65	cop 4590	. . . . . . 7 class ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩
67	46, 57, 66	ctp 4588	. . . . . 6 class {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩}
68	42, 67	cun 3897	. . . . 5 class ({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩})
69		cts 17434	. . . . . . . 8 class TopSet
70	9, 69	cfv 6538	. . . . . . 7 class (TopSet‘ndx)
71		ctopn 17592	. . . . . . . . 9 class TopOpen
72	6, 71	cfv 6538	. . . . . . . 8 class (TopOpen‘𝑟)
73		cqtop 17675	. . . . . . . 8 class qTop
74	72, 11, 73	co 7420	. . . . . . 7 class ((TopOpen‘𝑟) qTop 𝑓)
75	70, 74	cop 4590	. . . . . 6 class ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩
76		cple 17435	. . . . . . . 8 class le
77	9, 76	cfv 6538	. . . . . . 7 class (le‘ndx)
78	6, 76	cfv 6538	. . . . . . . . 9 class (le‘𝑟)
79	11, 78	ccom 5655	. . . . . . . 8 class (𝑓 ∘ (le‘𝑟))
80	11	ccnv 5650	. . . . . . . 8 class ◡𝑓
81	79, 80	ccom 5655	. . . . . . 7 class ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)
82	77, 81	cop 4590	. . . . . 6 class ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩
83		cds 17437	. . . . . . . 8 class dist
84	9, 83	cfv 6538	. . . . . . 7 class (dist‘ndx)
85		vy	. . . . . . . 8 setvar 𝑦
86		vn	. . . . . . . . . 10 setvar 𝑛
87		cn 12335	. . . . . . . . . 10 class ℕ
88		vg	. . . . . . . . . . . 12 setvar 𝑔
89		c1 11201	. . . . . . . . . . . . . . . . . 18 class 1
90		vh	. . . . . . . . . . . . . . . . . . 19 setvar ℎ
91	90	cv 1569	. . . . . . . . . . . . . . . . . 18 class ℎ
92	89, 91	cfv 6538	. . . . . . . . . . . . . . . . 17 class (ℎ‘1)
93		c1st 7999	. . . . . . . . . . . . . . . . 17 class 1st
94	92, 93	cfv 6538	. . . . . . . . . . . . . . . 16 class (1st ‘(ℎ‘1))
95	94, 11	cfv 6538	. . . . . . . . . . . . . . 15 class (𝑓‘(1st ‘(ℎ‘1)))
96	49	cv 1569	. . . . . . . . . . . . . . 15 class 𝑥
97	95, 96	wceq 1570	. . . . . . . . . . . . . 14 wff (𝑓‘(1st ‘(ℎ‘1))) = 𝑥
98	86	cv 1569	. . . . . . . . . . . . . . . . . 18 class 𝑛
99	98, 91	cfv 6538	. . . . . . . . . . . . . . . . 17 class (ℎ‘𝑛)
100		c2nd 8000	. . . . . . . . . . . . . . . . 17 class 2nd
101	99, 100	cfv 6538	. . . . . . . . . . . . . . . 16 class (2nd ‘(ℎ‘𝑛))
102	101, 11	cfv 6538	. . . . . . . . . . . . . . 15 class (𝑓‘(2nd ‘(ℎ‘𝑛)))
103	85	cv 1569	. . . . . . . . . . . . . . 15 class 𝑦
104	102, 103	wceq 1570	. . . . . . . . . . . . . 14 wff (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦
105		vi	. . . . . . . . . . . . . . . . . . . 20 setvar 𝑖
106	105	cv 1569	. . . . . . . . . . . . . . . . . . 19 class 𝑖
107	106, 91	cfv 6538	. . . . . . . . . . . . . . . . . 18 class (ℎ‘𝑖)
108	107, 100	cfv 6538	. . . . . . . . . . . . . . . . 17 class (2nd ‘(ℎ‘𝑖))
109	108, 11	cfv 6538	. . . . . . . . . . . . . . . 16 class (𝑓‘(2nd ‘(ℎ‘𝑖)))
110		caddc 11203	. . . . . . . . . . . . . . . . . . . 20 class +
111	106, 89, 110	co 7420	. . . . . . . . . . . . . . . . . . 19 class (𝑖 + 1)
112	111, 91	cfv 6538	. . . . . . . . . . . . . . . . . 18 class (ℎ‘(𝑖 + 1))
113	112, 93	cfv 6538	. . . . . . . . . . . . . . . . 17 class (1st ‘(ℎ‘(𝑖 + 1)))
114	113, 11	cfv 6538	. . . . . . . . . . . . . . . 16 class (𝑓‘(1st ‘(ℎ‘(𝑖 + 1))))
115	109, 114	wceq 1570	. . . . . . . . . . . . . . 15 wff (𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1))))
116		cmin 11541	. . . . . . . . . . . . . . . . 17 class −
117	98, 89, 116	co 7420	. . . . . . . . . . . . . . . 16 class (𝑛 − 1)
118		cfz 13639	. . . . . . . . . . . . . . . 16 class ...
119	89, 117, 118	co 7420	. . . . . . . . . . . . . . 15 class (1...(𝑛 − 1))
120	115, 105, 119	wral 3077	. . . . . . . . . . . . . 14 wff ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1))))
121	97, 104, 120	w3a 1103	. . . . . . . . . . . . 13 wff ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))
122	17, 17	cxp 5649	. . . . . . . . . . . . . 14 class (𝑣 × 𝑣)
123	89, 98, 118	co 7420	. . . . . . . . . . . . . 14 class (1...𝑛)
124		cmap 8847	. . . . . . . . . . . . . 14 class ↑m
125	122, 123, 124	co 7420	. . . . . . . . . . . . 13 class ((𝑣 × 𝑣) ↑m (1...𝑛))
126	121, 90, 125	crab 3413	. . . . . . . . . . . 12 class {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))}
127		cxrs 17672	. . . . . . . . . . . . 13 class ℝ*𝑠
128	6, 83	cfv 6538	. . . . . . . . . . . . . 14 class (dist‘𝑟)
129	88	cv 1569	. . . . . . . . . . . . . 14 class 𝑔
130	128, 129	ccom 5655	. . . . . . . . . . . . 13 class ((dist‘𝑟) ∘ 𝑔)
131		cgsu 17611	. . . . . . . . . . . . 13 class Σg
132	127, 130, 131	co 7420	. . . . . . . . . . . 12 class (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))
133	88, 126, 132	cmpt 5186	. . . . . . . . . . 11 class (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
134	133	crn 5652	. . . . . . . . . 10 class ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
135	86, 87, 134	ciun 4951	. . . . . . . . 9 class ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
136		cxr 11342	. . . . . . . . 9 class ℝ*
137		clt 11343	. . . . . . . . 9 class <
138	135, 136, 137	cinf 9433	. . . . . . . 8 class inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )
139	49, 85, 12, 12, 138	cmpo 7422	. . . . . . 7 class (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))
140	84, 139	cop 4590	. . . . . 6 class ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩
141	75, 82, 140	ctp 4588	. . . . 5 class {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}
142	68, 141	cun 3897	. . . 4 class (({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})
143	5, 8, 142	csb 3847	. . 3 class ⦋(Base‘𝑟) / 𝑣⦌(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})
144	2, 3, 4, 4, 143	cmpo 7422	. 2 class (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
145	1, 144	wceq 1570	1 wff “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))

This definition is used by:  imasval  17683