Detailed syntax breakdown of Definition df-trkgb
Step | Hyp | Ref
| Expression |
1 | | cstrkgb 24529 |
. 2
TarskiGB |
2 | | vy |
. . . . . . . . . . 11
 |
3 | 2 | cv 1454 |
. . . . . . . . . 10
 |
4 | | vx |
. . . . . . . . . . . 12
 |
5 | 4 | cv 1454 |
. . . . . . . . . . 11
 |
6 | | vi |
. . . . . . . . . . . 12
 |
7 | 6 | cv 1454 |
. . . . . . . . . . 11
 |
8 | 5, 5, 7 | co 6315 |
. . . . . . . . . 10
     |
9 | 3, 8 | wcel 1898 |
. . . . . . . . 9
     |
10 | 4, 2 | weq 1802 |
. . . . . . . . 9
 |
11 | 9, 10 | wi 4 |
. . . . . . . 8
       |
12 | | vp |
. . . . . . . . 9
 |
13 | 12 | cv 1454 |
. . . . . . . 8
 |
14 | 11, 2, 13 | wral 2749 |
. . . . . . 7

    
  |
15 | 14, 4, 13 | wral 2749 |
. . . . . 6


    
  |
16 | | vu |
. . . . . . . . . . . . . . 15
 |
17 | 16 | cv 1454 |
. . . . . . . . . . . . . 14
 |
18 | | vz |
. . . . . . . . . . . . . . . 16
 |
19 | 18 | cv 1454 |
. . . . . . . . . . . . . . 15
 |
20 | 5, 19, 7 | co 6315 |
. . . . . . . . . . . . . 14
     |
21 | 17, 20 | wcel 1898 |
. . . . . . . . . . . . 13
     |
22 | | vv |
. . . . . . . . . . . . . . 15
 |
23 | 22 | cv 1454 |
. . . . . . . . . . . . . 14
 |
24 | 3, 19, 7 | co 6315 |
. . . . . . . . . . . . . 14
     |
25 | 23, 24 | wcel 1898 |
. . . . . . . . . . . . 13
     |
26 | 21, 25 | wa 375 |
. . . . . . . . . . . 12
           |
27 | | va |
. . . . . . . . . . . . . . . 16
 |
28 | 27 | cv 1454 |
. . . . . . . . . . . . . . 15
 |
29 | 17, 3, 7 | co 6315 |
. . . . . . . . . . . . . . 15
     |
30 | 28, 29 | wcel 1898 |
. . . . . . . . . . . . . 14
     |
31 | 23, 5, 7 | co 6315 |
. . . . . . . . . . . . . . 15
     |
32 | 28, 31 | wcel 1898 |
. . . . . . . . . . . . . 14
     |
33 | 30, 32 | wa 375 |
. . . . . . . . . . . . 13
           |
34 | 33, 27, 13 | wrex 2750 |
. . . . . . . . . . . 12

           |
35 | 26, 34 | wi 4 |
. . . . . . . . . . 11
     
                  |
36 | 35, 22, 13 | wral 2749 |
. . . . . . . . . 10

     
                  |
37 | 36, 16, 13 | wral 2749 |
. . . . . . . . 9


     
                  |
38 | 37, 18, 13 | wral 2749 |
. . . . . . . 8



     
                  |
39 | 38, 2, 13 | wral 2749 |
. . . . . . 7




     
                  |
40 | 39, 4, 13 | wral 2749 |
. . . . . 6





     
                  |
41 | 28, 3, 7 | co 6315 |
. . . . . . . . . . . . 13
     |
42 | 5, 41 | wcel 1898 |
. . . . . . . . . . . 12
     |
43 | | vt |
. . . . . . . . . . . . 13
 |
44 | 43 | cv 1454 |
. . . . . . . . . . . 12
 |
45 | 42, 2, 44 | wral 2749 |
. . . . . . . . . . 11

     |
46 | | vs |
. . . . . . . . . . . 12
 |
47 | 46 | cv 1454 |
. . . . . . . . . . 11
 |
48 | 45, 4, 47 | wral 2749 |
. . . . . . . . . 10


     |
49 | 48, 27, 13 | wrex 2750 |
. . . . . . . . 9



     |
50 | | vb |
. . . . . . . . . . . . . 14
 |
51 | 50 | cv 1454 |
. . . . . . . . . . . . 13
 |
52 | 5, 3, 7 | co 6315 |
. . . . . . . . . . . . 13
     |
53 | 51, 52 | wcel 1898 |
. . . . . . . . . . . 12
     |
54 | 53, 2, 44 | wral 2749 |
. . . . . . . . . . 11

     |
55 | 54, 4, 47 | wral 2749 |
. . . . . . . . . 10


     |
56 | 55, 50, 13 | wrex 2750 |
. . . . . . . . 9



     |
57 | 49, 56 | wi 4 |
. . . . . . . 8
  

   



      |
58 | 13 | cpw 3963 |
. . . . . . . 8
  |
59 | 57, 43, 58 | wral 2749 |
. . . . . . 7
    

   



      |
60 | 59, 46, 58 | wral 2749 |
. . . . . 6
      

   



      |
61 | 15, 40, 60 | w3a 991 |
. . . . 5
 

    
  



           
             
  


   



       |
62 | | vf |
. . . . . . 7
 |
63 | 62 | cv 1454 |
. . . . . 6
 |
64 | | citv 24533 |
. . . . . 6
Itv |
65 | 63, 64 | cfv 5601 |
. . . . 5
Itv   |
66 | 61, 6, 65 | wsbc 3279 |
. . . 4
 Itv   ![]. ].](_drbrack.gif)        
 




          

             
  


   



       |
67 | | cbs 15170 |
. . . . 5
 |
68 | 63, 67 | cfv 5601 |
. . . 4
     |
69 | 66, 12, 68 | wsbc 3279 |
. . 3
      ![]. ].](_drbrack.gif)  Itv   ![]. ].](_drbrack.gif)        
 




          

             
  


   



       |
70 | 69, 62 | cab 2448 |
. 2
       ![]. ].](_drbrack.gif)  Itv   ![]. ].](_drbrack.gif)   
      




     
                 
 
  


   



        |
71 | 1, 70 | wceq 1455 |
1
TarskiGB
       ![]. ].](_drbrack.gif)  Itv   ![]. ].](_drbrack.gif)  

      




     
                 
 
  


   



        |