Definition df-homlimb 31532

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.)

Assertion

Ref	Expression
df-homlimb	|- HomLimB = ( f e. _V |-> [_ U_ n e. NN ( { n } X. dom ( f ` n ) ) / v ]_ [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >. )

Distinct variable group:   e, f, n, s, v, x

Detailed syntax breakdown of Definition df-homlimb

Step	Hyp	Ref	Expression
1		chlb 31524	. 2 class HomLimB
2		vf	. . 3 setvar f
3		cvv 3200	. . 3 class _V
4		vv	. . . 4 setvar v
5		vn	. . . . 5 setvar n
6		cn 11020	. . . . 5 class NN
7	5	cv 1482	. . . . . . 7 class n
8	7	csn 4177	. . . . . 6 class { n }
9	2	cv 1482	. . . . . . . 8 class f
10	7, 9	cfv 5888	. . . . . . 7 class ( f ` n )
11	10	cdm 5114	. . . . . 6 class dom ( f ` n )
12	8, 11	cxp 5112	. . . . 5 class ( { n } X. dom ( f ` n ) )
13	5, 6, 12	ciun 4520	. . . 4 class U_ n e. NN ( { n } X. dom ( f ` n ) )
14		ve	. . . . 5 setvar e
15	4	cv 1482	. . . . . . . . 9 class v
16		vs	. . . . . . . . . 10 setvar s
17	16	cv 1482	. . . . . . . . 9 class s
18	15, 17	wer 7739	. . . . . . . 8 wff s Er v
19		vx	. . . . . . . . . 10 setvar x
20	19	cv 1482	. . . . . . . . . . . . 13 class x
21		c1st 7166	. . . . . . . . . . . . 13 class 1st
22	20, 21	cfv 5888	. . . . . . . . . . . 12 class ( 1st ` x )
23		c1 9937	. . . . . . . . . . . 12 class 1
24		caddc 9939	. . . . . . . . . . . 12 class +
25	22, 23, 24	co 6650	. . . . . . . . . . 11 class ( ( 1st ` x ) + 1 )
26		c2nd 7167	. . . . . . . . . . . . 13 class 2nd
27	20, 26	cfv 5888	. . . . . . . . . . . 12 class ( 2nd ` x )
28	22, 9	cfv 5888	. . . . . . . . . . . 12 class ( f ` ( 1st ` x ) )
29	27, 28	cfv 5888	. . . . . . . . . . 11 class ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) )
30	25, 29	cop 4183	. . . . . . . . . 10 class <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >.
31	19, 15, 30	cmpt 4729	. . . . . . . . 9 class ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. )
32	31, 17	wss 3574	. . . . . . . 8 wff ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s
33	18, 32	wa 384	. . . . . . 7 wff ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s )
34	33, 16	cab 2608	. . . . . 6 class { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) }
35	34	cint 4475	. . . . 5 class |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) }
36	14	cv 1482	. . . . . . 7 class e
37	15, 36	cqs 7741	. . . . . 6 class ( v /. e )
38	7, 20	cop 4183	. . . . . . . . 9 class <. n , x >.
39	38, 36	cec 7740	. . . . . . . 8 class [ <. n , x >. ] e
40	19, 11, 39	cmpt 4729	. . . . . . 7 class ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e )
41	5, 6, 40	cmpt 4729	. . . . . 6 class ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) )
42	37, 41	cop 4183	. . . . 5 class <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >.
43	14, 35, 42	csb 3533	. . . 4 class [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >.
44	4, 13, 43	csb 3533	. . 3 class [_ U_ n e. NN ( { n } X. dom ( f ` n ) ) / v ]_ [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >.
45	2, 3, 44	cmpt 4729	. 2 class ( f e. _V |-> [_ U_ n e. NN ( { n } X. dom ( f ` n ) ) / v ]_ [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >. )
46	1, 45	wceq 1483	1 wff HomLimB = ( f e. _V |-> [_ U_ n e. NN ( { n } X. dom ( f ` n ) ) / v ]_ [_ |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) } / e ]_ <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >. )

This definition is referenced by: (None)