Detailed syntax breakdown of Definition df-homlim
Step | Hyp | Ref
| Expression |
1 | | chlim 33155 |
. 2
class
HomLim |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3397 |
. . 3
class
V |
5 | | ve |
. . . 4
setvar 𝑒 |
6 | 3 | cv 1541 |
. . . . 5
class 𝑓 |
7 | | chlb 33154 |
. . . . 5
class
HomLimB |
8 | 6, 7 | cfv 6333 |
. . . 4
class ( HomLimB
‘𝑓) |
9 | | vv |
. . . . 5
setvar 𝑣 |
10 | 5 | cv 1541 |
. . . . . 6
class 𝑒 |
11 | | c1st 7705 |
. . . . . 6
class
1st |
12 | 10, 11 | cfv 6333 |
. . . . 5
class
(1st ‘𝑒) |
13 | | vg |
. . . . . 6
setvar 𝑔 |
14 | | c2nd 7706 |
. . . . . . 7
class
2nd |
15 | 10, 14 | cfv 6333 |
. . . . . 6
class
(2nd ‘𝑒) |
16 | | cnx 16576 |
. . . . . . . . . 10
class
ndx |
17 | | cbs 16579 |
. . . . . . . . . 10
class
Base |
18 | 16, 17 | cfv 6333 |
. . . . . . . . 9
class
(Base‘ndx) |
19 | 9 | cv 1541 |
. . . . . . . . 9
class 𝑣 |
20 | 18, 19 | cop 4519 |
. . . . . . . 8
class
〈(Base‘ndx), 𝑣〉 |
21 | | cplusg 16661 |
. . . . . . . . . 10
class
+g |
22 | 16, 21 | cfv 6333 |
. . . . . . . . 9
class
(+g‘ndx) |
23 | | vn |
. . . . . . . . . 10
setvar 𝑛 |
24 | | cn 11709 |
. . . . . . . . . 10
class
ℕ |
25 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
26 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
27 | 23 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑛 |
28 | 13 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑔 |
29 | 27, 28 | cfv 6333 |
. . . . . . . . . . . . 13
class (𝑔‘𝑛) |
30 | 29 | cdm 5519 |
. . . . . . . . . . . 12
class dom
(𝑔‘𝑛) |
31 | 25 | cv 1541 |
. . . . . . . . . . . . . . 15
class 𝑥 |
32 | 31, 29 | cfv 6333 |
. . . . . . . . . . . . . 14
class ((𝑔‘𝑛)‘𝑥) |
33 | 26 | cv 1541 |
. . . . . . . . . . . . . . 15
class 𝑦 |
34 | 33, 29 | cfv 6333 |
. . . . . . . . . . . . . 14
class ((𝑔‘𝑛)‘𝑦) |
35 | 32, 34 | cop 4519 |
. . . . . . . . . . . . 13
class
〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉 |
36 | 2 | cv 1541 |
. . . . . . . . . . . . . . . . 17
class 𝑟 |
37 | 27, 36 | cfv 6333 |
. . . . . . . . . . . . . . . 16
class (𝑟‘𝑛) |
38 | 37, 21 | cfv 6333 |
. . . . . . . . . . . . . . 15
class
(+g‘(𝑟‘𝑛)) |
39 | 31, 33, 38 | co 7164 |
. . . . . . . . . . . . . 14
class (𝑥(+g‘(𝑟‘𝑛))𝑦) |
40 | 39, 29 | cfv 6333 |
. . . . . . . . . . . . 13
class ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦)) |
41 | 35, 40 | cop 4519 |
. . . . . . . . . . . 12
class
〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))〉 |
42 | 25, 26, 30, 30, 41 | cmpo 7166 |
. . . . . . . . . . 11
class (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))〉) |
43 | 42 | crn 5520 |
. . . . . . . . . 10
class ran
(𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))〉) |
44 | 23, 24, 43 | ciun 4878 |
. . . . . . . . 9
class ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))〉) |
45 | 22, 44 | cop 4519 |
. . . . . . . 8
class
〈(+g‘ndx), ∪
𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))〉)〉 |
46 | | cmulr 16662 |
. . . . . . . . . 10
class
.r |
47 | 16, 46 | cfv 6333 |
. . . . . . . . 9
class
(.r‘ndx) |
48 | 37, 46 | cfv 6333 |
. . . . . . . . . . . . . . 15
class
(.r‘(𝑟‘𝑛)) |
49 | 31, 33, 48 | co 7164 |
. . . . . . . . . . . . . 14
class (𝑥(.r‘(𝑟‘𝑛))𝑦) |
50 | 49, 29 | cfv 6333 |
. . . . . . . . . . . . 13
class ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦)) |
51 | 35, 50 | cop 4519 |
. . . . . . . . . . . 12
class
〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))〉 |
52 | 25, 26, 30, 30, 51 | cmpo 7166 |
. . . . . . . . . . 11
class (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))〉) |
53 | 52 | crn 5520 |
. . . . . . . . . 10
class ran
(𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))〉) |
54 | 23, 24, 53 | ciun 4878 |
. . . . . . . . 9
class ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))〉) |
55 | 47, 54 | cop 4519 |
. . . . . . . 8
class
〈(.r‘ndx), ∪
𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))〉)〉 |
56 | 20, 45, 55 | ctp 4517 |
. . . . . . 7
class
{〈(Base‘ndx), 𝑣〉, 〈(+g‘ndx),
∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))〉)〉,
〈(.r‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))〉)〉} |
57 | | ctopn 16791 |
. . . . . . . . . 10
class
TopOpen |
58 | 16, 57 | cfv 6333 |
. . . . . . . . 9
class
(TopOpen‘ndx) |
59 | 29 | ccnv 5518 |
. . . . . . . . . . . . 13
class ◡(𝑔‘𝑛) |
60 | | vs |
. . . . . . . . . . . . . 14
setvar 𝑠 |
61 | 60 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑠 |
62 | 59, 61 | cima 5522 |
. . . . . . . . . . . 12
class (◡(𝑔‘𝑛) “ 𝑠) |
63 | 37, 57 | cfv 6333 |
. . . . . . . . . . . 12
class
(TopOpen‘(𝑟‘𝑛)) |
64 | 62, 63 | wcel 2113 |
. . . . . . . . . . 11
wff (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛)) |
65 | 64, 23, 24 | wral 3053 |
. . . . . . . . . 10
wff
∀𝑛 ∈
ℕ (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛)) |
66 | 19 | cpw 4485 |
. . . . . . . . . 10
class 𝒫
𝑣 |
67 | 65, 60, 66 | crab 3057 |
. . . . . . . . 9
class {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛))} |
68 | 58, 67 | cop 4519 |
. . . . . . . 8
class
〈(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛))}〉 |
69 | | cds 16670 |
. . . . . . . . . 10
class
dist |
70 | 16, 69 | cfv 6333 |
. . . . . . . . 9
class
(dist‘ndx) |
71 | 27, 29 | cfv 6333 |
. . . . . . . . . . . . 13
class ((𝑔‘𝑛)‘𝑛) |
72 | 71 | cdm 5519 |
. . . . . . . . . . . 12
class dom
((𝑔‘𝑛)‘𝑛) |
73 | 37, 69 | cfv 6333 |
. . . . . . . . . . . . . 14
class
(dist‘(𝑟‘𝑛)) |
74 | 31, 33, 73 | co 7164 |
. . . . . . . . . . . . 13
class (𝑥(dist‘(𝑟‘𝑛))𝑦) |
75 | 35, 74 | cop 4519 |
. . . . . . . . . . . 12
class
〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, (𝑥(dist‘(𝑟‘𝑛))𝑦)〉 |
76 | 25, 26, 72, 72, 75 | cmpo 7166 |
. . . . . . . . . . 11
class (𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, (𝑥(dist‘(𝑟‘𝑛))𝑦)〉) |
77 | 76 | crn 5520 |
. . . . . . . . . 10
class ran
(𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, (𝑥(dist‘(𝑟‘𝑛))𝑦)〉) |
78 | 23, 24, 77 | ciun 4878 |
. . . . . . . . 9
class ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, (𝑥(dist‘(𝑟‘𝑛))𝑦)〉) |
79 | 70, 78 | cop 4519 |
. . . . . . . 8
class
〈(dist‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, (𝑥(dist‘(𝑟‘𝑛))𝑦)〉)〉 |
80 | | cple 16668 |
. . . . . . . . . 10
class
le |
81 | 16, 80 | cfv 6333 |
. . . . . . . . 9
class
(le‘ndx) |
82 | 37, 80 | cfv 6333 |
. . . . . . . . . . . 12
class
(le‘(𝑟‘𝑛)) |
83 | 82, 29 | ccom 5523 |
. . . . . . . . . . 11
class
((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)) |
84 | 59, 83 | ccom 5523 |
. . . . . . . . . 10
class (◡(𝑔‘𝑛) ∘ ((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛))) |
85 | 23, 24, 84 | ciun 4878 |
. . . . . . . . 9
class ∪ 𝑛 ∈ ℕ (◡(𝑔‘𝑛) ∘ ((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛))) |
86 | 81, 85 | cop 4519 |
. . . . . . . 8
class
〈(le‘ndx), ∪ 𝑛 ∈ ℕ (◡(𝑔‘𝑛) ∘ ((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)))〉 |
87 | 68, 79, 86 | ctp 4517 |
. . . . . . 7
class
{〈(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛))}〉, 〈(dist‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ 〈〈((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)〉, (𝑥(dist‘(𝑟‘𝑛))𝑦)〉)〉, 〈(le‘ndx),
∪ 𝑛 ∈ ℕ (◡(𝑔‘𝑛) ∘ ((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)))〉} |
88 | 56, 87 | cun 3839 |
. . . . . 6
class
({〈(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 | 13, 15, 88 | csb 3788 |
. . . . 5
class
⦋(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 | 9, 12, 89 | csb 3788 |
. . . 4
class
⦋(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 | 5, 8, 90 | csb 3788 |
. . 3
class
⦋( 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 | 2, 3, 4, 4, 91 | cmpo 7166 |
. 2
class (𝑟 ∈ 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‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)))〉})) |
93 | 1, 92 | wceq 1542 |
1
wff 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‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)))〉})) |