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 \in V ⟼ ⦋ ⋃_{n \in ℕ} (\{n\} \times dom f (n)) / v ⦌ ⦋ ⋂ \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)\} / e ⦌ ⟨v / e, (n \in ℕ ⟼ (x \in 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\} \times dom f (n))$
11	3 4 10	ciun	$class ⋃_{n \in ℕ} (\{n\} \times 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 \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩)$
30	29 14	wss	$wff (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s$
31	16 30	wa	$wff (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)$
32	31 13	cab	$class \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)\}$
33	32	cint	$class ⋂ \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq 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 \in dom f (n) ⟼ [⟨n, x⟩] e)$
40	3 4 39	cmpt	$class (n \in ℕ ⟼ (x \in dom f (n) ⟼ [⟨n, x⟩] e))$
41	36 40	cop	$class ⟨v / e, (n \in ℕ ⟼ (x \in dom f (n) ⟼ [⟨n, x⟩] e))⟩$
42	34 33 41	csb	$class ⦋ ⋂ \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)\} / e ⦌ ⟨v / e, (n \in ℕ ⟼ (x \in dom f (n) ⟼ [⟨n, x⟩] e))⟩$
43	12 11 42	csb	$class ⦋ ⋃_{n \in ℕ} (\{n\} \times dom f (n)) / v ⦌ ⦋ ⋂ \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)\} / e ⦌ ⟨v / e, (n \in ℕ ⟼ (x \in dom f (n) ⟼ [⟨n, x⟩] e))⟩$
44	1 2 43	cmpt	$class (f \in V ⟼ ⦋ ⋃_{n \in ℕ} (\{n\} \times dom f (n)) / v ⦌ ⦋ ⋂ \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)\} / e ⦌ ⟨v / e, (n \in ℕ ⟼ (x \in dom f (n) ⟼ [⟨n, x⟩] e))⟩)$
45	0 44	wceq	$wff HomLimB = (f \in V ⟼ ⦋ ⋃_{n \in ℕ} (\{n\} \times dom f (n)) / v ⦌ ⦋ ⋂ \{s \| (s Er v \land (x \in v ⟼ ⟨1^{st} (x) + 1, f (1^{st} (x)) (2^{nd} (x))⟩) \subseteq s)\} / e ⦌ ⟨v / e, (n \in ℕ ⟼ (x \in dom f (n) ⟼ [⟨n, x⟩] e))⟩)$

Metamath Proof Explorer

Definition df-homlimb

Detailed syntax breakdown