Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-homlimb Unicode version

Definition df-homlimb 23968
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
StepHypRef Expression
1 chlb 23960 . 2  class HomLimB
2 vf . . 3  set  f
3 cvv 2788 . . 3  class  _V
4 vv . . . 4  set  v
5 vn . . . . 5  set  n
6 cn 9746 . . . . 5  class  NN
75cv 1622 . . . . . . 7  class  n
87csn 3640 . . . . . 6  class  { n }
92cv 1622 . . . . . . . 8  class  f
107, 9cfv 5255 . . . . . . 7  class  ( f `
 n )
1110cdm 4689 . . . . . 6  class  dom  (
f `  n )
128, 11cxp 4687 . . . . 5  class  ( { n }  X.  dom  ( f `  n
) )
135, 6, 12ciun 3905 . . . 4  class  U_ n  e.  NN  ( { n }  X.  dom  ( f `
 n ) )
14 ve . . . . 5  set  e
154cv 1622 . . . . . . . . 9  class  v
16 vs . . . . . . . . . 10  set  s
1716cv 1622 . . . . . . . . 9  class  s
1815, 17wer 6657 . . . . . . . 8  wff  s  Er  v
19 vx . . . . . . . . . 10  set  x
2019cv 1622 . . . . . . . . . . . . 13  class  x
21 c1st 6120 . . . . . . . . . . . . 13  class  1st
2220, 21cfv 5255 . . . . . . . . . . . 12  class  ( 1st `  x )
23 c1 8738 . . . . . . . . . . . 12  class  1
24 caddc 8740 . . . . . . . . . . . 12  class  +
2522, 23, 24co 5858 . . . . . . . . . . 11  class  ( ( 1st `  x )  +  1 )
26 c2nd 6121 . . . . . . . . . . . . 13  class  2nd
2720, 26cfv 5255 . . . . . . . . . . . 12  class  ( 2nd `  x )
2822, 9cfv 5255 . . . . . . . . . . . 12  class  ( f `
 ( 1st `  x
) )
2927, 28cfv 5255 . . . . . . . . . . 11  class  ( ( f `  ( 1st `  x ) ) `  ( 2nd `  x ) )
3025, 29cop 3643 . . . . . . . . . 10  class  <. (
( 1st `  x
)  +  1 ) ,  ( ( f `
 ( 1st `  x
) ) `  ( 2nd `  x ) )
>.
3119, 15, 30cmpt 4077 . . . . . . . . 9  class  ( x  e.  v  |->  <. (
( 1st `  x
)  +  1 ) ,  ( ( f `
 ( 1st `  x
) ) `  ( 2nd `  x ) )
>. )
3231, 17wss 3152 . . . . . . . 8  wff  ( x  e.  v  |->  <. (
( 1st `  x
)  +  1 ) ,  ( ( f `
 ( 1st `  x
) ) `  ( 2nd `  x ) )
>. )  C_  s
3318, 32wa 358 . . . . . . 7  wff  ( s  Er  v  /\  (
x  e.  v  |->  <.
( ( 1st `  x
)  +  1 ) ,  ( ( f `
 ( 1st `  x
) ) `  ( 2nd `  x ) )
>. )  C_  s )
3433, 16cab 2269 . . . . . 6  class  { s  |  ( s  Er  v  /\  ( x  e.  v  |->  <. (
( 1st `  x
)  +  1 ) ,  ( ( f `
 ( 1st `  x
) ) `  ( 2nd `  x ) )
>. )  C_  s ) }
3534cint 3862 . . . . 5  class  |^| { s  |  ( s  Er  v  /\  ( x  e.  v  |->  <. (
( 1st `  x
)  +  1 ) ,  ( ( f `
 ( 1st `  x
) ) `  ( 2nd `  x ) )
>. )  C_  s ) }
3614cv 1622 . . . . . . 7  class  e
3715, 36cqs 6659 . . . . . 6  class  ( v /. e )
387, 20cop 3643 . . . . . . . . 9  class  <. n ,  x >.
3938, 36cec 6658 . . . . . . . 8  class  [ <. n ,  x >. ] e
4019, 11, 39cmpt 4077 . . . . . . 7  class  ( x  e.  dom  ( f `
 n )  |->  [
<. n ,  x >. ] e )
415, 6, 40cmpt 4077 . . . . . 6  class  ( n  e.  NN  |->  ( x  e.  dom  ( f `
 n )  |->  [
<. n ,  x >. ] e ) )
4237, 41cop 3643 . . . . 5  class  <. (
v /. e ) ,  ( n  e.  NN  |->  ( x  e. 
dom  ( f `  n )  |->  [ <. n ,  x >. ] e ) ) >.
4314, 35, 42csb 3081 . . . 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 ) ) >.
444, 13, 43csb 3081 . . 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 ) ) >.
452, 3, 44cmpt 4077 . 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 ) ) >.
)
461, 45wceq 1623 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 ) ) >.
)
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator