Detailed syntax breakdown of Definition df-dih
Step | Hyp | Ref
| Expression |
1 | | cdih 34840 |
. 2
 |
2 | | vk |
. . 3
 |
3 | | cvv 3056 |
. . 3
 |
4 | | vw |
. . . 4
 |
5 | 2 | cv 1453 |
. . . . 5
 |
6 | | clh 33593 |
. . . . 5
 |
7 | 5, 6 | cfv 5600 |
. . . 4
     |
8 | | vx |
. . . . 5
 |
9 | | cbs 15169 |
. . . . . 6
 |
10 | 5, 9 | cfv 5600 |
. . . . 5
     |
11 | 8 | cv 1453 |
. . . . . . 7
 |
12 | 4 | cv 1453 |
. . . . . . 7
 |
13 | | cple 15245 |
. . . . . . . 8
 |
14 | 5, 13 | cfv 5600 |
. . . . . . 7
     |
15 | 11, 12, 14 | wbr 4415 |
. . . . . 6
       |
16 | | cdib 34750 |
. . . . . . . . 9
 |
17 | 5, 16 | cfv 5600 |
. . . . . . . 8
     |
18 | 12, 17 | cfv 5600 |
. . . . . . 7
         |
19 | 11, 18 | cfv 5600 |
. . . . . 6
             |
20 | | vq |
. . . . . . . . . . . . 13
 |
21 | 20 | cv 1453 |
. . . . . . . . . . . 12
 |
22 | 21, 12, 14 | wbr 4415 |
. . . . . . . . . . 11
       |
23 | 22 | wn 3 |
. . . . . . . . . 10
       |
24 | | cmee 16238 |
. . . . . . . . . . . . . 14
 |
25 | 5, 24 | cfv 5600 |
. . . . . . . . . . . . 13
     |
26 | 11, 12, 25 | co 6314 |
. . . . . . . . . . . 12
         |
27 | | cjn 16237 |
. . . . . . . . . . . . 13
 |
28 | 5, 27 | cfv 5600 |
. . . . . . . . . . . 12
     |
29 | 21, 26, 28 | co 6314 |
. . . . . . . . . . 11
                 |
30 | 29, 11 | wceq 1454 |
. . . . . . . . . 10
                 |
31 | 23, 30 | wa 375 |
. . . . . . . . 9
                         |
32 | | vu |
. . . . . . . . . . 11
 |
33 | 32 | cv 1453 |
. . . . . . . . . 10
 |
34 | | cdic 34784 |
. . . . . . . . . . . . . 14
 |
35 | 5, 34 | cfv 5600 |
. . . . . . . . . . . . 13
     |
36 | 12, 35 | cfv 5600 |
. . . . . . . . . . . 12
         |
37 | 21, 36 | cfv 5600 |
. . . . . . . . . . 11
             |
38 | 26, 18 | cfv 5600 |
. . . . . . . . . . 11
                     |
39 | | cdvh 34690 |
. . . . . . . . . . . . . 14
 |
40 | 5, 39 | cfv 5600 |
. . . . . . . . . . . . 13
     |
41 | 12, 40 | cfv 5600 |
. . . . . . . . . . . 12
         |
42 | | clsm 17334 |
. . . . . . . . . . . 12
 |
43 | 41, 42 | cfv 5600 |
. . . . . . . . . . 11
             |
44 | 37, 38, 43 | co 6314 |
. . . . . . . . . 10
                                                 |
45 | 33, 44 | wceq 1454 |
. . . . . . . . 9
                                                 |
46 | 31, 45 | wi 4 |
. . . . . . . 8
                                                                           |
47 | | catm 32873 |
. . . . . . . . 9
 |
48 | 5, 47 | cfv 5600 |
. . . . . . . 8
     |
49 | 46, 20, 48 | wral 2748 |
. . . . . . 7
                                                                                 |
50 | | clss 18203 |
. . . . . . . 8
 |
51 | 41, 50 | cfv 5600 |
. . . . . . 7
             |
52 | 49, 32, 51 | crio 6275 |
. . . . . 6
               
                                                                                 |
53 | 15, 19, 52 | cif 3892 |
. . . . 5
                                     
                                                                                  |
54 | 8, 10, 53 | cmpt 4474 |
. . . 4
                            
                                                                                                 |
55 | 4, 7, 54 | cmpt 4474 |
. . 3
                                 
                                                                                                  |
56 | 2, 3, 55 | cmpt 4474 |
. 2
                                  
                                                                                                   |
57 | 1, 56 | wceq 1454 |
1
                                  
                                                                                                   |