Users' Mathboxes 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 32781
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 32773 . 2 class HomLimB
2 vf . . 3 setvar 𝑓
3 cvv 3492 . . 3 class V
4 vv . . . 4 setvar 𝑣
5 vn . . . . 5 setvar 𝑛
6 cn 11626 . . . . 5 class
75cv 1527 . . . . . . 7 class 𝑛
87csn 4557 . . . . . 6 class {𝑛}
92cv 1527 . . . . . . . 8 class 𝑓
107, 9cfv 6348 . . . . . . 7 class (𝑓𝑛)
1110cdm 5548 . . . . . 6 class dom (𝑓𝑛)
128, 11cxp 5546 . . . . 5 class ({𝑛} × dom (𝑓𝑛))
135, 6, 12ciun 4910 . . . 4 class 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛))
14 ve . . . . 5 setvar 𝑒
154cv 1527 . . . . . . . . 9 class 𝑣
16 vs . . . . . . . . . 10 setvar 𝑠
1716cv 1527 . . . . . . . . 9 class 𝑠
1815, 17wer 8275 . . . . . . . 8 wff 𝑠 Er 𝑣
19 vx . . . . . . . . . 10 setvar 𝑥
2019cv 1527 . . . . . . . . . . . . 13 class 𝑥
21 c1st 7676 . . . . . . . . . . . . 13 class 1st
2220, 21cfv 6348 . . . . . . . . . . . 12 class (1st𝑥)
23 c1 10526 . . . . . . . . . . . 12 class 1
24 caddc 10528 . . . . . . . . . . . 12 class +
2522, 23, 24co 7145 . . . . . . . . . . 11 class ((1st𝑥) + 1)
26 c2nd 7677 . . . . . . . . . . . . 13 class 2nd
2720, 26cfv 6348 . . . . . . . . . . . 12 class (2nd𝑥)
2822, 9cfv 6348 . . . . . . . . . . . 12 class (𝑓‘(1st𝑥))
2927, 28cfv 6348 . . . . . . . . . . 11 class ((𝑓‘(1st𝑥))‘(2nd𝑥))
3025, 29cop 4563 . . . . . . . . . 10 class ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩
3119, 15, 30cmpt 5137 . . . . . . . . 9 class (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩)
3231, 17wss 3933 . . . . . . . 8 wff (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠
3318, 32wa 396 . . . . . . 7 wff (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)
3433, 16cab 2796 . . . . . 6 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)}
3534cint 4867 . . . . 5 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)}
3614cv 1527 . . . . . . 7 class 𝑒
3715, 36cqs 8277 . . . . . 6 class (𝑣 / 𝑒)
387, 20cop 4563 . . . . . . . . 9 class 𝑛, 𝑥
3938, 36cec 8276 . . . . . . . 8 class [⟨𝑛, 𝑥⟩]𝑒
4019, 11, 39cmpt 5137 . . . . . . 7 class (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒)
415, 6, 40cmpt 5137 . . . . . 6 class (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))
4237, 41cop 4563 . . . . 5 class ⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
4314, 35, 42csb 3880 . . . 4 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
444, 13, 43csb 3880 . . 3 class 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛)) / 𝑣 {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
452, 3, 44cmpt 5137 . 2 class (𝑓 ∈ V ↦ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓𝑛)) / 𝑣 {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥𝑣 ↦ ⟨((1st𝑥) + 1), ((𝑓‘(1st𝑥))‘(2nd𝑥))⟩) ⊆ 𝑠)} / 𝑒⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
461, 45wceq 1528 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