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 V n n × dom f n / v s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s / e v / e n x dom f n n x e

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlb class HomLimB
1 vf setvar f
2 cvv class V
3 vn setvar n
4 cn class
5 3 cv setvar n
6 5 csn class n
7 1 cv setvar f
8 5 7 cfv class f n
9 8 cdm class dom f n
10 6 9 cxp class n × dom f n
11 3 4 10 ciun class n n × dom f n
12 vv setvar v
13 vs setvar s
14 13 cv setvar s
15 12 cv setvar v
16 15 14 wer wff s Er v
17 vx setvar x
18 c1st class 1 st
19 17 cv setvar x
20 19 18 cfv class 1 st x
21 caddc class +
22 c1 class 1
23 20 22 21 co class 1 st x + 1
24 20 7 cfv class f 1 st x
25 c2nd class 2 nd
26 19 25 cfv class 2 nd x
27 26 24 cfv class f 1 st x 2 nd x
28 23 27 cop class 1 st x + 1 f 1 st x 2 nd x
29 17 15 28 cmpt class x v 1 st x + 1 f 1 st x 2 nd x
30 29 14 wss wff x v 1 st x + 1 f 1 st x 2 nd x s
31 16 30 wa wff s Er v x v 1 st x + 1 f 1 st x 2 nd x s
32 31 13 cab class s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s
33 32 cint class s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s
34 ve setvar e
35 34 cv setvar e
36 15 35 cqs class v / e
37 5 19 cop class n x
38 37 35 cec class n x e
39 17 9 38 cmpt class x dom f n n x e
40 3 4 39 cmpt class n x dom f n n x e
41 36 40 cop class v / e n x dom f n n x e
42 34 33 41 csb class s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s / e v / e n x dom f n n x e
43 12 11 42 csb class n n × dom f n / v s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s / e v / e n x dom f n n x e
44 1 2 43 cmpt class f V n n × dom f n / v s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s / e v / e n x dom f n n x e
45 0 44 wceq wff HomLimB = f V n n × dom f n / v s | s Er v x v 1 st x + 1 f 1 st x 2 nd x s / e v / e n x dom f n n x e