Detailed syntax breakdown of Definition df-ltnqqs
Step | Hyp | Ref
| Expression |
1 | | cltq 7236 |
. 2
|
2 | | vx |
. . . . . . 7
|
3 | 2 | cv 1347 |
. . . . . 6
|
4 | | cnq 7231 |
. . . . . 6
|
5 | 3, 4 | wcel 2141 |
. . . . 5
|
6 | | vy |
. . . . . . 7
|
7 | 6 | cv 1347 |
. . . . . 6
|
8 | 7, 4 | wcel 2141 |
. . . . 5
|
9 | 5, 8 | wa 103 |
. . . 4
|
10 | | vz |
. . . . . . . . . . . . . 14
|
11 | 10 | cv 1347 |
. . . . . . . . . . . . 13
|
12 | | vw |
. . . . . . . . . . . . . 14
|
13 | 12 | cv 1347 |
. . . . . . . . . . . . 13
|
14 | 11, 13 | cop 3584 |
. . . . . . . . . . . 12
|
15 | | ceq 7230 |
. . . . . . . . . . . 12
|
16 | 14, 15 | cec 6508 |
. . . . . . . . . . 11
|
17 | 3, 16 | wceq 1348 |
. . . . . . . . . 10
|
18 | | vv |
. . . . . . . . . . . . . 14
|
19 | 18 | cv 1347 |
. . . . . . . . . . . . 13
|
20 | | vu |
. . . . . . . . . . . . . 14
|
21 | 20 | cv 1347 |
. . . . . . . . . . . . 13
|
22 | 19, 21 | cop 3584 |
. . . . . . . . . . . 12
|
23 | 22, 15 | cec 6508 |
. . . . . . . . . . 11
|
24 | 7, 23 | wceq 1348 |
. . . . . . . . . 10
|
25 | 17, 24 | wa 103 |
. . . . . . . . 9
|
26 | | cmi 7225 |
. . . . . . . . . . 11
|
27 | 11, 21, 26 | co 5851 |
. . . . . . . . . 10
|
28 | 13, 19, 26 | co 5851 |
. . . . . . . . . 10
|
29 | | clti 7226 |
. . . . . . . . . 10
|
30 | 27, 28, 29 | wbr 3987 |
. . . . . . . . 9
|
31 | 25, 30 | wa 103 |
. . . . . . . 8
|
32 | 31, 20 | wex 1485 |
. . . . . . 7
|
33 | 32, 18 | wex 1485 |
. . . . . 6
|
34 | 33, 12 | wex 1485 |
. . . . 5
|
35 | 34, 10 | wex 1485 |
. . . 4
|
36 | 9, 35 | wa 103 |
. . 3
|
37 | 36, 2, 6 | copab 4047 |
. 2
|
38 | 1, 37 | wceq 1348 |
1
|