Proof of Theorem tfrlemibxssdm
Step | Hyp | Ref
| Expression |
1 | | tfrlemi1.5 |
. . 3
|
2 | | tfrlemi1.4 |
. . . 4
|
3 | | tfrlemisucfn.2 |
. . . . . . . . . . . 12
|
4 | 3 | tfrlem3-2d 5951 |
. . . . . . . . . . 11
|
5 | 4 | simprd 112 |
. . . . . . . . . 10
|
6 | 5 | 3ad2ant1 959 |
. . . . . . . . 9
|
7 | | vex 2604 |
. . . . . . . . . . . . 13
|
8 | | opexg 3983 |
. . . . . . . . . . . . 13
|
9 | 7, 5, 8 | sylancr 405 |
. . . . . . . . . . . 12
|
10 | | snidg 3423 |
. . . . . . . . . . . 12
|
11 | | elun2 3140 |
. . . . . . . . . . . 12
|
12 | 9, 10, 11 | 3syl 17 |
. . . . . . . . . . 11
|
13 | 12 | 3ad2ant1 959 |
. . . . . . . . . 10
|
14 | | simp2r 965 |
. . . . . . . . . . . 12
|
15 | | simp3l 966 |
. . . . . . . . . . . 12
|
16 | | onelon 4139 |
. . . . . . . . . . . . . . 15
|
17 | | rspe 2412 |
. . . . . . . . . . . . . . 15
|
18 | 16, 17 | sylan 277 |
. . . . . . . . . . . . . 14
|
19 | | tfrlemisucfn.1 |
. . . . . . . . . . . . . . 15
|
20 | | vex 2604 |
. . . . . . . . . . . . . . 15
|
21 | 19, 20 | tfrlem3a 5948 |
. . . . . . . . . . . . . 14
|
22 | 18, 21 | sylibr 132 |
. . . . . . . . . . . . 13
|
23 | 22 | 3adant1 956 |
. . . . . . . . . . . 12
|
24 | 14, 15, 23 | 3jca 1118 |
. . . . . . . . . . 11
|
25 | | snexg 3956 |
. . . . . . . . . . . . . 14
|
26 | | unexg 4196 |
. . . . . . . . . . . . . . 15
|
27 | 20, 26 | mpan 414 |
. . . . . . . . . . . . . 14
|
28 | 9, 25, 27 | 3syl 17 |
. . . . . . . . . . . . 13
|
29 | | isset 2605 |
. . . . . . . . . . . . 13
|
30 | 28, 29 | sylib 120 |
. . . . . . . . . . . 12
|
31 | 30 | 3ad2ant1 959 |
. . . . . . . . . . 11
|
32 | | simpr3 946 |
. . . . . . . . . . . . . . 15
|
33 | | 19.8a 1522 |
. . . . . . . . . . . . . . . 16
|
34 | | rspe 2412 |
. . . . . . . . . . . . . . . . 17
|
35 | | tfrlemi1.3 |
. . . . . . . . . . . . . . . . . 18
|
36 | 35 | abeq2i 2189 |
. . . . . . . . . . . . . . . . 17
|
37 | 34, 36 | sylibr 132 |
. . . . . . . . . . . . . . . 16
|
38 | 33, 37 | sylan2 280 |
. . . . . . . . . . . . . . 15
|
39 | 32, 38 | eqeltrrd 2156 |
. . . . . . . . . . . . . 14
|
40 | 39 | 3exp2 1156 |
. . . . . . . . . . . . 13
|
41 | 40 | 3imp 1132 |
. . . . . . . . . . . 12
|
42 | 41 | exlimdv 1740 |
. . . . . . . . . . 11
|
43 | 24, 31, 42 | sylc 61 |
. . . . . . . . . 10
|
44 | | elunii 3606 |
. . . . . . . . . 10
|
45 | 13, 43, 44 | syl2anc 403 |
. . . . . . . . 9
|
46 | | opeq2 3571 |
. . . . . . . . . . . 12
|
47 | 46 | eleq1d 2147 |
. . . . . . . . . . 11
|
48 | 47 | spcegv 2686 |
. . . . . . . . . 10
|
49 | 7 | eldm2 4551 |
. . . . . . . . . 10
|
50 | 48, 49 | syl6ibr 160 |
. . . . . . . . 9
|
51 | 6, 45, 50 | sylc 61 |
. . . . . . . 8
|
52 | 51 | 3expia 1140 |
. . . . . . 7
|
53 | 52 | exlimdv 1740 |
. . . . . 6
|
54 | 53 | anassrs 392 |
. . . . 5
|
55 | 54 | ralimdva 2429 |
. . . 4
|
56 | 2, 55 | mpdan 412 |
. . 3
|
57 | 1, 56 | mpd 13 |
. 2
|
58 | | dfss3 2989 |
. 2
|
59 | 57, 58 | sylibr 132 |
1
|