Step | Hyp | Ref
| Expression |
1 | | fveq2 5510 |
. . . . 5
 recs     recs       |
2 | 1 | eleq1d 2246 |
. . . 4
  recs     recs        |
3 | 2 | imbi2d 230 |
. . 3
  
recs       recs         |
4 | | inss2 3356 |
. . . . . . 7
   |
5 | | ssorduni 4482 |
. . . . . . 7
 

     |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
 
  |
7 | | vex 2740 |
. . . . . . . . . 10
 |
8 | 7 | sucex 4494 |
. . . . . . . . 9
 |
9 | 8 | sucex 4494 |
. . . . . . . 8
 |
10 | 9 | inex1 4134 |
. . . . . . 7
 
 |
11 | 10 | uniex 4433 |
. . . . . 6
  
 |
12 | | elon2 4372 |
. . . . . 6
  

     
    |
13 | 6, 11, 12 | mpbir2an 942 |
. . . . 5
  
 |
14 | | tfrexlem.1 |
. . . . . . 7
 
               |
15 | 14 | tfrlem3 6305 |
. . . . . 6
 
               |
16 | | tfrexlem.2 |
. . . . . . 7
   
       |
17 | | fveq2 5510 |
. . . . . . . . . 10
           |
18 | 17 | eleq1d 2246 |
. . . . . . . . 9
     
       |
19 | 18 | anbi2d 464 |
. . . . . . . 8
  
    
         |
20 | 19 | cbvalv 1917 |
. . . . . . 7
                   |
21 | 16, 20 | sylib 122 |
. . . . . 6
   
       |
22 | 15, 21 | tfrlemi1 6326 |
. . . . 5
 
  
                         |
23 | 13, 22 | mpan2 425 |
. . . 4
                         |
24 | 15 | recsfval 6309 |
. . . . . . . . . . 11
recs    |
25 | 24 | breqi 4006 |
. . . . . . . . . 10
 recs        |
26 | | df-br 4001 |
. . . . . . . . . 10
   
  
   |
27 | | eluni 3810 |
. . . . . . . . . 10
    
         |
28 | 25, 26, 27 | 3bitri 206 |
. . . . . . . . 9
 recs        
   |
29 | 7 | sucid 4413 |
. . . . . . . . . . . . . . . . 17
 |
30 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
   |
31 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
32 | 14, 31 | tfrlem3a 6304 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  
             |
33 | 30, 32 | sylib 122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
   
             |
34 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
                |
35 | | simprrl 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
                |
36 | | simpll 527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
                   |
37 | | fnop 5314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        |
38 | 35, 36, 37 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
                |
39 | | onelon 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
40 | 34, 38, 39 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
                |
41 | 33, 40 | rexlimddv 2599 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
   |
42 | 41 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                         |
43 | | onsuc 4496 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
44 | 42, 43 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                      
  |
45 | | onsuc 4496 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
    
                         |
47 | | onss 4488 |
. . . . . . . . . . . . . . . . . . . . 21

  |
48 | 46, 47 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
    
                         |
49 | | df-ss 3142 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
50 | 48, 49 | sylib 122 |
. . . . . . . . . . . . . . . . . . 19
    
                       
   |
51 | 50 | unieqd 3818 |
. . . . . . . . . . . . . . . . . 18
    
                             |
52 | | eloni 4371 |
. . . . . . . . . . . . . . . . . . . 20
   |
53 | | ordtr 4374 |
. . . . . . . . . . . . . . . . . . . 20
   |
54 | 44, 52, 53 | 3syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
                         |
55 | 8 | unisuc 4409 |
. . . . . . . . . . . . . . . . . . 19


  |
56 | 54, 55 | sylib 122 |
. . . . . . . . . . . . . . . . . 18
    
                       
  |
57 | 51, 56 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
    
                            |
58 | 29, 57 | eleqtrrid 2267 |
. . . . . . . . . . . . . . . 16
    
                            |
