Definition 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 = ( 𝑟 ∈ V , 𝑓 ∈ V ↦ ⦋ ( HomLimB ‘ 𝑓 ) / 𝑒 ⦌ ⦋ ( 1st ‘ 𝑒 ) / 𝑣 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑔 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlim	⊢ HomLim
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		chlb	⊢ HomLimB
5	3	cv	⊢ 𝑓
6	5 4	cfv	⊢ ( HomLimB ‘ 𝑓 )
7		ve	⊢ 𝑒
8		c1st	⊢ 1st
9	7	cv	⊢ 𝑒
10	9 8	cfv	⊢ ( 1st ‘ 𝑒 )
11		vv	⊢ 𝑣
12		c2nd	⊢ 2nd
13	9 12	cfv	⊢ ( 2nd ‘ 𝑒 )
14		vg	⊢ 𝑔
15		cbs	⊢ Base
16		cnx	⊢ ndx
17	16 15	cfv	⊢ ( Base ‘ ndx )
18	11	cv	⊢ 𝑣
19	17 18	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑣 ⟩
20		cplusg	⊢ +g
21	16 20	cfv	⊢ ( +g ‘ ndx )
22		vn	⊢ 𝑛
23		cn	⊢ ℕ
24		vx	⊢ 𝑥
25	14	cv	⊢ 𝑔
26	22	cv	⊢ 𝑛
27	26 25	cfv	⊢ ( 𝑔 ‘ 𝑛 )
28	27	cdm	⊢ dom ( 𝑔 ‘ 𝑛 )
29		vy	⊢ 𝑦
30	24	cv	⊢ 𝑥
31	30 27	cfv	⊢ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 )
32	29	cv	⊢ 𝑦
33	32 27	cfv	⊢ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 )
34	31 33	cop	⊢ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩
35	1	cv	⊢ 𝑟
36	26 35	cfv	⊢ ( 𝑟 ‘ 𝑛 )
37	36 20	cfv	⊢ ( +g ‘ ( 𝑟 ‘ 𝑛 ) )
38	30 32 37	co	⊢ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 )
39	38 27	cfv	⊢ ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) )
40	34 39	cop	⊢ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩
41	24 29 28 28 40	cmpo	⊢ ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ )
42	41	crn	⊢ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ )
43	22 23 42	ciun	⊢ ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ )
44	21 43	cop	⊢ ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩
45		cmulr	⊢ .r
46	16 45	cfv	⊢ ( .r ‘ ndx )
47	36 45	cfv	⊢ ( .r ‘ ( 𝑟 ‘ 𝑛 ) )
48	30 32 47	co	⊢ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 )
49	48 27	cfv	⊢ ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) )
50	34 49	cop	⊢ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩
51	24 29 28 28 50	cmpo	⊢ ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ )
52	51	crn	⊢ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ )
53	22 23 52	ciun	⊢ ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ )
54	46 53	cop	⊢ ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩
55	19 44 54	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ }
56		ctopn	⊢ TopOpen
57	16 56	cfv	⊢ ( TopOpen ‘ ndx )
58		vs	⊢ 𝑠
59	18	cpw	⊢ 𝒫 𝑣
60	27	ccnv	⊢ ◡ ( 𝑔 ‘ 𝑛 )
61	58	cv	⊢ 𝑠
62	60 61	cima	⊢ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 )
63	36 56	cfv	⊢ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) )
64	62 63	wcel	⊢ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) )
65	64 22 23	wral	⊢ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) )
66	65 58 59	crab	⊢ { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) }
67	57 66	cop	⊢ ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩
68		cds	⊢ dist
69	16 68	cfv	⊢ ( dist ‘ ndx )
70	26 27	cfv	⊢ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 )
71	70	cdm	⊢ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 )
72	36 68	cfv	⊢ ( dist ‘ ( 𝑟 ‘ 𝑛 ) )
73	30 32 72	co	⊢ ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 )
74	34 73	cop	⊢ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩
75	24 29 71 71 74	cmpo	⊢ ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ )
76	75	crn	⊢ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ )
77	22 23 76	ciun	⊢ ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ )
78	69 77	cop	⊢ ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩
79		cple	⊢ le
80	16 79	cfv	⊢ ( le ‘ ndx )
81	36 79	cfv	⊢ ( le ‘ ( 𝑟 ‘ 𝑛 ) )
82	81 27	ccom	⊢ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) )
83	60 82	ccom	⊢ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) )
84	22 23 83	ciun	⊢ ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) )
85	80 84	cop	⊢ ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩
86	67 78 85	ctp	⊢ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ }
87	55 86	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } )
88	14 13 87	csb	⊢ ⦋ ( 2nd ‘ 𝑒 ) / 𝑔 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } )
89	11 10 88	csb	⊢ ⦋ ( 1st ‘ 𝑒 ) / 𝑣 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑔 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } )
90	7 6 89	csb	⊢ ⦋ ( HomLimB ‘ 𝑓 ) / 𝑒 ⦌ ⦋ ( 1st ‘ 𝑒 ) / 𝑣 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑔 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } )
91	1 3 2 2 90	cmpo	⊢ ( 𝑟 ∈ V , 𝑓 ∈ V ↦ ⦋ ( HomLimB ‘ 𝑓 ) / 𝑒 ⦌ ⦋ ( 1st ‘ 𝑒 ) / 𝑣 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑔 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } ) )
92	0 91	wceq	⊢ HomLim = ( 𝑟 ∈ V , 𝑓 ∈ V ↦ ⦋ ( HomLimB ‘ 𝑓 ) / 𝑒 ⦌ ⦋ ( 1st ‘ 𝑒 ) / 𝑣 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑔 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( +g ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( 𝑔 ‘ 𝑛 ) , 𝑦 ∈ dom ( 𝑔 ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( ( 𝑔 ‘ 𝑛 ) ‘ ( 𝑥 ( .r ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( TopOpen ‘ ndx ) , { 𝑠 ∈ 𝒫 𝑣 ∣ ∀ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) “ 𝑠 ) ∈ ( TopOpen ‘ ( 𝑟 ‘ 𝑛 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ∪ 𝑛 ∈ ℕ ran ( 𝑥 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) , 𝑦 ∈ dom ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑛 ) ↦ ⟨ ⟨ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) , ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑦 ) ⟩ , ( 𝑥 ( dist ‘ ( 𝑟 ‘ 𝑛 ) ) 𝑦 ) ⟩ ) ⟩ , ⟨ ( le ‘ ndx ) , ∪ 𝑛 ∈ ℕ ( ◡ ( 𝑔 ‘ 𝑛 ) ∘ ( ( le ‘ ( 𝑟 ‘ 𝑛 ) ) ∘ ( 𝑔 ‘ 𝑛 ) ) ) ⟩ } ) )