Detailed syntax breakdown of Definition df-plq0
Step | Hyp | Ref
| Expression |
1 | | cplq0 7224 |
. 2
class
+Q0 |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1341 |
. . . . . 6
class 𝑥 |
4 | | cnq0 7222 |
. . . . . 6
class
Q0 |
5 | 3, 4 | wcel 2135 |
. . . . 5
wff 𝑥 ∈
Q0 |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1341 |
. . . . . 6
class 𝑦 |
8 | 7, 4 | wcel 2135 |
. . . . 5
wff 𝑦 ∈
Q0 |
9 | 5, 8 | wa 103 |
. . . 4
wff (𝑥 ∈
Q0 ∧ 𝑦 ∈
Q0) |
10 | | vw |
. . . . . . . . . . . . . 14
setvar 𝑤 |
11 | 10 | cv 1341 |
. . . . . . . . . . . . 13
class 𝑤 |
12 | | vv |
. . . . . . . . . . . . . 14
setvar 𝑣 |
13 | 12 | cv 1341 |
. . . . . . . . . . . . 13
class 𝑣 |
14 | 11, 13 | cop 3576 |
. . . . . . . . . . . 12
class
〈𝑤, 𝑣〉 |
15 | | ceq0 7221 |
. . . . . . . . . . . 12
class
~Q0 |
16 | 14, 15 | cec 6493 |
. . . . . . . . . . 11
class
[〈𝑤, 𝑣〉]
~Q0 |
17 | 3, 16 | wceq 1342 |
. . . . . . . . . 10
wff 𝑥 = [〈𝑤, 𝑣〉]
~Q0 |
18 | | vu |
. . . . . . . . . . . . . 14
setvar 𝑢 |
19 | 18 | cv 1341 |
. . . . . . . . . . . . 13
class 𝑢 |
20 | | vf |
. . . . . . . . . . . . . 14
setvar 𝑓 |
21 | 20 | cv 1341 |
. . . . . . . . . . . . 13
class 𝑓 |
22 | 19, 21 | cop 3576 |
. . . . . . . . . . . 12
class
〈𝑢, 𝑓〉 |
23 | 22, 15 | cec 6493 |
. . . . . . . . . . 11
class
[〈𝑢, 𝑓〉]
~Q0 |
24 | 7, 23 | wceq 1342 |
. . . . . . . . . 10
wff 𝑦 = [〈𝑢, 𝑓〉]
~Q0 |
25 | 17, 24 | wa 103 |
. . . . . . . . 9
wff (𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0
) |
26 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
27 | 26 | cv 1341 |
. . . . . . . . . 10
class 𝑧 |
28 | | comu 6376 |
. . . . . . . . . . . . . 14
class
·o |
29 | 11, 21, 28 | co 5839 |
. . . . . . . . . . . . 13
class (𝑤 ·o 𝑓) |
30 | 13, 19, 28 | co 5839 |
. . . . . . . . . . . . 13
class (𝑣 ·o 𝑢) |
31 | | coa 6375 |
. . . . . . . . . . . . 13
class
+o |
32 | 29, 30, 31 | co 5839 |
. . . . . . . . . . . 12
class ((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)) |
33 | 13, 21, 28 | co 5839 |
. . . . . . . . . . . 12
class (𝑣 ·o 𝑓) |
34 | 32, 33 | cop 3576 |
. . . . . . . . . . 11
class
〈((𝑤
·o 𝑓)
+o (𝑣
·o 𝑢)),
(𝑣 ·o
𝑓)〉 |
35 | 34, 15 | cec 6493 |
. . . . . . . . . 10
class
[〈((𝑤
·o 𝑓)
+o (𝑣
·o 𝑢)),
(𝑣 ·o
𝑓)〉]
~Q0 |
36 | 27, 35 | wceq 1342 |
. . . . . . . . 9
wff 𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉]
~Q0 |
37 | 25, 36 | wa 103 |
. . . . . . . 8
wff ((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
) |
38 | 37, 20 | wex 1479 |
. . . . . . 7
wff
∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
) |
39 | 38, 18 | wex 1479 |
. . . . . 6
wff
∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
) |
40 | 39, 12 | wex 1479 |
. . . . 5
wff
∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
) |
41 | 40, 10 | wex 1479 |
. . . 4
wff
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
) |
42 | 9, 41 | wa 103 |
. . 3
wff ((𝑥 ∈
Q0 ∧ 𝑦 ∈ Q0) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
)) |
43 | 42, 2, 6, 26 | coprab 5840 |
. 2
class
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
))} |
44 | 1, 43 | wceq 1342 |
1
wff
+Q0 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q0 ∧
𝑦 ∈
Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q0 ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q0 ) ∧
𝑧 = [〈((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)〉] ~Q0
))} |