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 6195 |
. . . . . . . 8
    |
11 | | fndm 5180 |
. . . . . . . 8
 

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

  |
14 | 13 | unissd 3726 |
. . . . . . . . 9
     |
15 | 5, 3 | tfr1onlemssrecs 6190 |
. . . . . . . . 9
  recs    |
16 | 14, 15 | sstrd 3073 |
. . . . . . . 8
  recs    |
17 | | dmss 4698 |
. . . . . . . 8
  recs 
 recs    |
18 | 16, 17 | syl 14 |
. . . . . . 7
  recs    |
19 | 12, 18 | eqsstrrd 3100 |
. . . . . 6

recs    |
20 | 19 | sselda 3063 |
. . . . 5
 
 recs    |
21 | | eqid 2115 |
. . . . . 6
   
               
             |
22 | 21 | tfrlem9 6170 |
. . . . 5

recs 
recs        recs 
    |
23 | 20, 22 | syl 14 |
. . . 4
 
 recs        recs 
    |
24 | | tfrfun 6171 |
. . . . 5
recs   |
25 | 12 | eleq2d 2184 |
. . . . . 6
  
   |
26 | 25 | biimpar 293 |
. . . . 5
 
    |
27 | | funssfv 5401 |
. . . . 5
  recs   recs    recs            |
28 | 24, 16, 26, 27 | mp3an2ani 1305 |
. . . 4
 
 recs            |
29 | | ordelon 4265 |
. . . . . . . . . 10
     |
30 | 3, 8, 29 | syl2anc 406 |
. . . . . . . . 9
   |
31 | | eloni 4257 |
. . . . . . . . 9
   |
32 | 30, 31 | syl 14 |
. . . . . . . 8
   |
33 | | ordelss 4261 |
. . . . . . . 8
     |
34 | 32, 33 | sylan 279 |
. . . . . . 7
 
   |
35 | 12 | adantr 272 |
. . . . . . 7
 
    |
36 | 34, 35 | sseqtr4d 3102 |
. . . . . 6
 
    |
37 | | fun2ssres 5124 |
. . . . . 6
  recs   recs    recs        |
38 | 24, 16, 36, 37 | mp3an2ani 1305 |
. . . . 5
 
 recs        |
39 | 38 | fveq2d 5379 |
. . . 4
 
    recs             |
40 | 23, 28, 39 | 3eqtr3d 2155 |
. . 3
 
               |
41 | 40 | ralrimiva 2479 |
. 2
                |
42 | | fveq2 5375 |
. . . 4
             |
43 | | reseq2 4772 |
. . . . 5
  
      |
44 | 43 | fveq2d 5379 |
. . . 4
                 |
45 | 42, 44 | eqeq12d 2129 |
. . 3
                             |
46 | 45 | cbvralv 2628 |
. 2
 
           

              |
47 | 41, 46 | sylibr 133 |
1
                |