Detailed syntax breakdown of Definition df-mq0
Step | Hyp | Ref
| Expression |
1 | | cmq0 6388 |
. 2
·Q0 |
2 | | vx |
. . . . . . 7
|
3 | 2 | cv 1242 |
. . . . . 6
|
4 | | cnq0 6385 |
. . . . . 6
Q0 |
5 | 3, 4 | wcel 1393 |
. . . . 5
Q0 |
6 | | vy |
. . . . . . 7
|
7 | 6 | cv 1242 |
. . . . . 6
|
8 | 7, 4 | wcel 1393 |
. . . . 5
Q0 |
9 | 5, 8 | wa 97 |
. . . 4
Q0
Q0 |
10 | | vw |
. . . . . . . . . . . . . 14
|
11 | 10 | cv 1242 |
. . . . . . . . . . . . 13
|
12 | | vv |
. . . . . . . . . . . . . 14
|
13 | 12 | cv 1242 |
. . . . . . . . . . . . 13
|
14 | 11, 13 | cop 3378 |
. . . . . . . . . . . 12
|
15 | | ceq0 6384 |
. . . . . . . . . . . 12
~Q0 |
16 | 14, 15 | cec 6104 |
. . . . . . . . . . 11
~Q0 |
17 | 3, 16 | wceq 1243 |
. . . . . . . . . 10
~Q0 |
18 | | vu |
. . . . . . . . . . . . . 14
|
19 | 18 | cv 1242 |
. . . . . . . . . . . . 13
|
20 | | vf |
. . . . . . . . . . . . . 14
|
21 | 20 | cv 1242 |
. . . . . . . . . . . . 13
|
22 | 19, 21 | cop 3378 |
. . . . . . . . . . . 12
|
23 | 22, 15 | cec 6104 |
. . . . . . . . . . 11
~Q0 |
24 | 7, 23 | wceq 1243 |
. . . . . . . . . 10
~Q0 |
25 | 17, 24 | wa 97 |
. . . . . . . . 9
~Q0 ~Q0 |
26 | | vz |
. . . . . . . . . . 11
|
27 | 26 | cv 1242 |
. . . . . . . . . 10
|
28 | | comu 5999 |
. . . . . . . . . . . . 13
|
29 | 11, 19, 28 | co 5512 |
. . . . . . . . . . . 12
|
30 | 13, 21, 28 | co 5512 |
. . . . . . . . . . . 12
|
31 | 29, 30 | cop 3378 |
. . . . . . . . . . 11
|
32 | 31, 15 | cec 6104 |
. . . . . . . . . 10
~Q0 |
33 | 27, 32 | wceq 1243 |
. . . . . . . . 9
~Q0 |
34 | 25, 33 | wa 97 |
. . . . . . . 8
~Q0 ~Q0 ~Q0 |
35 | 34, 20 | wex 1381 |
. . . . . . 7
~Q0
~Q0 ~Q0 |
36 | 35, 18 | wex 1381 |
. . . . . 6
~Q0 ~Q0 ~Q0 |
37 | 36, 12 | wex 1381 |
. . . . 5
~Q0
~Q0 ~Q0 |
38 | 37, 10 | wex 1381 |
. . . 4
~Q0 ~Q0 ~Q0 |
39 | 9, 38 | wa 97 |
. . 3
Q0
Q0
~Q0 ~Q0 ~Q0 |
40 | 39, 2, 6, 26 | coprab 5513 |
. 2
Q0
Q0
~Q0 ~Q0 ~Q0 |
41 | 1, 40 | wceq 1243 |
1
·Q0
Q0
Q0
~Q0 ~Q0 ~Q0 |