Step | Hyp | Ref
| Expression |
1 | | f1otrg.h |
. . . . . 6
   |
2 | | elex 3040 |
. . . . . 6
   |
3 | 1, 2 | syl 17 |
. . . . 5
   |
4 | | f1otrkg.p |
. . . . . . . . 9
     |
5 | | f1otrkg.d |
. . . . . . . . 9
     |
6 | | f1otrkg.i |
. . . . . . . . 9
Itv   |
7 | | f1otrg.g |
. . . . . . . . . 10

TarskiG |
8 | 7 | adantr 472 |
. . . . . . . . 9
 

 
TarskiG |
9 | | f1otrkg.f |
. . . . . . . . . . . 12
       |
10 | | f1of 5828 |
. . . . . . . . . . . 12
    
      |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
       |
12 | 11 | adantr 472 |
. . . . . . . . . 10
 

        |
13 | | simprl 772 |
. . . . . . . . . 10
 

 
  |
14 | 12, 13 | ffvelrnd 6038 |
. . . . . . . . 9
 

        |
15 | | simprr 774 |
. . . . . . . . . 10
 

    |
16 | 12, 15 | ffvelrnd 6038 |
. . . . . . . . 9
 

        |
17 | 4, 5, 6, 8, 14, 16 | axtgcgrrflx 24589 |
. . . . . . . 8
 

                            |
18 | | f1otrkg.b |
. . . . . . . . 9
     |
19 | | f1otrkg.e |
. . . . . . . . 9
     |
20 | | f1otrkg.j |
. . . . . . . . 9
Itv   |
21 | 9 | adantr 472 |
. . . . . . . . 9
 

        |
22 | | f1otrkg.1 |
. . . . . . . . . 10
 

                    |
23 | 22 | adantlr 729 |
. . . . . . . . 9
   
 

                    |
24 | | f1otrkg.2 |
. . . . . . . . . 10
 

                          |
25 | 24 | adantlr 729 |
. . . . . . . . 9
   
 

                          |
26 | 4, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15 | f1otrgds 24978 |
. . . . . . . 8
 

                    |
27 | 4, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13 | f1otrgds 24978 |
. . . . . . . 8
 

                    |
28 | 17, 26, 27 | 3eqtr4d 2515 |
. . . . . . 7
 

            |
29 | 28 | ralrimivva 2814 |
. . . . . 6
  
          |
30 | | f1of1 5827 |
. . . . . . . . . . 11
    
      |
31 | 9, 30 | syl 17 |
. . . . . . . . . 10
       |
32 | 31 | 3ad2ant1 1051 |
. . . . . . . . 9
 

                |
33 | | simp21 1063 |
. . . . . . . . . 10
 

         
  |
34 | | simp22 1064 |
. . . . . . . . . 10
 

            |
35 | 33, 34 | jca 541 |
. . . . . . . . 9
 

          
   |
36 | 7 | 3ad2ant1 1051 |
. . . . . . . . . 10
 

         
TarskiG |
37 | 11 | 3ad2ant1 1051 |
. . . . . . . . . . 11
 

                |
38 | 37, 33 | ffvelrnd 6038 |
. . . . . . . . . 10
 

                |
39 | 37, 34 | ffvelrnd 6038 |
. . . . . . . . . 10
 

                |
40 | | simp23 1065 |
. . . . . . . . . . 11
 

            |
41 | 37, 40 | ffvelrnd 6038 |
. . . . . . . . . 10
 

                |
42 | | simp3 1032 |
. . . . . . . . . . 11
 

                    |
43 | 9 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
 

                |
44 | 22 | 3ad2antl1 1192 |
. . . . . . . . . . . 12
   
                               |
45 | 24 | 3ad2antl1 1192 |
. . . . . . . . . . . 12
   
                                     |
46 | 4, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34 | f1otrgds 24978 |
. . . . . . . . . . 11
 

                            |
47 | 4, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40 | f1otrgds 24978 |
. . . . . . . . . . 11
 

                            |
48 | 42, 46, 47 | 3eqtr3d 2513 |
. . . . . . . . . 10
 

                                    |
