Detailed syntax breakdown of Definition df-lm
Step | Hyp | Ref
| Expression |
1 | | clm 12587 |
. 2
class
⇝𝑡 |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | ctop 12395 |
. . 3
class
Top |
4 | | vf |
. . . . . . 7
setvar 𝑓 |
5 | 4 | cv 1334 |
. . . . . 6
class 𝑓 |
6 | 2 | cv 1334 |
. . . . . . . 8
class 𝑗 |
7 | 6 | cuni 3772 |
. . . . . . 7
class ∪ 𝑗 |
8 | | cc 7730 |
. . . . . . 7
class
ℂ |
9 | | cpm 6594 |
. . . . . . 7
class
↑pm |
10 | 7, 8, 9 | co 5824 |
. . . . . 6
class (∪ 𝑗
↑pm ℂ) |
11 | 5, 10 | wcel 2128 |
. . . . 5
wff 𝑓 ∈ (∪ 𝑗
↑pm ℂ) |
12 | | vx |
. . . . . . 7
setvar 𝑥 |
13 | 12 | cv 1334 |
. . . . . 6
class 𝑥 |
14 | 13, 7 | wcel 2128 |
. . . . 5
wff 𝑥 ∈ ∪ 𝑗 |
15 | | vu |
. . . . . . . 8
setvar 𝑢 |
16 | 12, 15 | wel 2129 |
. . . . . . 7
wff 𝑥 ∈ 𝑢 |
17 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
18 | 17 | cv 1334 |
. . . . . . . . 9
class 𝑦 |
19 | 15 | cv 1334 |
. . . . . . . . 9
class 𝑢 |
20 | 5, 18 | cres 4588 |
. . . . . . . . 9
class (𝑓 ↾ 𝑦) |
21 | 18, 19, 20 | wf 5166 |
. . . . . . . 8
wff (𝑓 ↾ 𝑦):𝑦⟶𝑢 |
22 | | cuz 9439 |
. . . . . . . . 9
class
ℤ≥ |
23 | 22 | crn 4587 |
. . . . . . . 8
class ran
ℤ≥ |
24 | 21, 17, 23 | wrex 2436 |
. . . . . . 7
wff
∃𝑦 ∈ ran
ℤ≥(𝑓
↾ 𝑦):𝑦⟶𝑢 |
25 | 16, 24 | wi 4 |
. . . . . 6
wff (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢) |
26 | 25, 15, 6 | wral 2435 |
. . . . 5
wff
∀𝑢 ∈
𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢) |
27 | 11, 14, 26 | w3a 963 |
. . . 4
wff (𝑓 ∈ (∪ 𝑗
↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢)) |
28 | 27, 4, 12 | copab 4024 |
. . 3
class
{〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗
↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))} |
29 | 2, 3, 28 | cmpt 4025 |
. 2
class (𝑗 ∈ Top ↦ {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗 ↑pm
ℂ) ∧ 𝑥 ∈
∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) |
30 | 1, 29 | wceq 1335 |
1
wff
⇝𝑡 = (𝑗 ∈ Top ↦ {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗 ↑pm
ℂ) ∧ 𝑥 ∈
∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) |