Step | Hyp | Ref
| Expression |
1 | | suplocsrlem.ss |
. . . . . . . 8
|
2 | | suplocsrlem.c |
. . . . . . . 8
|
3 | 1, 2 | sseldd 3098 |
. . . . . . 7
|
4 | | 0idsr 7575 |
. . . . . . 7
|
5 | 3, 4 | syl 14 |
. . . . . 6
|
6 | 5, 2 | eqeltrd 2216 |
. . . . 5
|
7 | | 1pr 7362 |
. . . . 5
|
8 | 6, 7 | jctil 310 |
. . . 4
|
9 | | opeq1 3705 |
. . . . . . . . 9
|
10 | 9 | eceq1d 6465 |
. . . . . . . 8
|
11 | | df-0r 7539 |
. . . . . . . 8
|
12 | 10, 11 | syl6eqr 2190 |
. . . . . . 7
|
13 | 12 | oveq2d 5790 |
. . . . . 6
|
14 | 13 | eleq1d 2208 |
. . . . 5
|
15 | | suplocsrlem.b |
. . . . 5
|
16 | 14, 15 | elrab2 2843 |
. . . 4
|
17 | 8, 16 | sylibr 133 |
. . 3
|
18 | | elex2 2702 |
. . 3
|
19 | 17, 18 | syl 14 |
. 2
|
20 | | suplocsrlem.ub |
. . . 4
|
21 | | breq1 3932 |
. . . . . . . . . 10
|
22 | 21 | rspccv 2786 |
. . . . . . . . 9
|
23 | 2, 22 | mpan9 279 |
. . . . . . . 8
|
24 | | 0lt1sr 7573 |
. . . . . . . . . . . . . 14
|
25 | | 0r 7558 |
. . . . . . . . . . . . . . 15
|
26 | | 1sr 7559 |
. . . . . . . . . . . . . . 15
|
27 | | m1r 7560 |
. . . . . . . . . . . . . . 15
|
28 | | ltasrg 7578 |
. . . . . . . . . . . . . . 15
|
29 | 25, 26, 27, 28 | mp3an 1315 |
. . . . . . . . . . . . . 14
|
30 | 24, 29 | mpbi 144 |
. . . . . . . . . . . . 13
|
31 | | 0idsr 7575 |
. . . . . . . . . . . . . 14
|
32 | 27, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
|
33 | | m1p1sr 7568 |
. . . . . . . . . . . . 13
|
34 | 30, 32, 33 | 3brtr3i 3957 |
. . . . . . . . . . . 12
|
35 | | ltasrg 7578 |
. . . . . . . . . . . . 13
|
36 | 27, 25, 3, 35 | mp3an12i 1319 |
. . . . . . . . . . . 12
|
37 | 34, 36 | mpbii 147 |
. . . . . . . . . . 11
|
38 | 37, 5 | breqtrd 3954 |
. . . . . . . . . 10
|
39 | | ltsosr 7572 |
. . . . . . . . . . 11
|
40 | | ltrelsr 7546 |
. . . . . . . . . . 11
|
41 | 39, 40 | sotri 4934 |
. . . . . . . . . 10
|
42 | 38, 41 | sylan 281 |
. . . . . . . . 9
|
43 | | map2psrprg 7613 |
. . . . . . . . . . 11
|
44 | 3, 43 | syl 14 |
. . . . . . . . . 10
|
45 | 44 | adantr 274 |
. . . . . . . . 9
|
46 | 42, 45 | mpbid 146 |
. . . . . . . 8
|
47 | 23, 46 | syldan 280 |
. . . . . . 7
|
48 | | breq1 3932 |
. . . . . . . . . . 11
|
49 | | simpllr 523 |
. . . . . . . . . . . . 13
|
50 | | breq2 3933 |
. . . . . . . . . . . . . . 15
|
51 | 50 | ralbidv 2437 |
. . . . . . . . . . . . . 14
|
52 | 51 | adantl 275 |
. . . . . . . . . . . . 13
|
53 | 49, 52 | mpbird 166 |
. . . . . . . . . . . 12
|
54 | 53 | adantr 274 |
. . . . . . . . . . 11
|
55 | 15 | rabeq2i 2683 |
. . . . . . . . . . . . 13
|
56 | 55 | simprbi 273 |
. . . . . . . . . . . 12
|
57 | 56 | adantl 275 |
. . . . . . . . . . 11
|
58 | 48, 54, 57 | rspcdva 2794 |
. . . . . . . . . 10
|
59 | 58 | ralrimiva 2505 |
. . . . . . . . 9
|
60 | 59 | ex 114 |
. . . . . . . 8
|
61 | 60 | reximdva 2534 |
. . . . . . 7
|
62 | 47, 61 | mpd 13 |
. . . . . 6
|
63 | 62 | ex 114 |
. . . . 5
|
64 | 63 | rexlimdvw 2553 |
. . . 4
|
65 | 20, 64 | mpd 13 |
. . 3
|
66 | | elrabi 2837 |
. . . . . . . 8
|
67 | | opeq1 3705 |
. . . . . . . . . . . . 13
|
68 | 67 | eceq1d 6465 |
. . . . . . . . . . . 12
|
69 | 68 | oveq2d 5790 |
. . . . . . . . . . 11
|
70 | 69 | eleq1d 2208 |
. . . . . . . . . 10
|
71 | 70 | cbvrabv 2685 |
. . . . . . . . 9
|
72 | 15, 71 | eqtri 2160 |
. . . . . . . 8
|
73 | 66, 72 | eleq2s 2234 |
. . . . . . 7
|
74 | 73 | adantl 275 |
. . . . . 6
|
75 | | simplr 519 |
. . . . . 6
|
76 | 3 | ad2antrr 479 |
. . . . . 6
|
77 | | ltpsrprg 7611 |
. . . . . 6
|
78 | 74, 75, 76, 77 | syl3anc 1216 |
. . . . 5
|
79 | 78 | ralbidva 2433 |
. . . 4
|
80 | 79 | rexbidva 2434 |
. . 3
|
81 | 65, 80 | mpbid 146 |
. 2
|
82 | | suplocsrlem.loc |
. . 3
|
83 | 15, 1, 2, 20, 82 | suplocsrlemb 7614 |
. 2
|
84 | 19, 81, 83 | suplocexpr 7533 |
1
|