Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlb 
 |-  HomLimB
1 vf 
 |-  f
2 cvv 
 |-  _V
3 vn 
 |-  n
4 cn 
 |-  NN
5 3 cv 
 |-  n
6 5 csn 
 |-  { n }
7 1 cv 
 |-  f
8 5 7 cfv 
 |-  ( f ` n )
9 8 cdm 
 |-  dom ( f ` n )
10 6 9 cxp 
 |-  ( { n } X. dom ( f ` n ) )
11 3 4 10 ciun 
 |-  U_ n e. NN ( { n } X. dom ( f ` n ) )
12 vv 
 |-  v
13 vs 
 |-  s
14 13 cv 
 |-  s
15 12 cv 
 |-  v
16 15 14 wer 
 |-  s Er v
17 vx 
 |-  x
18 c1st 
 |-  1st
19 17 cv 
 |-  x
20 19 18 cfv 
 |-  ( 1st ` x )
21 caddc 
 |-  +
22 c1 
 |-  1
23 20 22 21 co 
 |-  ( ( 1st ` x ) + 1 )
24 20 7 cfv 
 |-  ( f ` ( 1st ` x ) )
25 c2nd 
 |-  2nd
26 19 25 cfv 
 |-  ( 2nd ` x )
27 26 24 cfv 
 |-  ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) )
28 23 27 cop 
 |-  <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >.
29 17 15 28 cmpt 
 |-  ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. )
30 29 14 wss 
 |-  ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s
31 16 30 wa 
 |-  ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s )
32 31 13 cab 
 |-  { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) }
33 32 cint 
 |-  |^| { s | ( s Er v /\ ( x e. v |-> <. ( ( 1st ` x ) + 1 ) , ( ( f ` ( 1st ` x ) ) ` ( 2nd ` x ) ) >. ) C_ s ) }
34 ve 
 |-  e
35 34 cv 
 |-  e
36 15 35 cqs 
 |-  ( v /. e )
37 5 19 cop 
 |-  <. n , x >.
38 37 35 cec 
 |-  [ <. n , x >. ] e
39 17 9 38 cmpt 
 |-  ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e )
40 3 4 39 cmpt 
 |-  ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) )
41 36 40 cop 
 |-  <. ( v /. e ) , ( n e. NN |-> ( x e. dom ( f ` n ) |-> [ <. n , x >. ] e ) ) >.
42 34 33 41 csb 
 |-  [_ |^| { 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 ) ) >.
43 12 11 42 csb 
 |-  [_ 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 ) ) >.
44 1 2 43 cmpt 
 |-  ( 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 ) ) >. )
45 0 44 wceq 
 |-  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 ) ) >. )