59 | | fndm 5310 |
. . . . . . . . . . . . . . . . 17
   
     |
60 | 59 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
    
                      
 
   |
61 | 58, 60 | eleqtrrd 2257 |
. . . . . . . . . . . . . . 15
    
                         |
62 | 7 | eldm 4819 |
. . . . . . . . . . . . . . 15

     |
63 | 61, 62 | sylib 122 |
. . . . . . . . . . . . . 14
    
                       
    |
64 | | simpr 110 |
. . . . . . . . . . . . . . 15
                          
         |
65 | | fneq2 5300 |
. . . . . . . . . . . . . . . . . . . . 21
      
    |
66 | | raleq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
     
         
                  |
67 | 65, 66 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . . 20
      
          
                       |
68 | 67 | rspcev 2841 |
. . . . . . . . . . . . . . . . . . 19
                                          |
69 | 13, 68 | mpan 424 |
. . . . . . . . . . . . . . . . . 18
                     
               |
70 | | vex 2740 |
. . . . . . . . . . . . . . . . . . 19
 |
71 | 14, 70 | tfrlem3a 6304 |
. . . . . . . . . . . . . . . . . 18

  
             |
72 | 69, 71 | sylibr 134 |
. . . . . . . . . . . . . . . . 17
                       |
73 | 72 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
                          
       |
74 | | simplrr 536 |
. . . . . . . . . . . . . . . 16
                          
    
  |
75 | | simplrl 535 |
. . . . . . . . . . . . . . . . 17
                          
          |
76 | | df-br 4001 |
. . . . . . . . . . . . . . . . 17
  
  
  |
77 | 75, 76 | sylibr 134 |
. . . . . . . . . . . . . . . 16
                          
         |
78 | 15 | tfrlem5 6308 |
. . . . . . . . . . . . . . . . 17
 
           |
79 | 78 | imp 124 |
. . . . . . . . . . . . . . . 16
  

         |
80 | 73, 74, 64, 77, 79 | syl22anc 1239 |
. . . . . . . . . . . . . . 15
                          
    
  |
81 | 64, 80 | breqtrd 4026 |
. . . . . . . . . . . . . 14
                          
         |
82 | 63, 81 | exlimddv 1898 |
. . . . . . . . . . . . 13
    
                           |
83 | | vex 2740 |
. . . . . . . . . . . . . 14
 |
84 | 7, 83 | brelrn 4855 |
. . . . . . . . . . . . 13
     |
85 | 82, 84 | syl 14 |
. . . . . . . . . . . 12
    
                         |
86 | | elssuni 3835 |
. . . . . . . . . . . 12

   |
87 | 85, 86 | syl 14 |
. . . . . . . . . . 11
    
                      
   |
88 | 87 | ex 115 |
. . . . . . . . . 10
                         

    |
89 | 88 | exlimdv 1819 |
. . . . . . . . 9
                           
 
   |
90 | 28, 89 | biimtrid 152 |
. . . . . . . 8
                      recs   
   |
91 | 90 | alrimiv 1874 |
. . . . . . 7
                        recs  
    |
92 | | fvss 5524 |
. . . . . . 7
    recs  
 
recs    
   |
93 | 91, 92 | syl 14 |
. . . . . 6
                     recs        |
94 | 70 | rnex 4889 |
. . . . . . . 8
 |
95 | 94 | uniex 4433 |
. . . . . . 7

 |
96 | 95 | ssex 4137 |
. . . . . 6
 recs      recs       |
97 | 93, 96 | syl 14 |
. . . . 5
                     recs       |
98 | 97 | exlimiv 1598 |
. . . 4
                       recs       |
99 | 23, 98 | syl 14 |
. . 3
 recs       |
100 | 3, 99 | vtoclg 2797 |
. 2
  recs        |
101 | 100 | impcom 125 |
1
 
 recs       |