MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-imas Structured version   Visualization version   GIF version

Definition df-imas 16215
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 5156, 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 5155) and/or 𝑅 ( with df-ress 15912) 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
Distinct variable group:   𝑓,𝑔,,𝑖,𝑛,𝑝,𝑞,𝑟,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 16211 . 2 class s
2 vf . . 3 setvar 𝑓
3 vr . . 3 setvar 𝑟
4 cvv 3231 . . 3 class V
5 vv . . . 4 setvar 𝑣
63cv 1522 . . . . 5 class 𝑟
7 cbs 15904 . . . . 5 class Base
86, 7cfv 5926 . . . 4 class (Base‘𝑟)
9 cnx 15901 . . . . . . . . 9 class ndx
109, 7cfv 5926 . . . . . . . 8 class (Base‘ndx)
112cv 1522 . . . . . . . . 9 class 𝑓
1211crn 5144 . . . . . . . 8 class ran 𝑓
1310, 12cop 4216 . . . . . . 7 class ⟨(Base‘ndx), ran 𝑓
14 cplusg 15988 . . . . . . . . 9 class +g
159, 14cfv 5926 . . . . . . . 8 class (+g‘ndx)
16 vp . . . . . . . . 9 setvar 𝑝
175cv 1522 . . . . . . . . 9 class 𝑣
18 vq . . . . . . . . . 10 setvar 𝑞
1916cv 1522 . . . . . . . . . . . . . 14 class 𝑝
2019, 11cfv 5926 . . . . . . . . . . . . 13 class (𝑓𝑝)
2118cv 1522 . . . . . . . . . . . . . 14 class 𝑞
2221, 11cfv 5926 . . . . . . . . . . . . 13 class (𝑓𝑞)
2320, 22cop 4216 . . . . . . . . . . . 12 class ⟨(𝑓𝑝), (𝑓𝑞)⟩
246, 14cfv 5926 . . . . . . . . . . . . . 14 class (+g𝑟)
2519, 21, 24co 6690 . . . . . . . . . . . . 13 class (𝑝(+g𝑟)𝑞)
2625, 11cfv 5926 . . . . . . . . . . . 12 class (𝑓‘(𝑝(+g𝑟)𝑞))
2723, 26cop 4216 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩
2827csn 4210 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
2918, 17, 28ciun 4552 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
3016, 17, 29ciun 4552 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
3115, 30cop 4216 . . . . . . 7 class ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩
32 cmulr 15989 . . . . . . . . 9 class .r
339, 32cfv 5926 . . . . . . . 8 class (.r‘ndx)
346, 32cfv 5926 . . . . . . . . . . . . . 14 class (.r𝑟)
3519, 21, 34co 6690 . . . . . . . . . . . . 13 class (𝑝(.r𝑟)𝑞)
3635, 11cfv 5926 . . . . . . . . . . . 12 class (𝑓‘(𝑝(.r𝑟)𝑞))
3723, 36cop 4216 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩
3837csn 4210 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
3918, 17, 38ciun 4552 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
4016, 17, 39ciun 4552 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
4133, 40cop 4216 . . . . . . 7 class ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩
4213, 31, 41ctp 4214 . . . . . 6 class {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩}
43 csca 15991 . . . . . . . . 9 class Scalar
449, 43cfv 5926 . . . . . . . 8 class (Scalar‘ndx)
456, 43cfv 5926 . . . . . . . 8 class (Scalar‘𝑟)
4644, 45cop 4216 . . . . . . 7 class ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩
47 cvsca 15992 . . . . . . . . 9 class ·𝑠
489, 47cfv 5926 . . . . . . . 8 class ( ·𝑠 ‘ndx)
49 vx . . . . . . . . . 10 setvar 𝑥
5045, 7cfv 5926 . . . . . . . . . 10 class (Base‘(Scalar‘𝑟))
5122csn 4210 . . . . . . . . . 10 class {(𝑓𝑞)}
526, 47cfv 5926 . . . . . . . . . . . 12 class ( ·𝑠𝑟)
5319, 21, 52co 6690 . . . . . . . . . . 11 class (𝑝( ·𝑠𝑟)𝑞)
5453, 11cfv 5926 . . . . . . . . . 10 class (𝑓‘(𝑝( ·𝑠𝑟)𝑞))
5516, 49, 50, 51, 54cmpt2 6692 . . . . . . . . 9 class (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))
5618, 17, 55ciun 4552 . . . . . . . 8 class 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))
5748, 56cop 4216 . . . . . . 7 class ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩
58 cip 15993 . . . . . . . . 9 class ·𝑖
599, 58cfv 5926 . . . . . . . 8 class (·𝑖‘ndx)
606, 58cfv 5926 . . . . . . . . . . . . 13 class (·𝑖𝑟)
6119, 21, 60co 6690 . . . . . . . . . . . 12 class (𝑝(·𝑖𝑟)𝑞)
6223, 61cop 4216 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩
6362csn 4210 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6418, 17, 63ciun 4552 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6516, 17, 64ciun 4552 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6659, 65cop 4216 . . . . . . 7 class ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩
6746, 57, 66ctp 4214 . . . . . 6 class {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}
6842, 67cun 3605 . . . . 5 class ({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩})
69 cts 15994 . . . . . . . 8 class TopSet
709, 69cfv 5926 . . . . . . 7 class (TopSet‘ndx)
71 ctopn 16129 . . . . . . . . 9 class TopOpen
726, 71cfv 5926 . . . . . . . 8 class (TopOpen‘𝑟)
73 cqtop 16210 . . . . . . . 8 class qTop
7472, 11, 73co 6690 . . . . . . 7 class ((TopOpen‘𝑟) qTop 𝑓)
7570, 74cop 4216 . . . . . 6 class ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩
76 cple 15995 . . . . . . . 8 class le
779, 76cfv 5926 . . . . . . 7 class (le‘ndx)
786, 76cfv 5926 . . . . . . . . 9 class (le‘𝑟)
7911, 78ccom 5147 . . . . . . . 8 class (𝑓 ∘ (le‘𝑟))
8011ccnv 5142 . . . . . . . 8 class 𝑓
8179, 80ccom 5147 . . . . . . 7 class ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)
8277, 81cop 4216 . . . . . 6 class ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩
83 cds 15997 . . . . . . . 8 class dist
849, 83cfv 5926 . . . . . . 7 class (dist‘ndx)
85 vy . . . . . . . 8 setvar 𝑦
86 vn . . . . . . . . . 10 setvar 𝑛
87 cn 11058 . . . . . . . . . 10 class
88 vg . . . . . . . . . . . 12 setvar 𝑔
89 c1 9975 . . . . . . . . . . . . . . . . . 18 class 1
90 vh . . . . . . . . . . . . . . . . . . 19 setvar
9190cv 1522 . . . . . . . . . . . . . . . . . 18 class
9289, 91cfv 5926 . . . . . . . . . . . . . . . . 17 class (‘1)
93 c1st 7208 . . . . . . . . . . . . . . . . 17 class 1st
9492, 93cfv 5926 . . . . . . . . . . . . . . . 16 class (1st ‘(‘1))
9594, 11cfv 5926 . . . . . . . . . . . . . . 15 class (𝑓‘(1st ‘(‘1)))
9649cv 1522 . . . . . . . . . . . . . . 15 class 𝑥
9795, 96wceq 1523 . . . . . . . . . . . . . 14 wff (𝑓‘(1st ‘(‘1))) = 𝑥
9886cv 1522 . . . . . . . . . . . . . . . . . 18 class 𝑛
9998, 91cfv 5926 . . . . . . . . . . . . . . . . 17 class (𝑛)
100 c2nd 7209 . . . . . . . . . . . . . . . . 17 class 2nd
10199, 100cfv 5926 . . . . . . . . . . . . . . . 16 class (2nd ‘(𝑛))
102101, 11cfv 5926 . . . . . . . . . . . . . . 15 class (𝑓‘(2nd ‘(𝑛)))
10385cv 1522 . . . . . . . . . . . . . . 15 class 𝑦
104102, 103wceq 1523 . . . . . . . . . . . . . 14 wff (𝑓‘(2nd ‘(𝑛))) = 𝑦
105 vi . . . . . . . . . . . . . . . . . . . 20 setvar 𝑖
106105cv 1522 . . . . . . . . . . . . . . . . . . 19 class 𝑖
107106, 91cfv 5926 . . . . . . . . . . . . . . . . . 18 class (𝑖)
108107, 100cfv 5926 . . . . . . . . . . . . . . . . 17 class (2nd ‘(𝑖))
109108, 11cfv 5926 . . . . . . . . . . . . . . . 16 class (𝑓‘(2nd ‘(𝑖)))
110 caddc 9977 . . . . . . . . . . . . . . . . . . . 20 class +
111106, 89, 110co 6690 . . . . . . . . . . . . . . . . . . 19 class (𝑖 + 1)
112111, 91cfv 5926 . . . . . . . . . . . . . . . . . 18 class (‘(𝑖 + 1))
113112, 93cfv 5926 . . . . . . . . . . . . . . . . 17 class (1st ‘(‘(𝑖 + 1)))
114113, 11cfv 5926 . . . . . . . . . . . . . . . 16 class (𝑓‘(1st ‘(‘(𝑖 + 1))))
115109, 114wceq 1523 . . . . . . . . . . . . . . 15 wff (𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))
116 cmin 10304 . . . . . . . . . . . . . . . . 17 class
11798, 89, 116co 6690 . . . . . . . . . . . . . . . 16 class (𝑛 − 1)
118 cfz 12364 . . . . . . . . . . . . . . . 16 class ...
11989, 117, 118co 6690 . . . . . . . . . . . . . . 15 class (1...(𝑛 − 1))
120115, 105, 119wral 2941 . . . . . . . . . . . . . 14 wff 𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))
12197, 104, 120w3a 1054 . . . . . . . . . . . . 13 wff ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))
12217, 17cxp 5141 . . . . . . . . . . . . . 14 class (𝑣 × 𝑣)
12389, 98, 118co 6690 . . . . . . . . . . . . . 14 class (1...𝑛)
124 cmap 7899 . . . . . . . . . . . . . 14 class 𝑚
125122, 123, 124co 6690 . . . . . . . . . . . . 13 class ((𝑣 × 𝑣) ↑𝑚 (1...𝑛))
126121, 90, 125crab 2945 . . . . . . . . . . . 12 class { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))}
127 cxrs 16207 . . . . . . . . . . . . 13 class *𝑠
1286, 83cfv 5926 . . . . . . . . . . . . . 14 class (dist‘𝑟)
12988cv 1522 . . . . . . . . . . . . . 14 class 𝑔
130128, 129ccom 5147 . . . . . . . . . . . . 13 class ((dist‘𝑟) ∘ 𝑔)
131 cgsu 16148 . . . . . . . . . . . . 13 class Σg
132127, 130, 131co 6690 . . . . . . . . . . . 12 class (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))
13388, 126, 132cmpt 4762 . . . . . . . . . . 11 class (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
134133crn 5144 . . . . . . . . . 10 class ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
13586, 87, 134ciun 4552 . . . . . . . . 9 class 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
136 cxr 10111 . . . . . . . . 9 class *
137 clt 10112 . . . . . . . . 9 class <
138135, 136, 137cinf 8388 . . . . . . . 8 class inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )
13949, 85, 12, 12, 138cmpt2 6692 . . . . . . 7 class (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))
14084, 139cop 4216 . . . . . 6 class ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩
14175, 82, 140ctp 4214 . . . . 5 class {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}
14268, 141cun 3605 . . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})
1435, 8, 142csb 3566 . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})
1442, 3, 4, 4, 143cmpt2 6692 . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
1451, 144wceq 1523 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
Colors of variables: wff setvar class
This definition is referenced by:  imasval  16218
  Copyright terms: Public domain W3C validator