Step | Hyp | Ref
| Expression |
1 | | tfr1on.x |
. . 3
   |
2 | | ordelon 4380 |
. . 3
     |
3 | 1, 2 | sylan 283 |
. 2
 
   |
4 | | eleq1 2240 |
. . . . 5
 
   |
5 | 4 | anbi2d 464 |
. . . 4
  

     |
6 | | fneq2 5301 |
. . . . . 6
 
   |
7 | | raleq 2672 |
. . . . . 6
  
         

             |
8 | 6, 7 | anbi12d 473 |
. . . . 5
                               |
9 | 8 | exbidv 1825 |
. . . 4
     
              
              |
10 | 5, 9 | imbi12d 234 |
. . 3
   
    
             
    
               |
11 | | eleq1 2240 |
. . . . 5
 
   |
12 | 11 | anbi2d 464 |
. . . 4
  

     |
13 | | fneq2 5301 |
. . . . . 6
 
   |
14 | | raleq 2672 |
. . . . . 6
  
         

             |
15 | 13, 14 | anbi12d 473 |
. . . . 5
                               |
16 | 15 | exbidv 1825 |
. . . 4
     
              
              |
17 | 12, 16 | imbi12d 234 |
. . 3
   
    
             
    
               |
18 | | tfr1on.f |
. . . . . . . . 9
recs   |
19 | | tfr1on.g |
. . . . . . . . . 10
   |
20 | 19 | ad3antrrr 492 |
. . . . . . . . 9
   
      
                |
21 | 1 | ad3antrrr 492 |
. . . . . . . . 9
   
      
                |
22 | | tfr1on.ex |
. . . . . . . . . . . . . . . . 17
 

      |
23 | 22 | 3expia 1205 |
. . . . . . . . . . . . . . . 16
 
         |
24 | 23 | alrimiv 1874 |
. . . . . . . . . . . . . . 15
 
           |
25 | | fneq1 5300 |
. . . . . . . . . . . . . . . . 17
 
   |
26 | | fveq2 5511 |
. . . . . . . . . . . . . . . . . 18
           |
27 | 26 | eleq1d 2246 |
. . . . . . . . . . . . . . . . 17
     
       |
28 | 25, 27 | imbi12d 234 |
. . . . . . . . . . . . . . . 16
                 |
29 | 28 | cbvalv 1917 |
. . . . . . . . . . . . . . 15
   
               |
30 | 24, 29 | sylib 122 |
. . . . . . . . . . . . . 14
 
           |
31 | 30 | 19.21bi 1558 |
. . . . . . . . . . . . 13
 
         |
32 | 31 | 3impia 1200 |
. . . . . . . . . . . 12
 

      |
33 | 32 | 3adant1r 1231 |
. . . . . . . . . . 11
   
       |
34 | 33 | 3adant1r 1231 |
. . . . . . . . . 10
   
      
                    |
35 | 34 | 3adant1r 1231 |
. . . . . . . . 9
       
                 
       |
36 | | tfr1onlemsucfn.1 |
. . . . . . . . . 10
 
               |
37 | | fveq1 5510 |
. . . . . . . . . . . . . . 15
           |
38 | | reseq1 4897 |
. . . . . . . . . . . . . . . 16
       |
39 | 38 | fveq2d 5515 |
. . . . . . . . . . . . . . 15
               |
40 | 37, 39 | eqeq12d 2192 |
. . . . . . . . . . . . . 14
           
             |
41 | 40 | ralbidv 2477 |
. . . . . . . . . . . . 13
  
         

             |
42 | 25, 41 | anbi12d 473 |
. . . . . . . . . . . 12
                               |
43 | 42 | rexbidv 2478 |
. . . . . . . . . . 11
  
             

               |
44 | 43 | cbvabv 2302 |
. . . . . . . . . 10
   
              
              |
45 | 36, 44 | eqtri 2198 |
. . . . . . . . 9
 
         
     |
46 | | fneq1 5300 |
. . . . . . . . . . . . . . 15
 
   |
