Step | Hyp | Ref
| Expression |
1 | | frfnom 7170 |
. . . . . . 7
     
                |
2 | | seqomlem.a |
. . . . . . . . 9
                    |
3 | 2 | reseq1i 5107 |
. . . . . . . 8
                        |
4 | 3 | fneq1i 5680 |
. . . . . . 7
 
     
              
   |
5 | 1, 4 | mpbir 214 |
. . . . . 6
   |
6 | | fvres 5893 |
. . . . . . . . 9
             |
7 | 2 | seqomlem1 7185 |
. . . . . . . . 9
                  |
8 | 6, 7 | eqtrd 2505 |
. . . . . . . 8
                    |
9 | | fvex 5889 |
. . . . . . . . 9
         |
10 | | opelxpi 4871 |
. . . . . . . . 9
                          |
11 | 9, 10 | mpan2 685 |
. . . . . . . 8
                |
12 | 8, 11 | eqeltrd 2549 |
. . . . . . 7
           |
13 | 12 | rgen 2766 |
. . . . . 6
          |
14 | | ffnfv 6064 |
. . . . . 6
 
      
               |
15 | 5, 13, 14 | mpbir2an 934 |
. . . . 5
         |
16 | | frn 5747 |
. . . . 5
 
      
      |
17 | 15, 16 | ax-mp 5 |
. . . 4
     |
18 | | df-br 4396 |
. . . . . . . . . 10
    
  

   |
19 | | fvelrnb 5926 |
. . . . . . . . . . 11
 

    
              |
20 | 5, 19 | ax-mp 5 |
. . . . . . . . . 10
     
            |
21 | | fvres 5893 |
. . . . . . . . . . . 12
             |
22 | 21 | eqeq1d 2473 |
. . . . . . . . . . 11
                     |
23 | 22 | rexbiia 2880 |
. . . . . . . . . 10
          
          |
24 | 18, 20, 23 | 3bitri 279 |
. . . . . . . . 9
    
          |
25 | 2 | seqomlem1 7185 |
. . . . . . . . . . . . . . . 16
                  |
26 | 25 | adantl 473 |
. . . . . . . . . . . . . . 15
 
                  |
27 | 26 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
 
        
                 |
28 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
29 | | fvex 5889 |
. . . . . . . . . . . . . . 15
         |
30 | 28, 29 | opth1 4675 |
. . . . . . . . . . . . . 14
                 |
31 | 27, 30 | syl6bi 236 |
. . . . . . . . . . . . 13
 
            |
32 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
33 | 32 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
        
          |
34 | 33 | biimpd 212 |
. . . . . . . . . . . . 13
                   |
35 | 31, 34 | syli 37 |
. . . . . . . . . . . 12
 
                   |
36 | | fveq2 5879 |
. . . . . . . . . . . . 13
                         |
37 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
38 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
39 | 37, 38 | op2nd 6821 |
. . . . . . . . . . . . 13
      
 |
40 | 36, 39 | syl6req 2522 |
. . . . . . . . . . . 12
                  |
41 | 35, 40 | syl6 33 |
. . . . . . . . . . 11
 
                    |
42 | 41 | rexlimdva 2871 |
. . . . . . . . . 10
  
                  |
43 | 2 | seqomlem1 7185 |
. . . . . . . . . . . 12
                  |
44 | 32 | eqeq1d 2473 |
. . . . . . . . . . . . 13
                                   |
45 | 44 | rspcev 3136 |
. . . . . . . . . . . 12
                 
                  |
46 | 43, 45 | mpdan 681 |
. . . . . . . . . . 11
                   |
47 | | opeq2 4159 |
. . . . . . . . . . . . 13
        
  
             |
48 | 47 | eqeq2d 2481 |
. . . . . . . . . . . 12
        
                          |
49 | 48 | rexbidv 2892 |
. . . . . . . . . . 11
        
 
                          |
50 | 46, 49 | syl5ibrcom 230 |
. . . . . . . . . 10
                     |
51 | 42, 50 | impbid 195 |
. . . . . . . . 9
  
                  |
52 | 24, 51 | syl5bb 265 |
. . . . . . . 8
  
  
           |
53 | 52 | alrimiv 1781 |
. . . . . . 7
                   |
54 | | fvex 5889 |
. . . . . . . 8
         |
55 | | eqeq2 2482 |
. . . . . . . . . 10
        

           |
56 | 55 | bibi2d 325 |
. . . . . . . . 9
        
  
  

                 |
57 | 56 | albidv 1775 |
. . . . . . . 8
        
               
            |
58 | 54, 57 | spcev 3127 |
. . . . . . 7
                
            |
59 | 53, 58 | syl 17 |
. . . . . 6
             |
60 | | df-eu 2323 |
. . . . . 6
              
   |
61 | 59, 60 | sylibr 217 |
. . . . 5
        |
62 | 61 | rgen 2766 |
. . . 4
       |
63 | | dff3 6050 |
. . . 4
      
      
 
     |
64 | 17, 62, 63 | mpbir2an 934 |
. . 3
       |
65 | | df-ima 4852 |
. . . 4
       |
66 | 65 | feq1i 5730 |
. . 3
        
        |
67 | 64, 66 | mpbir 214 |
. 2
         |
68 | | dffn2 5741 |
. 2
               |
69 | 67, 68 | mpbir 214 |
1
     |