49 | 4, 5, 6, 36, 38, 39, 41, 48 | axtgcgrid 24590 |
. . . . . . . . 9
 

                    |
50 | | f1veqaeq 6179 |
. . . . . . . . . 10
      
          
   |
51 | 50 | imp 436 |
. . . . . . . . 9
                  
  |
52 | 32, 35, 49, 51 | syl21anc 1291 |
. . . . . . . 8
 

         
  |
53 | 52 | 3expia 1233 |
. . . . . . 7
 

              |
54 | 53 | ralrimivvva 2815 |
. . . . . 6
  

            |
55 | 29, 54 | jca 541 |
. . . . 5
                       
    |
56 | 18, 19, 20 | istrkgc 24581 |
. . . . 5
 TarskiGC    
         

        
     |
57 | 3, 55, 56 | sylanbrc 677 |
. . . 4

TarskiGC |
58 | 9 | 3ad2ant1 1051 |
. . . . . . . . . 10
 

            |
59 | 58, 30 | syl 17 |
. . . . . . . . 9
 

            |
60 | | simp2 1031 |
. . . . . . . . 9
 

      
   |
61 | 7 | 3ad2ant1 1051 |
. . . . . . . . . 10
 

      TarskiG |
62 | 14 | 3adant3 1050 |
. . . . . . . . . 10
 

            |
63 | 16 | 3adant3 1050 |
. . . . . . . . . 10
 

            |
64 | | simp3 1032 |
. . . . . . . . . . 11
 

            |
65 | 22 | 3ad2antl1 1192 |
. . . . . . . . . . . 12
   

                          |
66 | 24 | 3ad2antl1 1192 |
. . . . . . . . . . . 12
   

     
                          |
67 | 13 | 3adant3 1050 |
. . . . . . . . . . . 12
 

        |
68 | 15 | 3adant3 1050 |
. . . . . . . . . . . 12
 

        |
69 | 4, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68 | f1otrgitv 24979 |
. . . . . . . . . . 11
 

          
                   |
70 | 64, 69 | mpbid 215 |
. . . . . . . . . 10
 

                        |
71 | 4, 5, 6, 61, 62, 63, 70 | axtgbtwnid 24593 |
. . . . . . . . 9
 

                |
72 | 59, 60, 71, 51 | syl21anc 1291 |
. . . . . . . 8
 

        |
73 | 72 | 3expia 1233 |
. . . . . . 7
 

          |
74 | 73 | ralrimivva 2814 |
. . . . . 6
  
        |
75 | | f1ocnv 5840 |
. . . . . . . . . . . . . 14
    
       |
76 | | f1of 5828 |
. . . . . . . . . . . . . 14
             |
77 | 9, 75, 76 | 3syl 18 |
. . . . . . . . . . . . 13
        |
78 | 77 | ad5antr 748 |
. . . . . . . . . . . 12
     

  
      
                   
             
       |
79 | | simplr 770 |
. . . . . . . . . . . 12
     

  
      
                   
             
  |
80 | 78, 79 | ffvelrnd 6038 |
. . . . . . . . . . 11
     

  
      
                   
             
       |
81 | | simpr 468 |
. . . . . . . . . . . . 13
       
 

  
                       
                           |
82 | 81 | eleq1d 2533 |
. . . . . . . . . . . 12
       
 

  
                       
                                     |
83 | 81 | eleq1d 2533 |
. . . . . . . . . . . 12
       
 

  
                       
                                     |
84 | 82, 83 | anbi12d 725 |
. . . . . . . . . . 11
       
 

  
                       
                              
                       |
85 | | simprl 772 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
              |
86 | 21 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
    
  
 
                 |
87 | 86 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
     

  
      
                   
             
      |
88 | | f1ocnvfv2 6194 |
. . . . . . . . . . . . . . . 16
     
            |
89 | 88 | eleq1d 2533 |
. . . . . . . . . . . . . . 15
     
                      
               |
90 | 87, 79, 89 | syl2anc 673 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
                     
               |
91 | 85, 90 | mpbird 240 |
. . . . . . . . . . . . 13
     

  
      
                   
             
                       |
