Detailed syntax breakdown of Definition df-nat
Step | Hyp | Ref
| Expression |
1 | | cnat 16601 |
. 2
Nat |
2 | | vt |
. . 3
 |
3 | | vu |
. . 3
 |
4 | | ccat 16325 |
. . 3
 |
5 | | vf |
. . . 4
 |
6 | | vg |
. . . 4
 |
7 | 2 | cv 1482 |
. . . . 5
 |
8 | 3 | cv 1482 |
. . . . 5
 |
9 | | cfunc 16514 |
. . . . 5
 |
10 | 7, 8, 9 | co 6650 |
. . . 4
   |
11 | | vr |
. . . . 5
 |
12 | 5 | cv 1482 |
. . . . . 6
 |
13 | | c1st 7166 |
. . . . . 6
 |
14 | 12, 13 | cfv 5888 |
. . . . 5
     |
15 | | vs |
. . . . . 6
 |
16 | 6 | cv 1482 |
. . . . . . 7
 |
17 | 16, 13 | cfv 5888 |
. . . . . 6
     |
18 | | vy |
. . . . . . . . . . . . . 14
 |
19 | 18 | cv 1482 |
. . . . . . . . . . . . 13
 |
20 | | va |
. . . . . . . . . . . . . 14
 |
21 | 20 | cv 1482 |
. . . . . . . . . . . . 13
 |
22 | 19, 21 | cfv 5888 |
. . . . . . . . . . . 12
     |
23 | | vh |
. . . . . . . . . . . . . 14
 |
24 | 23 | cv 1482 |
. . . . . . . . . . . . 13
 |
25 | | vx |
. . . . . . . . . . . . . . 15
 |
26 | 25 | cv 1482 |
. . . . . . . . . . . . . 14
 |
27 | | c2nd 7167 |
. . . . . . . . . . . . . . 15
 |
28 | 12, 27 | cfv 5888 |
. . . . . . . . . . . . . 14
     |
29 | 26, 19, 28 | co 6650 |
. . . . . . . . . . . . 13
         |
30 | 24, 29 | cfv 5888 |
. . . . . . . . . . . 12
             |
31 | 11 | cv 1482 |
. . . . . . . . . . . . . . 15
 |
32 | 26, 31 | cfv 5888 |
. . . . . . . . . . . . . 14
     |
33 | 19, 31 | cfv 5888 |
. . . . . . . . . . . . . 14
     |
34 | 32, 33 | cop 4183 |
. . . . . . . . . . . . 13
            |
35 | 15 | cv 1482 |
. . . . . . . . . . . . . 14
 |
36 | 19, 35 | cfv 5888 |
. . . . . . . . . . . . 13
     |
37 | | cco 15953 |
. . . . . . . . . . . . . 14
comp |
38 | 8, 37 | cfv 5888 |
. . . . . . . . . . . . 13
comp   |
39 | 34, 36, 38 | co 6650 |
. . . . . . . . . . . 12
             comp         |
40 | 22, 30, 39 | co 6650 |
. . . . . . . . . . 11
                   comp                       |
41 | 16, 27 | cfv 5888 |
. . . . . . . . . . . . . 14
     |
42 | 26, 19, 41 | co 6650 |
. . . . . . . . . . . . 13
         |
43 | 24, 42 | cfv 5888 |
. . . . . . . . . . . 12
             |
44 | 26, 21 | cfv 5888 |
. . . . . . . . . . . 12
     |
45 | 26, 35 | cfv 5888 |
. . . . . . . . . . . . . 14
     |
46 | 32, 45 | cop 4183 |
. . . . . . . . . . . . 13
            |
47 | 46, 36, 38 | co 6650 |
. . . . . . . . . . . 12
             comp         |
48 | 43, 44, 47 | co 6650 |
. . . . . . . . . . 11
                           comp               |
49 | 40, 48 | wceq 1483 |
. . . . . . . . . 10
                   comp                                                 comp               |
50 | | chom 15952 |
. . . . . . . . . . . 12
 |
51 | 7, 50 | cfv 5888 |
. . . . . . . . . . 11
    |
52 | 26, 19, 51 | co 6650 |
. . . . . . . . . 10
        |
53 | 49, 23, 52 | wral 2912 |
. . . . . . . . 9
                            comp                                                 comp               |
54 | | cbs 15857 |
. . . . . . . . . 10
 |
55 | 7, 54 | cfv 5888 |
. . . . . . . . 9
     |
56 | 53, 18, 55 | wral 2912 |
. . . . . . . 8
                                  comp                                                 comp               |
57 | 56, 25, 55 | wral 2912 |
. . . . . . 7
                                        comp                                                 comp               |
58 | 8, 50 | cfv 5888 |
. . . . . . . . 9
    |
59 | 32, 45, 58 | co 6650 |
. . . . . . . 8
                |
60 | 25, 55, 59 | cixp 7908 |
. . . . . . 7
                      |
61 | 57, 20, 60 | crab 2916 |
. . . . . 6
                                                              comp                                                 comp                |
62 | 15, 17, 61 | csb 3533 |
. . . . 5
      ![]_ ]_](_urbrack.gif)  
                          
     
  
                        comp                                                 comp                |
63 | 11, 14, 62 | csb 3533 |
. . . 4
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
                          
     
  
                        comp                                                 comp                |
64 | 5, 6, 10, 10, 63 | cmpt2 6652 |
. . 3
            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
                          
     
  
                        comp                                                 comp                 |
65 | 2, 3, 4, 4, 64 | cmpt2 6652 |
. 2
              ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
                          
     
  
                        comp                                                 comp                  |
66 | 1, 65 | wceq 1483 |
1
Nat  
            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
                          
     
  
                        comp                                                 comp                  |