47 | | eleq1 2240 |
. . . . . . . . . . . . . . 15
 
   |
48 | | id 19 |
. . . . . . . . . . . . . . . . 17
   |
49 | | fveq2 5511 |
. . . . . . . . . . . . . . . . . . 19
           |
50 | 49 | opeq2d 3783 |
. . . . . . . . . . . . . . . . . 18
                 |
51 | 50 | sneqd 3604 |
. . . . . . . . . . . . . . . . 17
                     |
52 | 48, 51 | uneq12d 3290 |
. . . . . . . . . . . . . . . 16
                         |
53 | 52 | eqeq2d 2189 |
. . . . . . . . . . . . . . 15
                           |
54 | 46, 47, 53 | 3anbi123d 1312 |
. . . . . . . . . . . . . 14
  
                            |
55 | 54 | cbvexv 1918 |
. . . . . . . . . . . . 13
               
  
              |
56 | 55 | rexbii 2484 |
. . . . . . . . . . . 12
                

  
              |
57 | | fneq2 5301 |
. . . . . . . . . . . . . . 15
 
   |
58 | | opeq1 3776 |
. . . . . . . . . . . . . . . . . 18
                 |
59 | 58 | sneqd 3604 |
. . . . . . . . . . . . . . . . 17
                     |
60 | 59 | uneq2d 3289 |
. . . . . . . . . . . . . . . 16
                         |
61 | 60 | eqeq2d 2189 |
. . . . . . . . . . . . . . 15
                           |
62 | 57, 61 | 3anbi13d 1314 |
. . . . . . . . . . . . . 14
  
                            |
63 | 62 | exbidv 1825 |
. . . . . . . . . . . . 13
                
  
               |
64 | 63 | cbvrexv 2704 |
. . . . . . . . . . . 12
                

  
              |
65 | 56, 64 | bitri 184 |
. . . . . . . . . . 11
                

  
              |
66 | 65 | abbii 2293 |
. . . . . . . . . 10
    
                 
              |
67 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
                           |
68 | 67 | 3anbi3d 1318 |
. . . . . . . . . . . . 13
  
                            |
69 | 68 | exbidv 1825 |
. . . . . . . . . . . 12
                
  
               |
70 | 69 | rexbidv 2478 |
. . . . . . . . . . 11
  
              

  
               |
71 | 70 | cbvabv 2302 |
. . . . . . . . . 10
    
                 
              |
72 | 66, 71 | eqtri 2198 |
. . . . . . . . 9
    
                 
              |
73 | | tfr1onlemaccex.u |
. . . . . . . . . . . 12
 
 
  |
74 | 73 | adantlr 477 |
. . . . . . . . . . 11
        |
75 | 74 | adantlr 477 |
. . . . . . . . . 10
   
      
                 |
76 | 75 | adantlr 477 |
. . . . . . . . 9
       
                      |
77 | | simpr 110 |
. . . . . . . . 9
   
      
                |
78 | | simpr 110 |
. . . . . . . . . . . 12
       
                     |
79 | | simplr 528 |
. . . . . . . . . . . 12
       
                     |
80 | | ordtr1 4385 |
. . . . . . . . . . . . . 14

 
    |
81 | 1, 80 | syl 14 |
. . . . . . . . . . . . 13
       |
82 | 81 | ad4antr 494 |
. . . . . . . . . . . 12
       
                     
   |
83 | 78, 79, 82 | mp2and 433 |
. . . . . . . . . . 11
       
                     |
84 | | eleq1 2240 |
. . . . . . . . . . . . . 14
 
   |
85 | | fneq2 5301 |
. . . . . . . . . . . . . . . 16
 
   |
86 | | raleq 2672 |
. . . . . . . . . . . . . . . 16
  
         

             |
87 | 85, 86 | anbi12d 473 |
. . . . . . . . . . . . . . 15
                               |
88 | 87 | exbidv 1825 |
. . . . . . . . . . . . . 14
     
              
              |
