Step | Hyp | Ref
| Expression |
1 | | rdgeq2 7148 |
. . 3
           |
2 | | ifeq1 3876 |
. . . . . . . . 9
                                                   |
3 | 2 | eqeq2d 2481 |
. . . . . . . 8
                                                             |
4 | 3 | ralbidv 2829 |
. . . . . . 7
  
                                                            |
5 | 4 | anbi2d 718 |
. . . . . 6
                                


                                |
6 | 5 | rexbidv 2892 |
. . . . 5
  
                              
  
                                |
7 | 6 | abbidv 2589 |
. . . 4
    
                               
                                  |
8 | 7 | unieqd 4200 |
. . 3
     
                                
                                  |
9 | 1, 8 | eqeq12d 2486 |
. 2
          
                             
  
                                       |
10 | | df-rdg 7146 |
. . 3
  
 recs        
                |
11 | | dfrecs3 7109 |
. . 3
recs       
                  
                                     |
12 | | vex 3034 |
. . . . . . . . . . . . 13
 |
13 | 12 | resex 5154 |
. . . . . . . . . . . 12
   |
14 | | eqeq1 2475 |
. . . . . . . . . . . . . . 15
   
     |
15 | | relres 5138 |
. . . . . . . . . . . . . . . 16
   |
16 | | reldm0 5058 |
. . . . . . . . . . . . . . . 16
  
        |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 
     |
18 | 14, 17 | syl6bb 269 |
. . . . . . . . . . . . . 14
   
     |
19 | | dmeq 5040 |
. . . . . . . . . . . . . . . 16
  
    |
20 | | limeq 5442 |
. . . . . . . . . . . . . . . 16
   
     |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
   
     |
22 | | rneq 5066 |
. . . . . . . . . . . . . . . . 17
  
    |
23 | | df-ima 4852 |
. . . . . . . . . . . . . . . . 17
       |
24 | 22, 23 | syl6eqr 2523 |
. . . . . . . . . . . . . . . 16
  
      |
25 | 24 | unieqd 4200 |
. . . . . . . . . . . . . . 15
   
       |
26 | | id 22 |
. . . . . . . . . . . . . . . . 17
       |
27 | 19 | unieqd 4200 |
. . . . . . . . . . . . . . . . 17
   
     |
28 | 26, 27 | fveq12d 5885 |
. . . . . . . . . . . . . . . 16
         
         |
29 | 28 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                           |
30 | 21, 25, 29 | ifbieq12d 3899 |
. . . . . . . . . . . . . 14
    
                                        |
31 | 18, 30 | ifbieq2d 3897 |
. . . . . . . . . . . . 13
        
                                                |
32 | | eqid 2471 |
. . . . . . . . . . . . 13
                            
                |
33 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
34 | | imaexg 6749 |
. . . . . . . . . . . . . . . . 17
       |
35 | 12, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     |
36 | 35 | uniex 6606 |
. . . . . . . . . . . . . . 15
      |
37 | | fvex 5889 |
. . . . . . . . . . . . . . 15
              |
38 | 36, 37 | ifex 3940 |
. . . . . . . . . . . . . 14
 
                        |
39 | 33, 38 | ifex 3940 |
. . . . . . . . . . . . 13
       
                         |
40 | 31, 32, 39 | fvmpt 5963 |
. . . . . . . . . . . 12
 

       
                           
                          |
41 | 13, 40 | ax-mp 5 |
. . . . . . . . . . 11
       
                           
                         |
42 | | dmres 5131 |
. . . . . . . . . . . . 13
     |
43 | | onelss 5472 |
. . . . . . . . . . . . . . . . 17
 
   |
44 | 43 | imp 436 |
. . . . . . . . . . . . . . . 16
 

  |
45 | 44 | 3adant2 1049 |
. . . . . . . . . . . . . . 15
 

  |
46 | | fndm 5685 |
. . . . . . . . . . . . . . . 16

  |
47 | 46 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . 15
 
   |
48 | 45, 47 | sseqtr4d 3455 |
. . . . . . . . . . . . . 14
 

  |
49 | | df-ss 3404 |
. . . . . . . . . . . . . 14

    |
50 | 48, 49 | sylib 201 |
. . . . . . . . . . . . 13
 
     |
51 | 42, 50 | syl5eq 2517 |
. . . . . . . . . . . 12
 
     |
52 | | eqeq1 2475 |
. . . . . . . . . . . . . 14
   
     |
53 | | limeq 5442 |
. . . . . . . . . . . . . . 15
   
 
   |
54 | | unieq 4198 |
. . . . . . . . . . . . . . . . 17
         |
55 | 54 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
                     |
56 | 55 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                             |
57 | 53, 56 | ifbieq2d 3897 |
. . . . . . . . . . . . . 14
                  
                                |
58 | 52, 57 | ifbieq2d 3897 |
. . . . . . . . . . . . 13
          
                                                    |
59 | | onelon 5455 |
. . . . . . . . . . . . . . . 16
 
   |
60 | | eloni 5440 |
. . . . . . . . . . . . . . . 16
   |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
 
   |
