Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-homlim Structured version   Visualization version   GIF version

Definition df-homlim 33163
Description: The input to this function is a sequence (on ) of structures 𝑅(𝑛) and homomorphisms 𝐹(𝑛):𝑅(𝑛)⟶𝑅(𝑛 + 1). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-homlim HomLim = (𝑟 ∈ V, 𝑓 ∈ V ↦ ( HomLimB ‘𝑓) / 𝑒(1st𝑒) / 𝑣(2nd𝑒) / 𝑔({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩}))
Distinct variable group:   𝑒,𝑓,𝑔,𝑛,𝑟,𝑠,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-homlim
StepHypRef Expression
1 chlim 33155 . 2 class HomLim
2 vr . . 3 setvar 𝑟
3 vf . . 3 setvar 𝑓
4 cvv 3397 . . 3 class V
5 ve . . . 4 setvar 𝑒
63cv 1541 . . . . 5 class 𝑓
7 chlb 33154 . . . . 5 class HomLimB
86, 7cfv 6333 . . . 4 class ( HomLimB ‘𝑓)
9 vv . . . . 5 setvar 𝑣
105cv 1541 . . . . . 6 class 𝑒
11 c1st 7705 . . . . . 6 class 1st
1210, 11cfv 6333 . . . . 5 class (1st𝑒)
13 vg . . . . . 6 setvar 𝑔
14 c2nd 7706 . . . . . . 7 class 2nd
1510, 14cfv 6333 . . . . . 6 class (2nd𝑒)
16 cnx 16576 . . . . . . . . . 10 class ndx
17 cbs 16579 . . . . . . . . . 10 class Base
1816, 17cfv 6333 . . . . . . . . 9 class (Base‘ndx)
199cv 1541 . . . . . . . . 9 class 𝑣
2018, 19cop 4519 . . . . . . . 8 class ⟨(Base‘ndx), 𝑣
21 cplusg 16661 . . . . . . . . . 10 class +g
2216, 21cfv 6333 . . . . . . . . 9 class (+g‘ndx)
23 vn . . . . . . . . . 10 setvar 𝑛
24 cn 11709 . . . . . . . . . 10 class
25 vx . . . . . . . . . . . 12 setvar 𝑥
26 vy . . . . . . . . . . . 12 setvar 𝑦
2723cv 1541 . . . . . . . . . . . . . 14 class 𝑛
2813cv 1541 . . . . . . . . . . . . . 14 class 𝑔
2927, 28cfv 6333 . . . . . . . . . . . . 13 class (𝑔𝑛)
3029cdm 5519 . . . . . . . . . . . 12 class dom (𝑔𝑛)
3125cv 1541 . . . . . . . . . . . . . . 15 class 𝑥
3231, 29cfv 6333 . . . . . . . . . . . . . 14 class ((𝑔𝑛)‘𝑥)
3326cv 1541 . . . . . . . . . . . . . . 15 class 𝑦
3433, 29cfv 6333 . . . . . . . . . . . . . 14 class ((𝑔𝑛)‘𝑦)
3532, 34cop 4519 . . . . . . . . . . . . 13 class ⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩
362cv 1541 . . . . . . . . . . . . . . . . 17 class 𝑟
3727, 36cfv 6333 . . . . . . . . . . . . . . . 16 class (𝑟𝑛)
3837, 21cfv 6333 . . . . . . . . . . . . . . 15 class (+g‘(𝑟𝑛))
3931, 33, 38co 7164 . . . . . . . . . . . . . 14 class (𝑥(+g‘(𝑟𝑛))𝑦)
4039, 29cfv 6333 . . . . . . . . . . . . 13 class ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))
4135, 40cop 4519 . . . . . . . . . . . 12 class ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩
4225, 26, 30, 30, 41cmpo 7166 . . . . . . . . . . 11 class (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)
4342crn 5520 . . . . . . . . . 10 class ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)
4423, 24, 43ciun 4878 . . . . . . . . 9 class 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)
4522, 44cop 4519 . . . . . . . 8 class ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩
46 cmulr 16662 . . . . . . . . . 10 class .r
4716, 46cfv 6333 . . . . . . . . 9 class (.r‘ndx)
4837, 46cfv 6333 . . . . . . . . . . . . . . 15 class (.r‘(𝑟𝑛))
4931, 33, 48co 7164 . . . . . . . . . . . . . 14 class (𝑥(.r‘(𝑟𝑛))𝑦)
5049, 29cfv 6333 . . . . . . . . . . . . 13 class ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))
5135, 50cop 4519 . . . . . . . . . . . 12 class ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩
5225, 26, 30, 30, 51cmpo 7166 . . . . . . . . . . 11 class (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)
5352crn 5520 . . . . . . . . . 10 class ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)
5423, 24, 53ciun 4878 . . . . . . . . 9 class 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)
5547, 54cop 4519 . . . . . . . 8 class ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩
5620, 45, 55ctp 4517 . . . . . . 7 class {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩}
57 ctopn 16791 . . . . . . . . . 10 class TopOpen
5816, 57cfv 6333 . . . . . . . . 9 class (TopOpen‘ndx)
5929ccnv 5518 . . . . . . . . . . . . 13 class (𝑔𝑛)
60 vs . . . . . . . . . . . . . 14 setvar 𝑠
6160cv 1541 . . . . . . . . . . . . 13 class 𝑠
6259, 61cima 5522 . . . . . . . . . . . 12 class ((𝑔𝑛) “ 𝑠)
6337, 57cfv 6333 . . . . . . . . . . . 12 class (TopOpen‘(𝑟𝑛))
6462, 63wcel 2113 . . . . . . . . . . 11 wff ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))
6564, 23, 24wral 3053 . . . . . . . . . 10 wff 𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))
6619cpw 4485 . . . . . . . . . 10 class 𝒫 𝑣
6765, 60, 66crab 3057 . . . . . . . . 9 class {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}
6858, 67cop 4519 . . . . . . . 8 class ⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩
69 cds 16670 . . . . . . . . . 10 class dist
7016, 69cfv 6333 . . . . . . . . 9 class (dist‘ndx)
7127, 29cfv 6333 . . . . . . . . . . . . 13 class ((𝑔𝑛)‘𝑛)
7271cdm 5519 . . . . . . . . . . . 12 class dom ((𝑔𝑛)‘𝑛)
7337, 69cfv 6333 . . . . . . . . . . . . . 14 class (dist‘(𝑟𝑛))
7431, 33, 73co 7164 . . . . . . . . . . . . 13 class (𝑥(dist‘(𝑟𝑛))𝑦)
7535, 74cop 4519 . . . . . . . . . . . 12 class ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩
7625, 26, 72, 72, 75cmpo 7166 . . . . . . . . . . 11 class (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)
7776crn 5520 . . . . . . . . . 10 class ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)
7823, 24, 77ciun 4878 . . . . . . . . 9 class 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)
7970, 78cop 4519 . . . . . . . 8 class ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩
80 cple 16668 . . . . . . . . . 10 class le
8116, 80cfv 6333 . . . . . . . . 9 class (le‘ndx)
8237, 80cfv 6333 . . . . . . . . . . . 12 class (le‘(𝑟𝑛))
8382, 29ccom 5523 . . . . . . . . . . 11 class ((le‘(𝑟𝑛)) ∘ (𝑔𝑛))
8459, 83ccom 5523 . . . . . . . . . 10 class ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))
8523, 24, 84ciun 4878 . . . . . . . . 9 class 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))
8681, 85cop 4519 . . . . . . . 8 class ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩
8768, 79, 86ctp 4517 . . . . . . 7 class {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩}
8856, 87cun 3839 . . . . . 6 class ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩})
8913, 15, 88csb 3788 . . . . 5 class (2nd𝑒) / 𝑔({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩})
909, 12, 89csb 3788 . . . 4 class (1st𝑒) / 𝑣(2nd𝑒) / 𝑔({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩})
915, 8, 90csb 3788 . . 3 class ( HomLimB ‘𝑓) / 𝑒(1st𝑒) / 𝑣(2nd𝑒) / 𝑔({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩})
922, 3, 4, 4, 91cmpo 7166 . 2 class (𝑟 ∈ V, 𝑓 ∈ V ↦ ( HomLimB ‘𝑓) / 𝑒(1st𝑒) / 𝑣(2nd𝑒) / 𝑔({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩}))
931, 92wceq 1542 1 wff HomLim = (𝑟 ∈ V, 𝑓 ∈ V ↦ ( HomLimB ‘𝑓) / 𝑒(1st𝑒) / 𝑣(2nd𝑒) / 𝑔({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(+g‘(𝑟𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔𝑛), 𝑦 ∈ dom (𝑔𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, ((𝑔𝑛)‘(𝑥(.r‘(𝑟𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ ((𝑔𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟𝑛))}⟩, ⟨(dist‘ndx), 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔𝑛)‘𝑛) ↦ ⟨⟨((𝑔𝑛)‘𝑥), ((𝑔𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), 𝑛 ∈ ℕ ((𝑔𝑛) ∘ ((le‘(𝑟𝑛)) ∘ (𝑔𝑛)))⟩}))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator