Proof of Theorem tfrlem11
Step | Hyp | Ref
| Expression |
1 | | elsuci 5489 |
. 2
 recs  
recs  recs     |
2 | | tfrlem.1 |
. . . . . . . . 9
 
               |
3 | | tfrlem.3 |
. . . . . . . . 9
recs    recs     recs       |
4 | 2, 3 | tfrlem10 7105 |
. . . . . . . 8
 recs 
recs    |
5 | | fnfun 5673 |
. . . . . . . 8
 recs    |
6 | 4, 5 | syl 17 |
. . . . . . 7
 recs 
  |
7 | | ssun1 3597 |
. . . . . . . . 9
recs 
recs    recs     recs       |
8 | 7, 3 | sseqtr4i 3465 |
. . . . . . . 8
recs 
 |
9 | 2 | tfrlem9 7103 |
. . . . . . . . 9

recs 
recs        recs 
    |
10 | | funssfv 5880 |
. . . . . . . . . . . 12
  recs 
recs       recs       |
11 | 10 | 3expa 1208 |
. . . . . . . . . . 11
   recs  
recs       recs       |
12 | 11 | adantrl 722 |
. . . . . . . . . 10
   recs  
 recs  recs        recs       |
13 | | onelss 5465 |
. . . . . . . . . . . 12
 recs 
 recs  recs     |
14 | 13 | imp 431 |
. . . . . . . . . . 11
  recs  recs  
recs    |
15 | | fun2ssres 5623 |
. . . . . . . . . . . . 13
  recs 
recs     recs 
   |
16 | 15 | 3expa 1208 |
. . . . . . . . . . . 12
   recs  
recs     recs 
   |
17 | 16 | fveq2d 5869 |
. . . . . . . . . . 11
   recs  
recs            recs      |
18 | 14, 17 | sylan2 477 |
. . . . . . . . . 10
   recs  
 recs  recs       
     recs 
    |
19 | 12, 18 | eqeq12d 2466 |
. . . . . . . . 9
   recs  
 recs  recs               recs        recs       |
20 | 9, 19 | syl5ibr 225 |
. . . . . . . 8
   recs  
 recs  recs     recs               |
21 | 8, 20 | mpanl2 687 |
. . . . . . 7
   recs  recs   
 recs               |
22 | 6, 21 | sylan 474 |
. . . . . 6
  recs   recs  recs   
 recs               |
23 | 22 | exp32 610 |
. . . . 5
 recs 
 recs   recs  
recs 
               |
24 | 23 | pm2.43i 49 |
. . . 4
 recs 
 recs   recs                |
25 | 24 | pm2.43d 50 |
. . 3
 recs 
 recs               |
26 | | opex 4664 |
. . . . . . . . 9
          |
27 | 26 | snid 3996 |
. . . . . . . 8
                     |
28 | | opeq1 4166 |
. . . . . . . . . . 11

recs 
        
 recs            |
29 | 28 | adantl 468 |
. . . . . . . . . 10
  recs  recs  
        
 recs            |
30 | | eqimss 3484 |
. . . . . . . . . . . . . 14

recs 
recs    |
31 | 8, 15 | mp3an2 1352 |
. . . . . . . . . . . . . 14
  recs     recs     |
32 | 6, 30, 31 | syl2an 480 |
. . . . . . . . . . . . 13
  recs  recs  
  recs     |
33 | | reseq2 5100 |
. . . . . . . . . . . . . . 15

recs 
recs   recs 
recs     |
34 | 2 | tfrlem6 7100 |
. . . . . . . . . . . . . . . 16
recs   |
35 | | resdm 5146 |
. . . . . . . . . . . . . . . 16
 recs  recs  recs   recs    |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
recs  recs   recs   |
37 | 33, 36 | syl6eq 2501 |
. . . . . . . . . . . . . 14

recs 
recs   recs    |
38 | 37 | adantl 468 |
. . . . . . . . . . . . 13
  recs  recs  
recs   recs    |
39 | 32, 38 | eqtrd 2485 |
. . . . . . . . . . . 12
  recs  recs  
  recs    |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . 11
  recs  recs  
        recs     |
41 | 40 | opeq2d 4173 |
. . . . . . . . . 10
  recs  recs  
 recs          
recs     recs      |
42 | 29, 41 | eqtrd 2485 |
. . . . . . . . 9
  recs  recs  
        
 recs     recs      |
43 | 42 | sneqd 3980 |
. . . . . . . 8
  recs  recs  
             recs     recs       |
44 | 27, 43 | syl5eleq 2535 |
. . . . . . 7
  recs  recs  
           recs     recs       |
45 | | elun2 3602 |
. . . . . . 7
  
      
  recs     recs              recs    recs     recs        |
46 | 44, 45 | syl 17 |
. . . . . 6
  recs  recs  
         recs    recs     recs        |
47 | 46, 3 | syl6eleqr 2540 |
. . . . 5
  recs  recs  
           |
48 | 4 | adantr 467 |
. . . . . 6
  recs  recs  
recs    |
49 | | simpr 463 |
. . . . . . 7
  recs  recs  
recs    |
50 | | sucidg 5501 |
. . . . . . . 8
 recs 
recs  recs    |
51 | 50 | adantr 467 |
. . . . . . 7
  recs  recs  
recs  recs    |
52 | 49, 51 | eqeltrd 2529 |
. . . . . 6
  recs  recs  
recs    |
53 | | fnopfvb 5906 |
. . . . . 6
  recs 
recs             
            |
54 | 48, 52, 53 | syl2anc 667 |
. . . . 5
  recs  recs  
        
              |
55 | 47, 54 | mpbird 236 |
. . . 4
  recs  recs  
            |
56 | 55 | ex 436 |
. . 3
 recs 
 recs               |
57 | 25, 56 | jaod 382 |
. 2
 recs 
 
recs  recs  
             |
58 | 1, 57 | syl5 33 |
1
 recs 

recs 
             |