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

Definition df-homlimb 33115
 Description: The input to this function is a sequence (on ℕ) of homomorphisms 𝐹(𝑛):𝑅(𝑛)⟶𝑅(𝑛 + 1). The resulting structure is the direct limit of the direct system so defined. This function returns the pair ⟨𝑆, 𝐺⟩ where 𝑆 is the terminal object and 𝐺 is a sequence of functions such that 𝐺(𝑛):𝑅(𝑛)⟶𝑆 and 𝐺(𝑛) = 𝐹(𝑛) ∘ 𝐺(𝑛 + 1). (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-homlimb HomLimB = (𝑓 ∈ V ↦ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛)) / 𝑣 {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
Distinct variable group:   𝑒,𝑓,𝑛,𝑠,𝑣,𝑥

Detailed syntax breakdown of Definition df-homlimb
StepHypRef Expression
1 chlb 33107 . 2 class HomLimB
2 vf . . 3 setvar 𝑓
3 cvv 3409 . . 3 class V
4 vv . . . 4 setvar 𝑣
5 vn . . . . 5 setvar 𝑛
6 cn 11674 . . . . 5 class
75cv 1537 . . . . . . 7 class 𝑛
87csn 4522 . . . . . 6 class {𝑛}
92cv 1537 . . . . . . . 8 class 𝑓
107, 9cfv 6335 . . . . . . 7 class (𝑓𝑛)
1110cdm 5524 . . . . . 6 class dom (𝑓𝑛)
128, 11cxp 5522 . . . . 5 class ({𝑛} × dom (𝑓𝑛))
135, 6, 12ciun 4883 . . . 4 class 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛))
14 ve . . . . 5 setvar 𝑒
154cv 1537 . . . . . . . . 9 class 𝑣
16 vs . . . . . . . . . 10 setvar 𝑠
1716cv 1537 . . . . . . . . 9 class 𝑠
1815, 17wer 8296 . . . . . . . 8 wff 𝑠 Er 𝑣
19 vx . . . . . . . . . 10 setvar 𝑥
2019cv 1537 . . . . . . . . . . . . 13 class 𝑥
21 c1st 7691 . . . . . . . . . . . . 13 class 1st
2220, 21cfv 6335 . . . . . . . . . . . 12 class (1st𝑥)
23 c1 10576 . . . . . . . . . . . 12 class 1
24 caddc 10578 . . . . . . . . . . . 12 class +
2522, 23, 24co 7150 . . . . . . . . . . 11 class ((1st𝑥) + 1)
26 c2nd 7692 . . . . . . . . . . . . 13 class 2nd
2720, 26cfv 6335 . . . . . . . . . . . 12 class (2nd𝑥)
2822, 9cfv 6335 . . . . . . . . . . . 12 class (𝑓‘(1st𝑥))
2927, 28cfv 6335 . . . . . . . . . . 11 class ((𝑓‘(1st𝑥))‘(2nd𝑥))
3025, 29cop 4528 . . . . . . . . . 10 class ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩
3119, 15, 30cmpt 5112 . . . . . . . . 9 class (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩)
3231, 17wss 3858 . . . . . . . 8 wff (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠
3318, 32wa 399 . . . . . . 7 wff (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)
3433, 16cab 2735 . . . . . 6 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)}
3534cint 4838 . . . . 5 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)}
3614cv 1537 . . . . . . 7 class 𝑒
3715, 36cqs 8298 . . . . . 6 class (𝑣 / 𝑒)
387, 20cop 4528 . . . . . . . . 9 class 𝑛, 𝑥
3938, 36cec 8297 . . . . . . . 8 class [⟨𝑛, 𝑥⟩]𝑒
4019, 11, 39cmpt 5112 . . . . . . 7 class (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒)
415, 6, 40cmpt 5112 . . . . . 6 class (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))
4237, 41cop 4528 . . . . 5 class ⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
4314, 35, 42csb 3805 . . . 4 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
444, 13, 43csb 3805 . . 3 class 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛)) / 𝑣 {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
452, 3, 44cmpt 5112 . 2 class (𝑓 ∈ V ↦ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛)) / 𝑣 {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
461, 45wceq 1538 1 wff HomLimB = (𝑓 ∈ V ↦ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛)) / 𝑣 {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator