Proof of Theorem tfrlem11
Step | Hyp | Ref
| Expression |
1 | | elsuci 5791 |
. 2
recs
recs recs |
2 | | tfrlem.1 |
. . . . . . . . 9
|
3 | | tfrlem.3 |
. . . . . . . . 9
recs recs recs |
4 | 2, 3 | tfrlem10 7483 |
. . . . . . . 8
recs
recs |
5 | | fnfun 5988 |
. . . . . . . 8
recs |
6 | 4, 5 | syl 17 |
. . . . . . 7
recs
|
7 | | ssun1 3776 |
. . . . . . . . 9
recs
recs recs recs |
8 | 7, 3 | sseqtr4i 3638 |
. . . . . . . 8
recs
|
9 | 2 | tfrlem9 7481 |
. . . . . . . . 9
recs
recs recs
|
10 | | funssfv 6209 |
. . . . . . . . . . . 12
recs
recs recs |
11 | 10 | 3expa 1265 |
. . . . . . . . . . 11
recs
recs recs |
12 | 11 | adantrl 752 |
. . . . . . . . . 10
recs
recs recs recs |
13 | | onelss 5766 |
. . . . . . . . . . . 12
recs
recs recs |
14 | 13 | imp 445 |
. . . . . . . . . . 11
recs recs
recs |
15 | | fun2ssres 5931 |
. . . . . . . . . . . . 13
recs
recs recs
|
16 | 15 | 3expa 1265 |
. . . . . . . . . . . 12
recs
recs recs
|
17 | 16 | fveq2d 6195 |
. . . . . . . . . . 11
recs
recs recs |
18 | 14, 17 | sylan2 491 |
. . . . . . . . . 10
recs
recs recs
recs
|
19 | 12, 18 | eqeq12d 2637 |
. . . . . . . . 9
recs
recs recs recs recs |
20 | 9, 19 | syl5ibr 236 |
. . . . . . . 8
recs
recs recs recs |
21 | 8, 20 | mpanl2 717 |
. . . . . . 7
recs recs
recs |
22 | 6, 21 | sylan 488 |
. . . . . 6
recs recs recs
recs |
23 | 22 | exp32 631 |
. . . . 5
recs
recs recs
recs
|
24 | 23 | pm2.43i 52 |
. . . 4
recs
recs recs |
25 | 24 | pm2.43d 53 |
. . 3
recs
recs |
26 | | opex 4932 |
. . . . . . . . 9
|
27 | 26 | snid 4208 |
. . . . . . . 8
|
28 | | opeq1 4402 |
. . . . . . . . . . 11
recs
recs |
29 | 28 | adantl 482 |
. . . . . . . . . 10
recs recs
recs |
30 | | eqimss 3657 |
. . . . . . . . . . . . . 14
recs
recs |
31 | 8, 15 | mp3an2 1412 |
. . . . . . . . . . . . . 14
recs recs |
32 | 6, 30, 31 | syl2an 494 |
. . . . . . . . . . . . 13
recs recs
recs |
33 | | reseq2 5391 |
. . . . . . . . . . . . . . 15
recs
recs recs
recs |
34 | 2 | tfrlem6 7478 |
. . . . . . . . . . . . . . . 16
recs |
35 | | resdm 5441 |
. . . . . . . . . . . . . . . 16
recs recs recs recs |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
recs recs recs |
37 | 33, 36 | syl6eq 2672 |
. . . . . . . . . . . . . 14
recs
recs recs |
38 | 37 | adantl 482 |
. . . . . . . . . . . . 13
recs recs
recs recs |
39 | 32, 38 | eqtrd 2656 |
. . . . . . . . . . . 12
recs recs
recs |
40 | 39 | fveq2d 6195 |
. . . . . . . . . . 11
recs recs
recs |
41 | 40 | opeq2d 4409 |
. . . . . . . . . 10
recs recs
recs
recs recs |
42 | 29, 41 | eqtrd 2656 |
. . . . . . . . 9
recs recs
recs recs |
43 | 42 | sneqd 4189 |
. . . . . . . 8
recs recs
recs recs |
44 | 27, 43 | syl5eleq 2707 |
. . . . . . 7
recs recs
recs recs |
45 | | elun2 3781 |
. . . . . . 7
recs recs recs recs recs |
46 | 44, 45 | syl 17 |
. . . . . 6
recs recs
recs recs recs |
47 | 46, 3 | syl6eleqr 2712 |
. . . . 5
recs recs
|
48 | 4 | adantr 481 |
. . . . . 6
recs recs
recs |
49 | | simpr 477 |
. . . . . . 7
recs recs
recs |
50 | | sucidg 5803 |
. . . . . . . 8
recs
recs recs |
51 | 50 | adantr 481 |
. . . . . . 7
recs recs
recs recs |
52 | 49, 51 | eqeltrd 2701 |
. . . . . 6
recs recs
recs |
53 | | fnopfvb 6237 |
. . . . . 6
recs
recs
|
54 | 48, 52, 53 | syl2anc 693 |
. . . . 5
recs recs
|
55 | 47, 54 | mpbird 247 |
. . . 4
recs recs
|
56 | 55 | ex 450 |
. . 3
recs
recs |
57 | 25, 56 | jaod 395 |
. 2
recs
recs recs
|
58 | 1, 57 | syl5 34 |
1
recs
recs
|