Definition df-homlimb 30786

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

Step	Hyp	Ref	Expression
1		chlb 30778	. 2 class HomLimB
2		vf	. . 3 setvar 𝑓
3		cvv 3173	. . 3 class V
4		vv	. . . 4 setvar 𝑣
5		vn	. . . . 5 setvar 𝑛
6		cn 10897	. . . . 5 class ℕ
7	5	cv 1474	. . . . . . 7 class 𝑛
8	7	csn 4125	. . . . . 6 class {𝑛}
9	2	cv 1474	. . . . . . . 8 class 𝑓
10	7, 9	cfv 5804	. . . . . . 7 class (𝑓‘𝑛)
11	10	cdm 5038	. . . . . 6 class dom (𝑓‘𝑛)
12	8, 11	cxp 5036	. . . . 5 class ({𝑛} × dom (𝑓‘𝑛))
13	5, 6, 12	ciun 4455	. . . 4 class ∪ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓‘𝑛))
14		ve	. . . . 5 setvar 𝑒
15	4	cv 1474	. . . . . . . . 9 class 𝑣
16		vs	. . . . . . . . . 10 setvar 𝑠
17	16	cv 1474	. . . . . . . . 9 class 𝑠
18	15, 17	wer 7626	. . . . . . . 8 wff 𝑠 Er 𝑣
19		vx	. . . . . . . . . 10 setvar 𝑥
20	19	cv 1474	. . . . . . . . . . . . 13 class 𝑥
21		c1st 7057	. . . . . . . . . . . . 13 class 1st
22	20, 21	cfv 5804	. . . . . . . . . . . 12 class (1st ‘𝑥)
23		c1 9816	. . . . . . . . . . . 12 class 1
24		caddc 9818	. . . . . . . . . . . 12 class +
25	22, 23, 24	co 6549	. . . . . . . . . . 11 class ((1st ‘𝑥) + 1)
26		c2nd 7058	. . . . . . . . . . . . 13 class 2nd
27	20, 26	cfv 5804	. . . . . . . . . . . 12 class (2nd ‘𝑥)
28	22, 9	cfv 5804	. . . . . . . . . . . 12 class (𝑓‘(1st ‘𝑥))
29	27, 28	cfv 5804	. . . . . . . . . . 11 class ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))
30	25, 29	cop 4131	. . . . . . . . . 10 class ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩
31	19, 15, 30	cmpt 4643	. . . . . . . . 9 class (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩)
32	31, 17	wss 3540	. . . . . . . 8 wff (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠
33	18, 32	wa 383	. . . . . . 7 wff (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)
34	33, 16	cab 2596	. . . . . 6 class {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)}
35	34	cint 4410	. . . . 5 class ∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)}
36	14	cv 1474	. . . . . . 7 class 𝑒
37	15, 36	cqs 7628	. . . . . 6 class (𝑣 / 𝑒)
38	7, 20	cop 4131	. . . . . . . . 9 class ⟨𝑛, 𝑥⟩
39	38, 36	cec 7627	. . . . . . . 8 class [⟨𝑛, 𝑥⟩]𝑒
40	19, 11, 39	cmpt 4643	. . . . . . 7 class (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒)
41	5, 6, 40	cmpt 4643	. . . . . 6 class (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))
42	37, 41	cop 4131	. . . . 5 class ⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
43	14, 35, 42	csb 3499	. . . 4 class ⦋∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)} / 𝑒⦌⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
44	4, 13, 43	csb 3499	. . 3 class ⦋∪ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓‘𝑛)) / 𝑣⦌⦋∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)} / 𝑒⦌⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩
45	2, 3, 44	cmpt 4643	. 2 class (𝑓 ∈ V ↦ ⦋∪ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓‘𝑛)) / 𝑣⦌⦋∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)} / 𝑒⦌⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
46	1, 45	wceq 1475	1 wff HomLimB = (𝑓 ∈ V ↦ ⦋∪ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓‘𝑛)) / 𝑣⦌⦋∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)} / 𝑒⦌⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)

This definition is referenced by: (None)