df-homlim

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)

		Ref	Expression
	Assertion	df-homlim	$⊢ HomLim = (r \in V, f \in V ⟼ ⦋ HomLimB (f) / e ⦌ ⦋ 1^{st} (e) / v ⦌ ⦋ 2^{nd} (e) / g ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlim	$class HomLim$
1		vr	$setvar r$
2		cvv	$class V$
3		vf	$setvar f$
4		chlb	$class HomLimB$
5	3	cv	$setvar f$
6	5 4	cfv	$class HomLimB (f)$
7		ve	$setvar e$
8		c1st	$class 1^{st}$
9	7	cv	$setvar e$
10	9 8	cfv	$class 1^{st} (e)$
11		vv	$setvar v$
12		c2nd	$class 2^{nd}$
13	9 12	cfv	$class 2^{nd} (e)$
14		vg	$setvar g$
15		cbs	$class Base$
16		cnx	$class ndx$
17	16 15	cfv	$class {Base}_{ndx}$
18	11	cv	$setvar v$
19	17 18	cop	$class ⟨{Base}_{ndx}, v⟩$
20		cplusg	$class +_{𝑔}$
21	16 20	cfv	$class +_{ndx}$
22		vn	$setvar n$
23		cn	$class ℕ$
24		vx	$setvar x$
25	14	cv	$setvar g$
26	22	cv	$setvar n$
27	26 25	cfv	$class g (n)$
28	27	cdm	$class dom g (n)$
29		vy	$setvar y$
30	24	cv	$setvar x$
31	30 27	cfv	$class g (n) (x)$
32	29	cv	$setvar y$
33	32 27	cfv	$class g (n) (y)$
34	31 33	cop	$class ⟨g (n) (x), g (n) (y)⟩$
35	1	cv	$setvar r$
36	26 35	cfv	$class r (n)$
37	36 20	cfv	$class +_{r (n)}$
38	30 32 37	co	$class (x +_{r (n)} y)$
39	38 27	cfv	$class g (n) (x +_{r (n)} y)$
40	34 39	cop	$class ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩$
41	24 29 28 28 40	cmpo	$class (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)$
42	41	crn	$class ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)$
43	22 23 42	ciun	$class ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)$
44	21 43	cop	$class ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩$
45		cmulr	$class \cdot_{𝑟}$
46	16 45	cfv	$class \cdot_{ndx}$
47	36 45	cfv	$class \cdot_{r (n)}$
48	30 32 47	co	$class (x \cdot_{r (n)} y)$
49	48 27	cfv	$class g (n) (x \cdot_{r (n)} y)$
50	34 49	cop	$class ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩$
51	24 29 28 28 50	cmpo	$class (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)$
52	51	crn	$class ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)$
53	22 23 52	ciun	$class ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)$
54	46 53	cop	$class ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩$
55	19 44 54	ctp	$class \{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\}$
56		ctopn	$class TopOpen$
57	16 56	cfv	$class TopOpen (ndx)$
58		vs	$setvar s$
59	18	cpw	$class 𝒫 v$
60	27	ccnv	$class {g (n)}^{-1}$
61	58	cv	$setvar s$
62	60 61	cima	$class {g (n)}^{-1} [s]$
63	36 56	cfv	$class TopOpen (r (n))$
64	62 63	wcel	$wff {g (n)}^{-1} [s] \in TopOpen (r (n))$
65	64 22 23	wral	$wff \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))$
66	65 58 59	crab	$class \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}$
67	57 66	cop	$class ⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩$
68		cds	$class dist$
69	16 68	cfv	$class dist (ndx)$
70	26 27	cfv	$class g (n) (n)$
71	70	cdm	$class dom g (n) (n)$
72	36 68	cfv	$class dist (r (n))$
73	30 32 72	co	$class (x dist (r (n)) y)$
74	34 73	cop	$class ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩$
75	24 29 71 71 74	cmpo	$class (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)$
76	75	crn	$class ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)$
77	22 23 76	ciun	$class ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)$
78	69 77	cop	$class ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩$
79		cple	$class le$
80	16 79	cfv	$class \leq_{ndx}$
81	36 79	cfv	$class \leq_{r (n)}$
82	81 27	ccom	$class (\leq_{r (n)} \circ g (n))$
83	60 82	ccom	$class ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))$
84	22 23 83	ciun	$class ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))$
85	80 84	cop	$class ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩$
86	67 78 85	ctp	$class \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\}$
87	55 86	cun	$class (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\})$
88	14 13 87	csb	$class ⦋ 2^{nd} (e) / g ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\})$
89	11 10 88	csb	$class ⦋ 1^{st} (e) / v ⦌ ⦋ 2^{nd} (e) / g ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\})$
90	7 6 89	csb	$class ⦋ HomLimB (f) / e ⦌ ⦋ 1^{st} (e) / v ⦌ ⦋ 2^{nd} (e) / g ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\})$
91	1 3 2 2 90	cmpo	$class (r \in V, f \in V ⟼ ⦋ HomLimB (f) / e ⦌ ⦋ 1^{st} (e) / v ⦌ ⦋ 2^{nd} (e) / g ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\}))$
92	0 91	wceq	$wff HomLim = (r \in V, f \in V ⟼ ⦋ HomLimB (f) / e ⦌ ⦋ 1^{st} (e) / v ⦌ ⦋ 2^{nd} (e) / g ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x +_{r (n)} y)⟩)⟩, ⟨\cdot_{ndx}, ⋃_{n \in ℕ} ran (x \in dom g (n), y \in dom g (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, g (n) (x \cdot_{r (n)} y)⟩)⟩\} \cup \{⟨TopOpen (ndx), \{s \in 𝒫 v \| \forall n \in ℕ {g (n)}^{-1} [s] \in TopOpen (r (n))\}⟩, ⟨dist (ndx), ⋃_{n \in ℕ} ran (x \in dom g (n) (n), y \in dom g (n) (n) ⟼ ⟨⟨g (n) (x), g (n) (y)⟩, x dist (r (n)) y⟩)⟩, ⟨\leq_{ndx}, ⋃_{n \in ℕ} ({g (n)}^{-1} \circ (\leq_{r (n)} \circ g (n)))⟩\}))$

Metamath Proof Explorer

Definition df-homlim

Detailed syntax breakdown