92 | | simplll 776 |
. . . . . . . . . . . . . . 15
       
 

  
                       
                    
  
 
             |
93 | | simplll 776 |
. . . . . . . . . . . . . . . 16
     
  
 
           
        |
94 | 93, 23 | sylancom 680 |
. . . . . . . . . . . . . . 15
     
  
 
           
                    |
95 | 92, 94 | sylancom 680 |
. . . . . . . . . . . . . 14
       
 

  
                       
                                   |
96 | | simplll 776 |
. . . . . . . . . . . . . . 15
       
 

  
                       
              
     
  
 
             |
97 | | simplll 776 |
. . . . . . . . . . . . . . . 16
     
  
 
           
        |
98 | 97, 25 | sylancom 680 |
. . . . . . . . . . . . . . 15
     
  
 
           
      
                   |
99 | 96, 98 | sylancom 680 |
. . . . . . . . . . . . . 14
       
 

  
                       
              
                          |
100 | | simplr2 1073 |
. . . . . . . . . . . . . . 15
    
  
 
          
  |
101 | 100 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
  |
102 | 15 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
    
  
 
             |
103 | 102 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
  |
104 | 4, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80 | f1otrgitv 24979 |
. . . . . . . . . . . . 13
     

  
      
                   
             
         
                        |
105 | 91, 104 | mpbird 240 |
. . . . . . . . . . . 12
     

  
      
                   
             
           |
106 | | simprr 774 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
              |
107 | 88 | eleq1d 2533 |
. . . . . . . . . . . . . . 15
     
                      
               |
108 | 87, 79, 107 | syl2anc 673 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
                     
               |
109 | 106, 108 | mpbird 240 |
. . . . . . . . . . . . 13
     

  
      
                   
             
                       |
110 | | simplr3 1074 |
. . . . . . . . . . . . . . 15
    
  
 
             |
111 | 110 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
  |
112 | 13 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
    
  
 
          
  |
113 | 112 | ad2antrr 740 |
. . . . . . . . . . . . . 14
     

  
      
                   
             
  |
114 | 4, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80 | f1otrgitv 24979 |
. . . . . . . . . . . . 13
     

  
      
                   
             
         
                        |
115 | 109, 114 | mpbird 240 |
. . . . . . . . . . . 12
     

  
      
                   
             
           |
116 | 105, 115 | jca 541 |
. . . . . . . . . . 11
     

  
      
                   
             
                      |
117 | 80, 84, 116 | rspcedvd 3143 |
. . . . . . . . . 10
     

  
      
                   
             

            |
118 | 8 | ad2antrr 740 |
. . . . . . . . . . 11
    
  
 
          
TarskiG |
119 | 12 | ad2antrr 740 |
. . . . . . . . . . . 12
    
  
 
                 |
120 | 119, 112 | ffvelrnd 6038 |
. . . . . . . . . . 11
    
  
 
                 |
121 | 119, 102 | ffvelrnd 6038 |
. . . . . . . . . . 11
    
  
 
                 |
122 | | simplr1 1072 |
. . . . . . . . . . . 12
    
  
 
             |
123 | 119, 122 | ffvelrnd 6038 |
. . . . . . . . . . 11
    
  
 
                 |
124 | 119, 100 | ffvelrnd 6038 |
. . . . . . . . . . 11
    
  
 
                 |
125 | 119, 110 | ffvelrnd 6038 |
. . . . . . . . . . 11
    
  
 
                 |
126 | | simprl 772 |
. . . . . . . . . . . 12
    
  
 
          
      |
127 | 4, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100 | f1otrgitv 24979 |
. . . . . . . . . . . 12
    
  
 
                                   |
128 | 126, 127 | mpbid 215 |
. . . . . . . . . . 11
    
  
 
                             |
129 | | simprr 774 |
. . . . . . . . . . . 12
    
  
 
                 |
130 | 4, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110 | f1otrgitv 24979 |
. . . . . . . . . . . 12
    
  
 
                                   |
131 | 129, 130 | mpbid 215 |
. . . . . . . . . . 11
    
  
 
                             |
132 | 4, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131 | axtgpasch 24594 |
. . . . . . . . . 10
    
  
 
           
                            |
