Detailed syntax breakdown of Definition df-limced
Step | Hyp | Ref
| Expression |
1 | | climc 13119 |
. 2
lim |
2 | | vf |
. . 3
|
3 | | vx |
. . 3
|
4 | | cc 7733 |
. . . 4
|
5 | | cpm 6597 |
. . . 4
|
6 | 4, 4, 5 | co 5827 |
. . 3
|
7 | 2 | cv 1334 |
. . . . . . . 8
|
8 | 7 | cdm 4589 |
. . . . . . 7
|
9 | 8, 4, 7 | wf 5169 |
. . . . . 6
|
10 | 8, 4 | wss 3102 |
. . . . . 6
|
11 | 9, 10 | wa 103 |
. . . . 5
|
12 | 3 | cv 1334 |
. . . . . . 7
|
13 | 12, 4 | wcel 2128 |
. . . . . 6
|
14 | | vz |
. . . . . . . . . . . . 13
|
15 | 14 | cv 1334 |
. . . . . . . . . . . 12
|
16 | | cap 8461 |
. . . . . . . . . . . 12
# |
17 | 15, 12, 16 | wbr 3967 |
. . . . . . . . . . 11
# |
18 | | cmin 8051 |
. . . . . . . . . . . . . 14
|
19 | 15, 12, 18 | co 5827 |
. . . . . . . . . . . . 13
|
20 | | cabs 10909 |
. . . . . . . . . . . . 13
|
21 | 19, 20 | cfv 5173 |
. . . . . . . . . . . 12
|
22 | | vd |
. . . . . . . . . . . . 13
|
23 | 22 | cv 1334 |
. . . . . . . . . . . 12
|
24 | | clt 7915 |
. . . . . . . . . . . 12
|
25 | 21, 23, 24 | wbr 3967 |
. . . . . . . . . . 11
|
26 | 17, 25 | wa 103 |
. . . . . . . . . 10
# |
27 | 15, 7 | cfv 5173 |
. . . . . . . . . . . . 13
|
28 | | vy |
. . . . . . . . . . . . . 14
|
29 | 28 | cv 1334 |
. . . . . . . . . . . . 13
|
30 | 27, 29, 18 | co 5827 |
. . . . . . . . . . . 12
|
31 | 30, 20 | cfv 5173 |
. . . . . . . . . . 11
|
32 | | ve |
. . . . . . . . . . . 12
|
33 | 32 | cv 1334 |
. . . . . . . . . . 11
|
34 | 31, 33, 24 | wbr 3967 |
. . . . . . . . . 10
|
35 | 26, 34 | wi 4 |
. . . . . . . . 9
# |
36 | 35, 14, 8 | wral 2435 |
. . . . . . . 8
# |
37 | | crp 9567 |
. . . . . . . 8
|
38 | 36, 22, 37 | wrex 2436 |
. . . . . . 7
# |
39 | 38, 32, 37 | wral 2435 |
. . . . . 6
#
|
40 | 13, 39 | wa 103 |
. . . . 5
# |
41 | 11, 40 | wa 103 |
. . . 4
# |
42 | 41, 28, 4 | crab 2439 |
. . 3
# |
43 | 2, 3, 6, 4, 42 | cmpo 5829 |
. 2
# |
44 | 1, 43 | wceq 1335 |
1
lim
# |