62 | 61 | 3adant2 1049 |
. . . . . . . . . . . . . 14
 
   |
63 | | ordzsl 6691 |
. . . . . . . . . . . . . . 15
  
   |
64 | | iftrue 3878 |
. . . . . . . . . . . . . . . . 17

                            |
65 | | iftrue 3878 |
. . . . . . . . . . . . . . . . 17

                          |
66 | 64, 65 | eqtr4d 2508 |
. . . . . . . . . . . . . . . 16

                                                    |
67 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
68 | 67 | sucid 5509 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
69 | | fvres 5893 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
71 | | eloni 5440 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
72 | | ordunisuc 6678 |
. . . . . . . . . . . . . . . . . . . . . . 23

   |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  |
74 | 73 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
         
      |
75 | 73 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
            |
76 | 70, 74, 75 | 3eqtr4a 2531 |
. . . . . . . . . . . . . . . . . . . 20
               |
77 | 76 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
                       |
78 | | nsuceq0 5510 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
79 | 78 | neii 2645 |
. . . . . . . . . . . . . . . . . . . . 21
 |
80 | 79 | iffalsei 3882 |
. . . . . . . . . . . . . . . . . . . 20
     
                                 
        |
81 | | nlimsucg 6688 |
. . . . . . . . . . . . . . . . . . . . 21
   |
82 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . . . 21
  
                                |
83 | 67, 81, 82 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
 
                               |
84 | 80, 83 | eqtri 2493 |
. . . . . . . . . . . . . . . . . . 19
     
                        
       |
85 | 79 | iffalsei 3882 |
. . . . . . . . . . . . . . . . . . . 20
     
                                      |
86 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . . . 21
  
                            |
87 | 67, 81, 86 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
 
                           |
88 | 85, 87 | eqtri 2493 |
. . . . . . . . . . . . . . . . . . 19
     
                            |
89 | 77, 84, 88 | 3eqtr4g 2530 |
. . . . . . . . . . . . . . . . . 18
      
                         
                    |
90 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
91 | | limeq 5442 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
92 | | reseq2 5106 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
93 | | unieq 4198 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
94 | 92, 93 | fveq12d 5885 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
95 | 94 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
96 | 91, 95 | ifbieq2d 3897 |
. . . . . . . . . . . . . . . . . . . 20
              
        
                     |
97 | 90, 96 | ifbieq2d 3897 |
. . . . . . . . . . . . . . . . . . 19
                                
                      |
98 | 93 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
99 | 98 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
100 | 91, 99 | ifbieq2d 3897 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
101 | 90, 100 | ifbieq2d 3897 |
. . . . . . . . . . . . . . . . . . 19
                              
                    |
102 | 97, 101 | eqeq12d 2486 |
. . . . . . . . . . . . . . . . . 18
                   
                                      
                        
                     |
103 | 89, 102 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . 17
                                                       |
104 | 103 | rexlimiv 2867 |
. . . . . . . . . . . . . . . 16
                                                      |
105 | | iftrue 3878 |
. . . . . . . . . . . . . . . . . 18

                            |
106 | | df-lim 5435 |
. . . . . . . . . . . . . . . . . . . . 21
 
    |
107 | 106 | simp2bi 1046 |
. . . . . . . . . . . . . . . . . . . 20

  |
108 | 107 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . 19

  |
109 | 108 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . 18

                                                 |
110 | | iftrue 3878 |
. . . . . . . . . . . . . . . . . 18

                          |
111 | 105, 109,
110 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . . 17

                                               |
112 | 108 | iffalsed 3883 |
. . . . . . . . . . . . . . . . 17

                                             |
113 | 111, 112 | eqtr4d 2508 |
. . . . . . . . . . . . . . . 16

                                                    |
114 | 66, 104, 113 | 3jaoi 1357 |
. . . . . . . . . . . . . . 15
  
                                                     |
115 | 63, 114 | sylbi 200 |
. . . . . . . . . . . . . 14

                                                    |
116 | 62, 115 | syl 17 |
. . . . . . . . . . . . 13
 
                                                     |
117 | 58, 116 | sylan9eqr 2527 |
. . . . . . . . . . . 12
  
   
                                                          |
118 | 51, 117 | mpdan 681 |
. . . . . . . . . . 11
 
        
                                                  |
119 | 41, 118 | syl5eq 2517 |
. . . . . . . . . 10
 
         
                                             |
120 | 119 | eqeq2d 2481 |
. . . . . . . . 9
 
             
                   
                               |
121 | 120 | 3expa 1231 |
. . . . . . . 8
    
                                
                               |
122 | 121 | ralbidva 2828 |
. . . . . . 7
 
              
                   

                               |
123 | 122 | pm5.32da 653 |
. . . . . 6
               
                                                       |
124 | 123 | rexbiia 2880 |
. . . . 5
                                    
  
                               |
125 | 124 | abbii 2587 |
. . . 4
   
           
                         
                               |
126 | 125 | unieqi 4199 |
. . 3
    
           
                          
                               |
127 | 10, 11, 126 | 3eqtri 2497 |
. 2
  
                                     |
128 | 9, 127 | vtoclg 3093 |
1
         
                                |