Detailed syntax breakdown of Definition df-ucn
Step | Hyp | Ref
| Expression |
1 | | cucn 23027 |
. 2
class
Cnu |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | vv |
. . 3
setvar 𝑣 |
4 | | cust 22951 |
. . . . 5
class
UnifOn |
5 | 4 | crn 5526 |
. . . 4
class ran
UnifOn |
6 | 5 | cuni 4796 |
. . 3
class ∪ ran UnifOn |
7 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
8 | 7 | cv 1541 |
. . . . . . . . . 10
class 𝑥 |
9 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
10 | 9 | cv 1541 |
. . . . . . . . . 10
class 𝑦 |
11 | | vr |
. . . . . . . . . . 11
setvar 𝑟 |
12 | 11 | cv 1541 |
. . . . . . . . . 10
class 𝑟 |
13 | 8, 10, 12 | wbr 5030 |
. . . . . . . . 9
wff 𝑥𝑟𝑦 |
14 | | vf |
. . . . . . . . . . . 12
setvar 𝑓 |
15 | 14 | cv 1541 |
. . . . . . . . . . 11
class 𝑓 |
16 | 8, 15 | cfv 6339 |
. . . . . . . . . 10
class (𝑓‘𝑥) |
17 | 10, 15 | cfv 6339 |
. . . . . . . . . 10
class (𝑓‘𝑦) |
18 | | vs |
. . . . . . . . . . 11
setvar 𝑠 |
19 | 18 | cv 1541 |
. . . . . . . . . 10
class 𝑠 |
20 | 16, 17, 19 | wbr 5030 |
. . . . . . . . 9
wff (𝑓‘𝑥)𝑠(𝑓‘𝑦) |
21 | 13, 20 | wi 4 |
. . . . . . . 8
wff (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) |
22 | 2 | cv 1541 |
. . . . . . . . . 10
class 𝑢 |
23 | 22 | cuni 4796 |
. . . . . . . . 9
class ∪ 𝑢 |
24 | 23 | cdm 5525 |
. . . . . . . 8
class dom ∪ 𝑢 |
25 | 21, 9, 24 | wral 3053 |
. . . . . . 7
wff
∀𝑦 ∈ dom
∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) |
26 | 25, 7, 24 | wral 3053 |
. . . . . 6
wff
∀𝑥 ∈ dom
∪ 𝑢∀𝑦 ∈ dom ∪
𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) |
27 | 26, 11, 22 | wrex 3054 |
. . . . 5
wff
∃𝑟 ∈
𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪
𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) |
28 | 3 | cv 1541 |
. . . . 5
class 𝑣 |
29 | 27, 18, 28 | wral 3053 |
. . . 4
wff
∀𝑠 ∈
𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪
𝑢∀𝑦 ∈ dom ∪
𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) |
30 | 28 | cuni 4796 |
. . . . . 6
class ∪ 𝑣 |
31 | 30 | cdm 5525 |
. . . . 5
class dom ∪ 𝑣 |
32 | | cmap 8437 |
. . . . 5
class
↑m |
33 | 31, 24, 32 | co 7170 |
. . . 4
class (dom
∪ 𝑣 ↑m dom ∪ 𝑢) |
34 | 29, 14, 33 | crab 3057 |
. . 3
class {𝑓 ∈ (dom ∪ 𝑣
↑m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪
𝑢∀𝑦 ∈ dom ∪
𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} |
35 | 2, 3, 6, 6, 34 | cmpo 7172 |
. 2
class (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran
UnifOn ↦ {𝑓 ∈
(dom ∪ 𝑣 ↑m dom ∪ 𝑢)
∣ ∀𝑠 ∈
𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪
𝑢∀𝑦 ∈ dom ∪
𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) |
36 | 1, 35 | wceq 1542 |
1
wff
Cnu = (𝑢 ∈
∪ ran UnifOn, 𝑣 ∈ ∪ ran
UnifOn ↦ {𝑓 ∈
(dom ∪ 𝑣 ↑m dom ∪ 𝑢)
∣ ∀𝑠 ∈
𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪
𝑢∀𝑦 ∈ dom ∪
𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) |