Proof of Theorem tfrlemibxssdm
Step | Hyp | Ref
| Expression |
1 | | tfrlemi1.5 |
. . 3
|
2 | | tfrlemi1.4 |
. . . 4
|
3 | | tfrlemisucfn.2 |
. . . . . . . . . . . 12
|
4 | 3 | tfrlem3-2d 6303 |
. . . . . . . . . . 11
|
5 | 4 | simprd 114 |
. . . . . . . . . 10
|
6 | 5 | 3ad2ant1 1018 |
. . . . . . . . 9
|
7 | | vex 2738 |
. . . . . . . . . . . . 13
|
8 | | opexg 4222 |
. . . . . . . . . . . . 13
|
9 | 7, 5, 8 | sylancr 414 |
. . . . . . . . . . . 12
|
10 | | snidg 3618 |
. . . . . . . . . . . 12
|
11 | | elun2 3301 |
. . . . . . . . . . . 12
|
12 | 9, 10, 11 | 3syl 17 |
. . . . . . . . . . 11
|
13 | 12 | 3ad2ant1 1018 |
. . . . . . . . . 10
|
14 | | simp2r 1024 |
. . . . . . . . . . . 12
|
15 | | simp3l 1025 |
. . . . . . . . . . . 12
|
16 | | onelon 4378 |
. . . . . . . . . . . . . . 15
|
17 | | rspe 2524 |
. . . . . . . . . . . . . . 15
|
18 | 16, 17 | sylan 283 |
. . . . . . . . . . . . . 14
|
19 | | tfrlemisucfn.1 |
. . . . . . . . . . . . . . 15
|
20 | | vex 2738 |
. . . . . . . . . . . . . . 15
|
21 | 19, 20 | tfrlem3a 6301 |
. . . . . . . . . . . . . 14
|
22 | 18, 21 | sylibr 134 |
. . . . . . . . . . . . 13
|
23 | 22 | 3adant1 1015 |
. . . . . . . . . . . 12
|
24 | 14, 15, 23 | 3jca 1177 |
. . . . . . . . . . 11
|
25 | | snexg 4179 |
. . . . . . . . . . . . . 14
|
26 | | unexg 4437 |
. . . . . . . . . . . . . . 15
|
27 | 20, 26 | mpan 424 |
. . . . . . . . . . . . . 14
|
28 | 9, 25, 27 | 3syl 17 |
. . . . . . . . . . . . 13
|
29 | | isset 2741 |
. . . . . . . . . . . . 13
|
30 | 28, 29 | sylib 122 |
. . . . . . . . . . . 12
|
31 | 30 | 3ad2ant1 1018 |
. . . . . . . . . . 11
|
32 | | simpr3 1005 |
. . . . . . . . . . . . . . 15
|
33 | | 19.8a 1588 |
. . . . . . . . . . . . . . . 16
|
34 | | rspe 2524 |
. . . . . . . . . . . . . . . . 17
|
35 | | tfrlemi1.3 |
. . . . . . . . . . . . . . . . . 18
|
36 | 35 | abeq2i 2286 |
. . . . . . . . . . . . . . . . 17
|
37 | 34, 36 | sylibr 134 |
. . . . . . . . . . . . . . . 16
|
38 | 33, 37 | sylan2 286 |
. . . . . . . . . . . . . . 15
|
39 | 32, 38 | eqeltrrd 2253 |
. . . . . . . . . . . . . 14
|
40 | 39 | 3exp2 1225 |
. . . . . . . . . . . . 13
|
41 | 40 | 3imp 1193 |
. . . . . . . . . . . 12
|
42 | 41 | exlimdv 1817 |
. . . . . . . . . . 11
|
43 | 24, 31, 42 | sylc 62 |
. . . . . . . . . 10
|
44 | | elunii 3810 |
. . . . . . . . . 10
|
45 | 13, 43, 44 | syl2anc 411 |
. . . . . . . . 9
|
46 | | opeq2 3775 |
. . . . . . . . . . . 12
|
47 | 46 | eleq1d 2244 |
. . . . . . . . . . 11
|
48 | 47 | spcegv 2823 |
. . . . . . . . . 10
|
49 | 7 | eldm2 4818 |
. . . . . . . . . 10
|
50 | 48, 49 | syl6ibr 162 |
. . . . . . . . 9
|
51 | 6, 45, 50 | sylc 62 |
. . . . . . . 8
|
52 | 51 | 3expia 1205 |
. . . . . . 7
|
53 | 52 | exlimdv 1817 |
. . . . . 6
|
54 | 53 | anassrs 400 |
. . . . 5
|
55 | 54 | ralimdva 2542 |
. . . 4
|
56 | 2, 55 | mpdan 421 |
. . 3
|
57 | 1, 56 | mpd 13 |
. 2
|
58 | | dfss3 3143 |
. 2
|
59 | 57, 58 | sylibr 134 |
1
|