Detailed syntax breakdown of Definition df-pt
Step | Hyp | Ref
| Expression |
1 | | cpt 12437 |
. 2
class
∏t |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | cvv 2712 |
. . 3
class
V |
4 | | vg |
. . . . . . . . . 10
setvar 𝑔 |
5 | 4 | cv 1334 |
. . . . . . . . 9
class 𝑔 |
6 | 2 | cv 1334 |
. . . . . . . . . 10
class 𝑓 |
7 | 6 | cdm 4588 |
. . . . . . . . 9
class dom 𝑓 |
8 | 5, 7 | wfn 5167 |
. . . . . . . 8
wff 𝑔 Fn dom 𝑓 |
9 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
10 | 9 | cv 1334 |
. . . . . . . . . . 11
class 𝑦 |
11 | 10, 5 | cfv 5172 |
. . . . . . . . . 10
class (𝑔‘𝑦) |
12 | 10, 6 | cfv 5172 |
. . . . . . . . . 10
class (𝑓‘𝑦) |
13 | 11, 12 | wcel 2128 |
. . . . . . . . 9
wff (𝑔‘𝑦) ∈ (𝑓‘𝑦) |
14 | 13, 9, 7 | wral 2435 |
. . . . . . . 8
wff
∀𝑦 ∈ dom
𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) |
15 | 12 | cuni 3774 |
. . . . . . . . . . 11
class ∪ (𝑓‘𝑦) |
16 | 11, 15 | wceq 1335 |
. . . . . . . . . 10
wff (𝑔‘𝑦) = ∪ (𝑓‘𝑦) |
17 | | vz |
. . . . . . . . . . . 12
setvar 𝑧 |
18 | 17 | cv 1334 |
. . . . . . . . . . 11
class 𝑧 |
19 | 7, 18 | cdif 3099 |
. . . . . . . . . 10
class (dom
𝑓 ∖ 𝑧) |
20 | 16, 9, 19 | wral 2435 |
. . . . . . . . 9
wff
∀𝑦 ∈
(dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦) |
21 | | cfn 6687 |
. . . . . . . . 9
class
Fin |
22 | 20, 17, 21 | wrex 2436 |
. . . . . . . 8
wff
∃𝑧 ∈ Fin
∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦) |
23 | 8, 14, 22 | w3a 963 |
. . . . . . 7
wff (𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) |
24 | | vx |
. . . . . . . . 9
setvar 𝑥 |
25 | 24 | cv 1334 |
. . . . . . . 8
class 𝑥 |
26 | 9, 7, 11 | cixp 6645 |
. . . . . . . 8
class X𝑦 ∈
dom 𝑓(𝑔‘𝑦) |
27 | 25, 26 | wceq 1335 |
. . . . . . 7
wff 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦) |
28 | 23, 27 | wa 103 |
. . . . . 6
wff ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦)) |
29 | 28, 4 | wex 1472 |
. . . . 5
wff
∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦)) |
30 | 29, 24 | cab 2143 |
. . . 4
class {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))} |
31 | | ctg 12436 |
. . . 4
class
topGen |
32 | 30, 31 | cfv 5172 |
. . 3
class
(topGen‘{𝑥
∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}) |
33 | 2, 3, 32 | cmpt 4027 |
. 2
class (𝑓 ∈ V ↦
(topGen‘{𝑥 ∣
∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) |
34 | 1, 33 | wceq 1335 |
1
wff
∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) |