Definition df-homlimb

Description: The input to this function is a sequence (on NN ) of homomorphisms F ( n ) : R ( n ) --> R ( n + 1 ) . The resulting structure is the direct limit of the direct system so defined. This function returns the pair <. S , G >. where S is the terminal object and G is a sequence of functions such that G ( n ) : R ( n ) --> S and G ( n ) = F ( n ) o. G ( n + 1 ) . (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-homlimb	⊢ HomLimB = ( 𝑓 ∈ V ↦ ⦋ ∪ 𝑛 ∈ ℕ ( { 𝑛 } × dom ( 𝑓 ‘ 𝑛 ) ) / 𝑣 ⦌ ⦋ ∩ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) } / 𝑒 ⦌ ⟨ ( 𝑣 / 𝑒 ) , ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlb	⊢ HomLimB
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cn	⊢ ℕ
5	3	cv	⊢ 𝑛
6	5	csn	⊢ { 𝑛 }
7	1	cv	⊢ 𝑓
8	5 7	cfv	⊢ ( 𝑓 ‘ 𝑛 )
9	8	cdm	⊢ dom ( 𝑓 ‘ 𝑛 )
10	6 9	cxp	⊢ ( { 𝑛 } × dom ( 𝑓 ‘ 𝑛 ) )
11	3 4 10	ciun	⊢ ∪ 𝑛 ∈ ℕ ( { 𝑛 } × dom ( 𝑓 ‘ 𝑛 ) )
12		vv	⊢ 𝑣
13		vs	⊢ 𝑠
14	13	cv	⊢ 𝑠
15	12	cv	⊢ 𝑣
16	15 14	wer	⊢ 𝑠 Er 𝑣
17		vx	⊢ 𝑥
18		c1st	⊢ 1st
19	17	cv	⊢ 𝑥
20	19 18	cfv	⊢ ( 1st ‘ 𝑥 )
21		caddc	⊢ +
22		c1	⊢ 1
23	20 22 21	co	⊢ ( ( 1st ‘ 𝑥 ) + 1 )
24	20 7	cfv	⊢ ( 𝑓 ‘ ( 1st ‘ 𝑥 ) )
25		c2nd	⊢ 2nd
26	19 25	cfv	⊢ ( 2nd ‘ 𝑥 )
27	26 24	cfv	⊢ ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) )
28	23 27	cop	⊢ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩
29	17 15 28	cmpt	⊢ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ )
30	29 14	wss	⊢ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠
31	16 30	wa	⊢ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 )
32	31 13	cab	⊢ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) }
33	32	cint	⊢ ∩ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) }
34		ve	⊢ 𝑒
35	34	cv	⊢ 𝑒
36	15 35	cqs	⊢ ( 𝑣 / 𝑒 )
37	5 19	cop	⊢ ⟨ 𝑛 , 𝑥 ⟩
38	37 35	cec	⊢ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒
39	17 9 38	cmpt	⊢ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 )
40	3 4 39	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) )
41	36 40	cop	⊢ ⟨ ( 𝑣 / 𝑒 ) , ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) ) ⟩
42	34 33 41	csb	⊢ ⦋ ∩ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) } / 𝑒 ⦌ ⟨ ( 𝑣 / 𝑒 ) , ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) ) ⟩
43	12 11 42	csb	⊢ ⦋ ∪ 𝑛 ∈ ℕ ( { 𝑛 } × dom ( 𝑓 ‘ 𝑛 ) ) / 𝑣 ⦌ ⦋ ∩ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) } / 𝑒 ⦌ ⟨ ( 𝑣 / 𝑒 ) , ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) ) ⟩
44	1 2 43	cmpt	⊢ ( 𝑓 ∈ V ↦ ⦋ ∪ 𝑛 ∈ ℕ ( { 𝑛 } × dom ( 𝑓 ‘ 𝑛 ) ) / 𝑣 ⦌ ⦋ ∩ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) } / 𝑒 ⦌ ⟨ ( 𝑣 / 𝑒 ) , ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) ) ⟩ )
45	0 44	wceq	⊢ HomLimB = ( 𝑓 ∈ V ↦ ⦋ ∪ 𝑛 ∈ ℕ ( { 𝑛 } × dom ( 𝑓 ‘ 𝑛 ) ) / 𝑣 ⦌ ⦋ ∩ { 𝑠 ∣ ( 𝑠 Er 𝑣 ∧ ( 𝑥 ∈ 𝑣 ↦ ⟨ ( ( 1st ‘ 𝑥 ) + 1 ) , ( ( 𝑓 ‘ ( 1st ‘ 𝑥 ) ) ‘ ( 2nd ‘ 𝑥 ) ) ⟩ ) ⊆ 𝑠 ) } / 𝑒 ⦌ ⟨ ( 𝑣 / 𝑒 ) , ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ dom ( 𝑓 ‘ 𝑛 ) ↦ [ ⟨ 𝑛 , 𝑥 ⟩ ] 𝑒 ) ) ⟩ )