Proof of Theorem tfr1onlemubacc
Step | Hyp | Ref
| Expression |
1 | | tfr1on.f |
. . . . . . . . 9
recs   |
2 | | tfr1on.g |
. . . . . . . . 9
   |
3 | | tfr1on.x |
. . . . . . . . 9
   |
4 | | tfr1on.ex |
. . . . . . . . 9
 

      |
5 | | tfr1onlemsucfn.1 |
. . . . . . . . 9
 
               |
6 | | tfr1onlembacc.3 |
. . . . . . . . 9
 
                 |
7 | | tfr1onlembacc.u |
. . . . . . . . 9
 
 
  |
8 | | tfr1onlembacc.4 |
. . . . . . . . 9
   |
9 | | tfr1onlembacc.5 |
. . . . . . . . 9
     
             |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembfn 6338 |
. . . . . . . 8
    |
11 | | fndm 5310 |
. . . . . . . 8
 

  |
12 | 10, 11 | syl 14 |
. . . . . . 7
    |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembacc 6336 |
. . . . . . . . . 10

  |
14 | 13 | unissd 3831 |
. . . . . . . . 9
     |
15 | 5, 3 | tfr1onlemssrecs 6333 |
. . . . . . . . 9
  recs    |
16 | 14, 15 | sstrd 3165 |
. . . . . . . 8
  recs    |
17 | | dmss 4821 |
. . . . . . . 8
  recs 
 recs    |
18 | 16, 17 | syl 14 |
. . . . . . 7
  recs    |
19 | 12, 18 | eqsstrrd 3192 |
. . . . . 6

recs    |
20 | 19 | sselda 3155 |
. . . . 5
 
 recs    |
21 | | eqid 2177 |
. . . . . 6
   
               
             |
22 | 21 | tfrlem9 6313 |
. . . . 5

recs 
recs        recs 
    |
23 | 20, 22 | syl 14 |
. . . 4
 
 recs        recs 
    |
24 | | tfrfun 6314 |
. . . . 5
recs   |
25 | 12 | eleq2d 2247 |
. . . . . 6
  
   |
26 | 25 | biimpar 297 |
. . . . 5
 
    |
27 | | funssfv 5536 |
. . . . 5
  recs   recs    recs            |
28 | 24, 16, 26, 27 | mp3an2ani 1344 |
. . . 4
 
 recs            |
29 | | ordelon 4379 |
. . . . . . . . . 10
     |
30 | 3, 8, 29 | syl2anc 411 |
. . . . . . . . 9
   |
31 | | eloni 4371 |
. . . . . . . . 9
   |
32 | 30, 31 | syl 14 |
. . . . . . . 8
   |
33 | | ordelss 4375 |
. . . . . . . 8
     |
34 | 32, 33 | sylan 283 |
. . . . . . 7
 
   |
35 | 12 | adantr 276 |
. . . . . . 7
 
    |
36 | 34, 35 | sseqtrrd 3194 |
. . . . . 6
 
    |
37 | | fun2ssres 5254 |
. . . . . 6
  recs   recs    recs        |
38 | 24, 16, 36, 37 | mp3an2ani 1344 |
. . . . 5
 
 recs        |
39 | 38 | fveq2d 5514 |
. . . 4
 
    recs             |
40 | 23, 28, 39 | 3eqtr3d 2218 |
. . 3
 
               |
41 | 40 | ralrimiva 2550 |
. 2
                |
42 | | fveq2 5510 |
. . . 4
             |
43 | | reseq2 4897 |
. . . . 5
  
      |
44 | 43 | fveq2d 5514 |
. . . 4
                 |
45 | 42, 44 | eqeq12d 2192 |
. . 3
                             |
46 | 45 | cbvralv 2703 |
. 2
 
           

              |
47 | 41, 46 | sylibr 134 |
1
                |