Metamath Proof Explorer


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 ‘ ( 𝑟𝑛 ) ) ∘ ( 𝑔𝑛 ) ) ) ⟩ } ) )