Proof of Theorem tfrlem9
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | visset 1350 |
. . 3
    |
| 2 | 1 | eldm2 2528 |
. 2
          |
| 3 | | tfrlem.2 |
. . . . . . 7
   |
| 4 | | tfrlem.1 |
. . . . . . . 8
   
        |
| 5 | 4 | unieqi 1928 |
. . . . . . 7
|
| 6 | 3, 5 | eqtr 1119 |
. . . . . 6
|
| 7 | 6 | eleq2i 1153 |
. . . . 5
|
| 8 | | eluniab 1926 |
. . . . 5
|
| 9 | 7, 8 | bitr 151 |
. . . 4
|
| 10 | | visset 1350 |
. . . . . . . . . . . . . . 15
|
| 11 | 1, 10 | fnop 2727 |
. . . . . . . . . . . . . 14
 |
| 12 | | ra4e 1244 |
. . . . . . . . . . . . . . . . 17
|
| 13 | 4 | cleqabi 1176 |
. . . . . . . . . . . . . . . . . 18
|
| 14 | | elssuni 1940 |
. . . . . . . . . . . . . . . . . . 19
 |
| 15 | 14, 3 | syl6ssr 1547 |
. . . . . . . . . . . . . . . . . 18
|
| 16 | 13, 15 | sylbir 176 |
. . . . . . . . . . . . . . . . 17
|
| 17 | 12, 16 | syl 12 |
. . . . . . . . . . . . . . . 16
|
| 18 | | ra4 1243 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 19 | 18 | com12 13 |
. . . . . . . . . . . . . . . . . . . 20
|
| 20 | | fndm 2723 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 21 | 20 | eleq2d 1156 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 22 | 4, 3 | tfrlem7 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
| 23 | | funssfv 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 24 | 23 | adantrl 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 25 | | fun2ssres 2699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 26 | 25 | fveq2d 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 27 | 20 | eleq1d 1155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 28 | | onelsst 2255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 29 | 27, 28 | syl6bir 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 30 | 29 | imp31 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 31 | 26, 30 | sylan2 346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 32 | 24, 31 | cleq12d 1115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 33 | 22, 32 | mpan11 529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 34 | 33 | biimprd 136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 35 | 34 | exp 291 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 36 | 35 | com3l 34 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 37 | 36 | exp31 293 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 38 | 37 | com34 36 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 39 | 38 | com24 37 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 40 | 21, 39 | sylbird 180 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 41 | 40 | com3l 34 |
. . . . . . . . . . . . . . . . . . . 20
|
| 42 | 19, 41 | syld 27 |
. . . . . . . . . . . . . . . . . . 19
|
| 43 | 42 | com24 37 |
. . . . . . . . . . . . . . . . . 18
|
| 44 | 43 | imp4d 285 |
. . . . . . . . . . . . . . . . 17
|
| 45 | 44 | com13 33 |
. . . . . . . . . . . . . . . 16
|
| 46 | 17, 45 | mpcom 49 |
. . . . . . . . . . . . . . 15
|
| 47 | 46 | com12 13 |
. . . . . . . . . . . . . 14
|
| 48 | 11, 47 | syl 12 |
. . . . . . . . . . . . 13
|
| 49 | 48 | exp4d 298 |
. . . . . . . . . . . 12
|
Home