133 | 117, 132 | r19.29a 2918 |
. . . . . . . . 9
    
  
 
           
            |
134 | 133 | ex 441 |
. . . . . . . 8
   
 

             
             |
135 | 134 | ralrimivvva 2815 |
. . . . . . 7
 

  


           
             |
136 | 135 | ralrimivva 2814 |
. . . . . 6
  



           
             |
137 | 9 | ad5antr 748 |
. . . . . . . . . . . . . . . 16
     
     
 
                         |
138 | | simpllr 777 |
. . . . . . . . . . . . . . . 16
     
     
 
                     |
139 | 137, 138,
88 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     
     
 
                              |
140 | | ffn 5739 |
. . . . . . . . . . . . . . . . . 18
    
  |
141 | 137, 10, 140 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
     
     
 
                  
  |
142 | | simp-4r 785 |
. . . . . . . . . . . . . . . . . . . 20
         



        |
143 | 142 | simpld 466 |
. . . . . . . . . . . . . . . . . . 19
         



     |
144 | 143 | elpwid 3952 |
. . . . . . . . . . . . . . . . . 18
         



 
  |
145 | 144 | adantlr 729 |
. . . . . . . . . . . . . . . . 17
     
     
 
                  
  |
146 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
     
     
 
                  
  |
147 | | fnfvima 6161 |
. . . . . . . . . . . . . . . . 17
             |
148 | 141, 145,
146, 147 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
     
     
 
                             |
149 | 142 | simprd 470 |
. . . . . . . . . . . . . . . . . . 19
         



     |
150 | 149 | elpwid 3952 |
. . . . . . . . . . . . . . . . . 18
         



 
  |
151 | 150 | adantlr 729 |
. . . . . . . . . . . . . . . . 17
     
     
 
                  
  |
152 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
     
     
 
                     |
153 | | fnfvima 6161 |
. . . . . . . . . . . . . . . . 17
             |
154 | 141, 151,
152, 153 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
     
     
 
                             |
155 | | simplr 770 |
. . . . . . . . . . . . . . . 16
     
     
 
                   
     
           |
156 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
                   |
157 | 156 | eleq2d 2534 |
. . . . . . . . . . . . . . . . 17
         
           |
158 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                           |
159 | 158 | eleq2d 2534 |
. . . . . . . . . . . . . . . . 17
             
               |
160 | 157, 159 | rspc2va 3148 |
. . . . . . . . . . . . . . . 16
                                    
              |
161 | 148, 154,
155, 160 | syl21anc 1291 |
. . . . . . . . . . . . . . 15
     
     
 
                                 |
162 | 139, 161 | eqeltrd 2549 |
. . . . . . . . . . . . . 14
     
     
 
                                          |
163 | 9 | ad4antr 746 |
. . . . . . . . . . . . . . . 16
         



        |
164 | | simp-5l 786 |
. . . . . . . . . . . . . . . . 17
     
     
 
 

    |
165 | 164, 22 | sylancom 680 |
. . . . . . . . . . . . . . . 16
     
     
 
 

                    |
166 | | simp-5l 786 |
. . . . . . . . . . . . . . . . 17
     
     
 
 

    |
167 | 166, 24 | sylancom 680 |
. . . . . . . . . . . . . . . 16
     
     
 
 

                          |
168 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
         



 
  |
169 | 144, 168 | sseldd 3419 |
. . . . . . . . . . . . . . . 16
         



 
  |
170 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
         



    |
171 | 150, 170 | sseldd 3419 |
. . . . . . . . . . . . . . . 16
         



    |
172 | 77 | ad4antr 746 |
. . . . . . . . . . . . . . . . 17
         



         |
173 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
         



    |
174 | 172, 173 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . 16
         



         |
175 | 4, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174 | f1otrgitv 24979 |
. . . . . . . . . . . . . . 15
         



                                    |
176 | 175 | adantlr 729 |
. . . . . . . . . . . . . 14
     
     
 
                                                     |
177 | 162, 176 | mpbird 240 |
. . . . . . . . . . . . 13
     
     
 
                              |
