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