Proof of Theorem tfrlem10
Step | Hyp | Ref
| Expression |
1 | | fvex 5875 |
. . . . . . 7
  recs    |
2 | | funsng 5628 |
. . . . . . 7
  recs    recs   
  recs     recs       |
3 | 1, 2 | mpan2 677 |
. . . . . 6
 recs 
  recs     recs       |
4 | | tfrlem.1 |
. . . . . . 7
 
               |
5 | 4 | tfrlem7 7101 |
. . . . . 6
recs   |
6 | 3, 5 | jctil 540 |
. . . . 5
 recs 
 recs    recs     recs        |
7 | 1 | dmsnop 5310 |
. . . . . . 7
  recs     recs    
 recs    |
8 | 7 | ineq2i 3631 |
. . . . . 6
 recs   
recs     recs      
recs 
 recs     |
9 | 4 | tfrlem8 7102 |
. . . . . . 7
recs   |
10 | | orddisj 5461 |
. . . . . . 7
 recs  
recs 
 recs      |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
 recs  
recs     |
12 | 8, 11 | eqtri 2473 |
. . . . 5
 recs   
recs     recs       |
13 | | funun 5624 |
. . . . 5
  
recs 
  recs     recs       recs   
recs     recs      
recs    recs     recs        |
14 | 6, 12, 13 | sylancl 668 |
. . . 4
 recs 
recs    recs     recs        |
15 | 7 | uneq2i 3585 |
. . . . 5
 recs   
recs     recs      
recs   recs     |
16 | | dmun 5041 |
. . . . 5
recs    recs     recs       recs    recs     recs       |
17 | | df-suc 5429 |
. . . . 5
recs   recs   recs     |
18 | 15, 16, 17 | 3eqtr4i 2483 |
. . . 4
recs    recs     recs      recs   |
19 | 14, 18 | jctir 541 |
. . 3
 recs 
 recs   
recs     recs      recs    recs     recs      recs     |
20 | | df-fn 5585 |
. . 3
 recs   
recs     recs      recs  
recs    recs     recs      recs   
recs     recs     
recs     |
21 | 19, 20 | sylibr 216 |
. 2
 recs 
recs    recs     recs      recs    |
22 | | tfrlem.3 |
. . 3
recs    recs     recs       |
23 | 22 | fneq1i 5670 |
. 2
 recs 
recs    recs     recs      recs    |
24 | 21, 23 | sylibr 216 |
1
 recs 
recs    |