Detailed syntax breakdown of Definition df-mp
Step | Hyp | Ref
| Expression |
1 | | cmp 10476 |
. 2
class
·P |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cnp 10473 |
. . 3
class
P |
5 | | vw |
. . . . . . . 8
setvar 𝑤 |
6 | 5 | cv 1542 |
. . . . . . 7
class 𝑤 |
7 | | vv |
. . . . . . . . 9
setvar 𝑣 |
8 | 7 | cv 1542 |
. . . . . . . 8
class 𝑣 |
9 | | vu |
. . . . . . . . 9
setvar 𝑢 |
10 | 9 | cv 1542 |
. . . . . . . 8
class 𝑢 |
11 | | cmq 10470 |
. . . . . . . 8
class
·Q |
12 | 8, 10, 11 | co 7213 |
. . . . . . 7
class (𝑣
·Q 𝑢) |
13 | 6, 12 | wceq 1543 |
. . . . . 6
wff 𝑤 = (𝑣 ·Q 𝑢) |
14 | 3 | cv 1542 |
. . . . . 6
class 𝑦 |
15 | 13, 9, 14 | wrex 3062 |
. . . . 5
wff
∃𝑢 ∈
𝑦 𝑤 = (𝑣 ·Q 𝑢) |
16 | 2 | cv 1542 |
. . . . 5
class 𝑥 |
17 | 15, 7, 16 | wrex 3062 |
. . . 4
wff
∃𝑣 ∈
𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 ·Q 𝑢) |
18 | 17, 5 | cab 2714 |
. . 3
class {𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 ·Q 𝑢)} |
19 | 2, 3, 4, 4, 18 | cmpo 7215 |
. 2
class (𝑥 ∈ P, 𝑦 ∈ P ↦
{𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 ·Q 𝑢)}) |
20 | 1, 19 | wceq 1543 |
1
wff
·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 ·Q 𝑢)}) |