Definition df-homlim 31533

Description: The input to this function is a sequence (on NN) of structures R ( n ) and homomorphisms F ( n ) : R ( n ) --> R ( n + 1 ). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref

Expression

df-homlim

|- HomLim = ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )

Distinct variable group:   e, f, g, n, r, s, v, x, y

Detailed syntax breakdown of Definition df-homlim

Step	Hyp	Ref	Expression
1		chlim 31525	. 2 class HomLim
2		vr	. . 3 setvar r
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5		ve	. . . 4 setvar e
6	3	cv 1482	. . . . 5 class f
7		chlb 31524	. . . . 5 class HomLimB
8	6, 7	cfv 5888	. . . 4 class ( HomLimB ` f )
9		vv	. . . . 5 setvar v
10	5	cv 1482	. . . . . 6 class e
11		c1st 7166	. . . . . 6 class 1st
12	10, 11	cfv 5888	. . . . 5 class ( 1st ` e )
13		vg	. . . . . 6 setvar g
14		c2nd 7167	. . . . . . 7 class 2nd
15	10, 14	cfv 5888	. . . . . 6 class ( 2nd ` e )
16		cnx 15854	. . . . . . . . . 10 class ndx
17		cbs 15857	. . . . . . . . . 10 class Base
18	16, 17	cfv 5888	. . . . . . . . 9 class ( Base ` ndx )
19	9	cv 1482	. . . . . . . . 9 class v
20	18, 19	cop 4183	. . . . . . . 8 class <. ( Base ` ndx ) , v >.
21		cplusg 15941	. . . . . . . . . 10 class +g
22	16, 21	cfv 5888	. . . . . . . . 9 class ( +g ` ndx )
23		vn	. . . . . . . . . 10 setvar n
24		cn 11020	. . . . . . . . . 10 class NN
25		vx	. . . . . . . . . . . 12 setvar x
26		vy	. . . . . . . . . . . 12 setvar y
27	23	cv 1482	. . . . . . . . . . . . . 14 class n
28	13	cv 1482	. . . . . . . . . . . . . 14 class g
29	27, 28	cfv 5888	. . . . . . . . . . . . 13 class ( g ` n )
30	29	cdm 5114	. . . . . . . . . . . 12 class dom ( g ` n )
31	25	cv 1482	. . . . . . . . . . . . . . 15 class x
32	31, 29	cfv 5888	. . . . . . . . . . . . . 14 class ( ( g ` n ) ` x )
33	26	cv 1482	. . . . . . . . . . . . . . 15 class y
34	33, 29	cfv 5888	. . . . . . . . . . . . . 14 class ( ( g ` n ) ` y )
35	32, 34	cop 4183	. . . . . . . . . . . . 13 class <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >.
36	2	cv 1482	. . . . . . . . . . . . . . . . 17 class r
37	27, 36	cfv 5888	. . . . . . . . . . . . . . . 16 class ( r ` n )
38	37, 21	cfv 5888	. . . . . . . . . . . . . . 15 class ( +g ` ( r ` n ) )
39	31, 33, 38	co 6650	. . . . . . . . . . . . . 14 class ( x ( +g ` ( r ` n ) ) y )
40	39, 29	cfv 5888	. . . . . . . . . . . . 13 class ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) )
41	35, 40	cop 4183	. . . . . . . . . . . 12 class <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >.
42	25, 26, 30, 30, 41	cmpt2 6652	. . . . . . . . . . 11 class ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. )
43	42	crn 5115	. . . . . . . . . 10 class ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. )
44	23, 24, 43	ciun 4520	. . . . . . . . 9 class U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. )
45	22, 44	cop 4183	. . . . . . . 8 class <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >.
46		cmulr 15942	. . . . . . . . . 10 class .r
47	16, 46	cfv 5888	. . . . . . . . 9 class ( .r ` ndx )
48	37, 46	cfv 5888	. . . . . . . . . . . . . . 15 class ( .r ` ( r ` n ) )
49	31, 33, 48	co 6650	. . . . . . . . . . . . . 14 class ( x ( .r ` ( r ` n ) ) y )
50	49, 29	cfv 5888	. . . . . . . . . . . . 13 class ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) )
51	35, 50	cop 4183	. . . . . . . . . . . 12 class <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >.
52	25, 26, 30, 30, 51	cmpt2 6652	. . . . . . . . . . 11 class ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. )
53	52	crn 5115	. . . . . . . . . 10 class ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. )
54	23, 24, 53	ciun 4520	. . . . . . . . 9 class U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. )
55	47, 54	cop 4183	. . . . . . . 8 class <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >.
56	20, 45, 55	ctp 4181	. . . . . . 7 class { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. }
57		ctopn 16082	. . . . . . . . . 10 class TopOpen
58	16, 57	cfv 5888	. . . . . . . . 9 class ( TopOpen ` ndx )
59	29	ccnv 5113	. . . . . . . . . . . . 13 class `' ( g ` n )
60		vs	. . . . . . . . . . . . . 14 setvar s
61	60	cv 1482	. . . . . . . . . . . . 13 class s
62	59, 61	cima 5117	. . . . . . . . . . . 12 class ( `' ( g ` n ) " s )
63	37, 57	cfv 5888	. . . . . . . . . . . 12 class ( TopOpen ` ( r ` n ) )
64	62, 63	wcel 1990	. . . . . . . . . . 11 wff ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) )
65	64, 23, 24	wral 2912	. . . . . . . . . 10 wff A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) )
66	19	cpw 4158	. . . . . . . . . 10 class ~P v
67	65, 60, 66	crab 2916	. . . . . . . . 9 class { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) }
68	58, 67	cop 4183	. . . . . . . 8 class <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >.
69		cds 15950	. . . . . . . . . 10 class dist
70	16, 69	cfv 5888	. . . . . . . . 9 class ( dist ` ndx )
71	27, 29	cfv 5888	. . . . . . . . . . . . 13 class ( ( g ` n ) ` n )
72	71	cdm 5114	. . . . . . . . . . . 12 class dom ( ( g ` n ) ` n )
73	37, 69	cfv 5888	. . . . . . . . . . . . . 14 class ( dist ` ( r ` n ) )
74	31, 33, 73	co 6650	. . . . . . . . . . . . 13 class ( x ( dist ` ( r ` n ) ) y )
75	35, 74	cop 4183	. . . . . . . . . . . 12 class <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >.
76	25, 26, 72, 72, 75	cmpt2 6652	. . . . . . . . . . 11 class ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. )
77	76	crn 5115	. . . . . . . . . 10 class ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. )
78	23, 24, 77	ciun 4520	. . . . . . . . 9 class U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. )
79	70, 78	cop 4183	. . . . . . . 8 class <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >.
80		cple 15948	. . . . . . . . . 10 class le
81	16, 80	cfv 5888	. . . . . . . . 9 class ( le ` ndx )
82	37, 80	cfv 5888	. . . . . . . . . . . 12 class ( le ` ( r ` n ) )
83	82, 29	ccom 5118	. . . . . . . . . . 11 class ( ( le ` ( r ` n ) ) o. ( g ` n ) )
84	59, 83	ccom 5118	. . . . . . . . . 10 class ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) )
85	23, 24, 84	ciun 4520	. . . . . . . . 9 class U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) )
86	81, 85	cop 4183	. . . . . . . 8 class <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >.
87	68, 79, 86	ctp 4181	. . . . . . 7 class { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. }
88	56, 87	cun 3572	. . . . . 6 class ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
89	13, 15, 88	csb 3533	. . . . 5 class [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
90	9, 12, 89	csb 3533	. . . 4 class [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
91	5, 8, 90	csb 3533	. . 3 class [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
92	2, 3, 4, 4, 91	cmpt2 6652	. 2 class ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )
93	1, 92	wceq 1483	1 wff HomLim = ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )

This definition is referenced by: (None)