178 | 177 | ralrimivva 2814 |
. . . . . . . . . . . 12
         


                


           |
179 | 178 | adantllr 733 |
. . . . . . . . . . 11
     
     


      
               


           |
180 | 77 | ad4antr 746 |
. . . . . . . . . . . . . 14
         
        
       |
181 | | simpr 468 |
. . . . . . . . . . . . . 14
         
        
  |
182 | 180, 181 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
         
        
       |
183 | | eleq1 2537 |
. . . . . . . . . . . . . . 15
          
            |
184 | 183 | 2ralbidv 2832 |
. . . . . . . . . . . . . 14
       

   


            |
185 | 184 | adantl 473 |
. . . . . . . . . . . . 13
     
     


                   

            |
186 | 182, 185 | rspcedv 3140 |
. . . . . . . . . . . 12
         
        
 

         


       |
187 | 186 | adantr 472 |
. . . . . . . . . . 11
     
     


      
               
 

         


       |
188 | 179, 187 | mpd 15 |
. . . . . . . . . 10
     
     


      
               



      |
189 | 7 | ad3antrrr 744 |
. . . . . . . . . . 11
        
        TarskiG |
190 | | imassrn 5185 |
. . . . . . . . . . . 12
     |
191 | | f1ofo 5835 |
. . . . . . . . . . . . . 14
    
      |
192 | | forn 5809 |
. . . . . . . . . . . . . 14
       |
193 | 9, 191, 192 | 3syl 18 |
. . . . . . . . . . . . 13
   |
194 | 193 | ad3antrrr 744 |
. . . . . . . . . . . 12
        
       
  |
195 | 190, 194 | syl5sseq 3466 |
. . . . . . . . . . 11
        
              |
196 | | imassrn 5185 |
. . . . . . . . . . . 12
     |
197 | 196, 194 | syl5sseq 3466 |
. . . . . . . . . . 11
        
              |
198 | 11 | ad3antrrr 744 |
. . . . . . . . . . . 12
        
              |
199 | | simplr 770 |
. . . . . . . . . . . 12
        
          |
200 | 198, 199 | ffvelrnd 6038 |
. . . . . . . . . . 11
        
              |
201 | 9 | ad5antr 748 |
. . . . . . . . . . . . . . . . . 18
     
     


                     |
202 | | ffn 5739 |
. . . . . . . . . . . . . . . . . 18
      
  |
203 | 201, 75, 76, 202 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
     
     


               
  |
204 | 195 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
     
     


                     |
205 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
     
     


                     |
206 | | fnfvima 6161 |
. . . . . . . . . . . . . . . . 17
  
   
                     |
207 | 203, 204,
205, 206 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
     
     


                               |
208 | 201, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
     
     


                     |
209 | | simp-5r 787 |
. . . . . . . . . . . . . . . . . . 19
     
     


                
    |
210 | 209 | simpld 466 |
. . . . . . . . . . . . . . . . . 18
     
     


                  |
211 | 210 | elpwid 3952 |
. . . . . . . . . . . . . . . . 17
     
     


                 |
212 | | f1imacnv 5844 |
. . . . . . . . . . . . . . . . 17
     
            |
213 | 208, 211,
212 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
     
     


                          |
214 | 207, 213 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
     
     


                      |
215 | 197 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
     
     


                     |
216 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
     
     


                     |
217 | | fnfvima 6161 |
. . . . . . . . . . . . . . . . 17
  
   
                     |
218 | 203, 215,
216, 217 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
     
     


                               |
219 | 209 | simprd 470 |
. . . . . . . . . . . . . . . . . 18
     
     


                  |
220 | 219 | elpwid 3952 |
. . . . . . . . . . . . . . . . 17
     
     


                 |
221 | | f1imacnv 5844 |
. . . . . . . . . . . . . . . . 17
     
            |
222 | 208, 220,
221 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
     
     


                          |
223 | 218, 222 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
     
     


                      |
224 | | simpllr 777 |
. . . . . . . . . . . . . . 15
     
     


               

      |
225 | | eleq1 2537 |
. . . . . . . . . . . . . . . 16
          
            |
226 | | oveq2 6316 |
. . . . . . . . . . . . . . . . 17
                     |
