Detailed syntax breakdown of Definition df-ofs
Step | Hyp | Ref
| Expression |
1 | | cofs 30799 |
. 2
 |
2 | | vp |
. . . . . . . . . . . . . . 15
 |
3 | 2 | cv 1454 |
. . . . . . . . . . . . . 14
 |
4 | | va |
. . . . . . . . . . . . . . . . 17
 |
5 | 4 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
6 | | vb |
. . . . . . . . . . . . . . . . 17
 |
7 | 6 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
8 | 5, 7 | cop 3986 |
. . . . . . . . . . . . . . 15
    |
9 | | vc |
. . . . . . . . . . . . . . . . 17
 |
10 | 9 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
11 | | vd |
. . . . . . . . . . . . . . . . 17
 |
12 | 11 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
13 | 10, 12 | cop 3986 |
. . . . . . . . . . . . . . 15
    |
14 | 8, 13 | cop 3986 |
. . . . . . . . . . . . . 14
          |
15 | 3, 14 | wceq 1455 |
. . . . . . . . . . . . 13
    
     |
16 | | vq |
. . . . . . . . . . . . . . 15
 |
17 | 16 | cv 1454 |
. . . . . . . . . . . . . 14
 |
18 | | vx |
. . . . . . . . . . . . . . . . 17
 |
19 | 18 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
20 | | vy |
. . . . . . . . . . . . . . . . 17
 |
21 | 20 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
22 | 19, 21 | cop 3986 |
. . . . . . . . . . . . . . 15
    |
23 | | vz |
. . . . . . . . . . . . . . . . 17
 |
24 | 23 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
25 | | vw |
. . . . . . . . . . . . . . . . 17
 |
26 | 25 | cv 1454 |
. . . . . . . . . . . . . . . 16
 |
27 | 24, 26 | cop 3986 |
. . . . . . . . . . . . . . 15
    |
28 | 22, 27 | cop 3986 |
. . . . . . . . . . . . . 14
          |
29 | 17, 28 | wceq 1455 |
. . . . . . . . . . . . 13
    
     |
30 | 5, 10 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
31 | | cbtwn 24975 |
. . . . . . . . . . . . . . . 16
 |
32 | 7, 30, 31 | wbr 4418 |
. . . . . . . . . . . . . . 15
    |
33 | 19, 24 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
34 | 21, 33, 31 | wbr 4418 |
. . . . . . . . . . . . . . 15
    |
35 | 32, 34 | wa 375 |
. . . . . . . . . . . . . 14
         |
36 | | ccgr 24976 |
. . . . . . . . . . . . . . . 16
Cgr |
37 | 8, 22, 36 | wbr 4418 |
. . . . . . . . . . . . . . 15
   Cgr    |
38 | 7, 10 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
39 | 21, 24 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
40 | 38, 39, 36 | wbr 4418 |
. . . . . . . . . . . . . . 15
   Cgr    |
41 | 37, 40 | wa 375 |
. . . . . . . . . . . . . 14
    Cgr      Cgr     |
42 | 5, 12 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
43 | 19, 26 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
44 | 42, 43, 36 | wbr 4418 |
. . . . . . . . . . . . . . 15
   Cgr    |
45 | 7, 12 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
46 | 21, 26 | cop 3986 |
. . . . . . . . . . . . . . . 16
    |
47 | 45, 46, 36 | wbr 4418 |
. . . . . . . . . . . . . . 15
   Cgr    |
48 | 44, 47 | wa 375 |
. . . . . . . . . . . . . 14
    Cgr      Cgr     |
49 | 35, 41, 48 | w3a 991 |
. . . . . . . . . . . . 13
 
  
   
    Cgr      Cgr   
    Cgr      Cgr      |
50 | 15, 29, 49 | w3a 991 |
. . . . . . . . . . . 12
     
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
51 | | vn |
. . . . . . . . . . . . . 14
 |
52 | 51 | cv 1454 |
. . . . . . . . . . . . 13
 |
53 | | cee 24974 |
. . . . . . . . . . . . 13
 |
54 | 52, 53 | cfv 5605 |
. . . . . . . . . . . 12
     |
55 | 50, 25, 54 | wrex 2750 |
. . . . . . . . . . 11
           
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
56 | 55, 23, 54 | wrex 2750 |
. . . . . . . . . 10
                 
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
57 | 56, 20, 54 | wrex 2750 |
. . . . . . . . 9
                       
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
58 | 57, 18, 54 | wrex 2750 |
. . . . . . . 8
                             
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
59 | 58, 11, 54 | wrex 2750 |
. . . . . . 7
                                   
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
60 | 59, 9, 54 | wrex 2750 |
. . . . . 6
                                         
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
61 | 60, 6, 54 | wrex 2750 |
. . . . 5
                                               
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
62 | 61, 4, 54 | wrex 2750 |
. . . 4
                                                     
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
63 | | cn 10642 |
. . . 4
 |
64 | 62, 51, 63 | wrex 2750 |
. . 3
                                                      
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr       |
65 | 64, 2, 16 | copab 4476 |
. 2
    
                                                     
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr        |
66 | 1, 65 | wceq 1455 |
1
    
                                                     
   
    
   
 
  
   
    Cgr      Cgr   
    Cgr      Cgr        |