89 | 84, 88 | imbi12d 234 |
. . . . . . . . . . . . 13
      
                
               |
90 | | simpllr 534 |
. . . . . . . . . . . . 13
       
                   

                  |
91 | 89, 90, 78 | rspcdva 2846 |
. . . . . . . . . . . 12
       
                       
              |
92 | | fneq1 5300 |
. . . . . . . . . . . . . . 15
 
   |
93 | | fveq1 5510 |
. . . . . . . . . . . . . . . . 17
           |
94 | | reseq1 4897 |
. . . . . . . . . . . . . . . . . 18
       |
95 | 94 | fveq2d 5515 |
. . . . . . . . . . . . . . . . 17
               |
96 | 93, 95 | eqeq12d 2192 |
. . . . . . . . . . . . . . . 16
           
             |
97 | 96 | ralbidv 2477 |
. . . . . . . . . . . . . . 15
  
         

             |
98 | 92, 97 | anbi12d 473 |
. . . . . . . . . . . . . 14
                               |
99 | 98 | cbvexv 1918 |
. . . . . . . . . . . . 13
    
              
             |
100 | | fveq2 5511 |
. . . . . . . . . . . . . . . . 17
           |
101 | | reseq2 4898 |
. . . . . . . . . . . . . . . . . 18
       |
102 | 101 | fveq2d 5515 |
. . . . . . . . . . . . . . . . 17
               |
103 | 100, 102 | eqeq12d 2192 |
. . . . . . . . . . . . . . . 16
           
             |
104 | 103 | cbvralv 2703 |
. . . . . . . . . . . . . . 15
 
         

            |
105 | 104 | anbi2i 457 |
. . . . . . . . . . . . . 14
             


             |
106 | 105 | exbii 1605 |
. . . . . . . . . . . . 13
    
              
             |
107 | 99, 106 | bitri 184 |
. . . . . . . . . . . 12
    
              
             |
108 | 91, 107 | syl6ib 161 |
. . . . . . . . . . 11
       
                       
              |
109 | 83, 108 | mpd 13 |
. . . . . . . . . 10
       
                                    |
110 | 109 | ralrimiva 2550 |
. . . . . . . . 9
   
      
              
                 |
111 | 18, 20, 21, 35, 45, 72, 76, 77, 110 | tfr1onlemex 6342 |
. . . . . . . 8
   
      
                               |
112 | | fneq1 5300 |
. . . . . . . . . 10
 
   |
113 | | fveq1 5510 |
. . . . . . . . . . . 12
           |
114 | | reseq1 4897 |
. . . . . . . . . . . . 13
       |
115 | 114 | fveq2d 5515 |
. . . . . . . . . . . 12
               |
116 | 113, 115 | eqeq12d 2192 |
. . . . . . . . . . 11
           
             |
117 | 116 | ralbidv 2477 |
. . . . . . . . . 10
  
         

             |
118 | 112, 117 | anbi12d 473 |
. . . . . . . . 9
                               |
119 | 118 | cbvexv 1918 |
. . . . . . . 8
    
              
             |
120 | 111, 119 | sylib 122 |
. . . . . . 7
   
      
                               |
121 | 120 | exp31 364 |
. . . . . 6
 

 
    
           

                   |
122 | 121 | expcom 116 |
. . . . 5
   

               

                    |
123 | 122 | a2d 26 |
. . . 4
  


                  
                    |
124 | | impexp 263 |
. . . . . 6
                         
               |
125 | 124 | ralbii 2483 |
. . . . 5
 
 
                       
               |
126 | | r19.21v 2554 |
. . . . 5
 
 
                
      
               |
127 | 125, 126 | bitri 184 |
. . . 4
 
 
                       
               |
128 | | impexp 263 |
. . . 4
                         
               |
129 | 123, 127,
128 | 3imtr4g 205 |
. . 3
  
 
    
                  
               |
130 | 10, 17, 129 | tfis3 4582 |
. 2
  
                   |
131 | 3, 130 | mpcom 36 |
1
 
                  |