227 | 226 | eleq2d 2534 |
. . . . . . . . . . . . . . . 16
                                 |
228 | 225, 227 | rspc2va 3148 |
. . . . . . . . . . . . . . 15
              

                     |
229 | 214, 223,
224, 228 | syl21anc 1291 |
. . . . . . . . . . . . . 14
     
     


                               |
230 | | simp-6l 788 |
. . . . . . . . . . . . . . . 16
        
  
                  
 
  |
231 | 230, 22 | sylancom 680 |
. . . . . . . . . . . . . . 15
        
  
                  
 
                  |
232 | | simp-6l 788 |
. . . . . . . . . . . . . . . 16
        
  
                  
 
  |
233 | 232, 24 | sylancom 680 |
. . . . . . . . . . . . . . 15
        
  
                  
 
                        |
234 | | simp-4r 785 |
. . . . . . . . . . . . . . 15
     
     


                 |
235 | 215, 216 | sseldd 3419 |
. . . . . . . . . . . . . . . 16
     
     


                 |
236 | | f1ocnvdm 6201 |
. . . . . . . . . . . . . . . 16
     
        |
237 | 201, 235,
236 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     
     


                      |
238 | 204, 205 | sseldd 3419 |
. . . . . . . . . . . . . . . 16
     
     


                 |
239 | | f1ocnvdm 6201 |
. . . . . . . . . . . . . . . 16
     
        |
240 | 201, 238,
239 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     
     


                      |
241 | 4, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240 | f1otrgitv 24979 |
. . . . . . . . . . . . . 14
     
     


                                                           |
242 | 229, 241 | mpbid 215 |
. . . . . . . . . . . . 13
     
     


                                           |
243 | | f1ocnvfv2 6194 |
. . . . . . . . . . . . . 14
     
            |
244 | 201, 238,
243 | syl2anc 673 |
. . . . . . . . . . . . 13
     
     


                          |
245 | | f1ocnvfv2 6194 |
. . . . . . . . . . . . . . 15
     
            |
246 | 201, 235,
245 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
     


                          |
247 | 246 | oveq2d 6324 |
. . . . . . . . . . . . 13
     
     


                                          |
248 | 242, 244,
247 | 3eltr3d 2563 |
. . . . . . . . . . . 12
     
     


                         |
249 | 248 | 3impa 1226 |
. . . . . . . . . . 11
         
                
          |
250 | 4, 5, 6, 189, 195, 197, 200, 249 | axtgcont 24596 |
. . . . . . . . . 10
        
         
     
           |
251 | 188, 250 | r19.29a 2918 |
. . . . . . . . 9
        
         

      |
252 | 251 | r19.29an 2917 |
. . . . . . . 8
    
    

     


      |
253 | 252 | ex 441 |
. . . . . . 7
 
      


   



       |
254 | 253 | ralrimivva 2814 |
. . . . . 6
      


   



       |
255 | 74, 136, 254 | 3jca 1210 |
. . . . 5
        
 




          

             
  


   



        |
256 | 18, 19, 20 | istrkgb 24582 |
. . . . 5
 TarskiGB    
      




     
                 
 
  


   



         |
257 | 3, 255, 256 | sylanbrc 677 |
. . . 4

TarskiGB |
258 | 57, 257 | elind 3609 |
. . 3
 TarskiGC
TarskiGB  |
259 | 7 | ad9antr 756 |
. . . . . . . . . . . . . . . . 17
         
         
                                                
TarskiG |
260 | 11 | ad9antr 756 |
. . . . . . . . . . . . . . . . . 18
         
         
                                                
      |
261 | | simp-9r 795 |
. . . . . . . . . . . . . . . . . 18
         
         
                                                
  |
262 | 260, 261 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . 17
         
         
                                                
      |
263 | | simp-8r 793 |
. . . . . . . . . . . . . . . . . 18
         
         
                                                
  |
264 | 260, 263 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . 17
         
         
                                                
      |
265 | | simp-7r 791 |
. . . . . . . . . . . . . . . . . 18
         
         
                                                
  |
266 | 260, 265 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . 17
         
           |