Proof of Theorem icorempt2
Step | Hyp | Ref
| Expression |
1 | | icorempt2.1 |
. 2
|
2 | | df-ico 12181 |
. . . 4
|
3 | 2 | reseq1i 5392 |
. . 3
|
4 | | ressxr 10083 |
. . . 4
|
5 | | resmpt2 6758 |
. . . 4
|
6 | 4, 4, 5 | mp2an 708 |
. . 3
|
7 | 3, 6 | eqtri 2644 |
. 2
|
8 | | nfv 1843 |
. . . 4
|
9 | | nfrab1 3122 |
. . . 4
|
10 | | nfrab1 3122 |
. . . 4
|
11 | | rabid 3116 |
. . . . . . . 8
|
12 | | rexr 10085 |
. . . . . . . . . . . . . . . . 17
|
13 | | nltmnf 11963 |
. . . . . . . . . . . . . . . . 17
|
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . 16
|
15 | | renemnf 10088 |
. . . . . . . . . . . . . . . . 17
|
16 | 15 | neneqd 2799 |
. . . . . . . . . . . . . . . 16
|
17 | 14, 16 | jca 554 |
. . . . . . . . . . . . . . 15
|
18 | | pm4.56 516 |
. . . . . . . . . . . . . . 15
|
19 | 17, 18 | sylib 208 |
. . . . . . . . . . . . . 14
|
20 | | mnfxr 10096 |
. . . . . . . . . . . . . . 15
|
21 | | xrleloe 11977 |
. . . . . . . . . . . . . . 15
|
22 | 12, 20, 21 | sylancl 694 |
. . . . . . . . . . . . . 14
|
23 | 19, 22 | mtbird 315 |
. . . . . . . . . . . . 13
|
24 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
25 | 24 | notbid 308 |
. . . . . . . . . . . . 13
|
26 | 23, 25 | syl5ibrcom 237 |
. . . . . . . . . . . 12
|
27 | 26 | con2d 129 |
. . . . . . . . . . 11
|
28 | | rexr 10085 |
. . . . . . . . . . . 12
|
29 | | pnfnlt 11962 |
. . . . . . . . . . . . . 14
|
30 | | breq1 4656 |
. . . . . . . . . . . . . . 15
|
31 | 30 | notbid 308 |
. . . . . . . . . . . . . 14
|
32 | 29, 31 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
|
33 | 32 | con2d 129 |
. . . . . . . . . . . 12
|
34 | 28, 33 | syl 17 |
. . . . . . . . . . 11
|
35 | 27, 34 | im2anan9 880 |
. . . . . . . . . 10
|
36 | 35 | anim2d 589 |
. . . . . . . . 9
|
37 | | renepnf 10087 |
. . . . . . . . . . . 12
|
38 | 37 | neneqd 2799 |
. . . . . . . . . . 11
|
39 | 38 | pm4.71i 664 |
. . . . . . . . . 10
|
40 | | xrnemnf 11951 |
. . . . . . . . . . . 12
|
41 | 40 | anbi1i 731 |
. . . . . . . . . . 11
|
42 | | df-ne 2795 |
. . . . . . . . . . . . 13
|
43 | 42 | anbi2i 730 |
. . . . . . . . . . . 12
|
44 | 43 | anbi1i 731 |
. . . . . . . . . . 11
|
45 | | pm5.61 749 |
. . . . . . . . . . 11
|
46 | 41, 44, 45 | 3bitr3i 290 |
. . . . . . . . . 10
|
47 | | anass 681 |
. . . . . . . . . 10
|
48 | 39, 46, 47 | 3bitr2ri 289 |
. . . . . . . . 9
|
49 | 36, 48 | syl6ib 241 |
. . . . . . . 8
|
50 | 11, 49 | syl5bi 232 |
. . . . . . 7
|
51 | 11 | simprbi 480 |
. . . . . . . 8
|
52 | 51 | a1i 11 |
. . . . . . 7
|
53 | 50, 52 | jcad 555 |
. . . . . 6
|
54 | | rabid 3116 |
. . . . . 6
|
55 | 53, 54 | syl6ibr 242 |
. . . . 5
|
56 | | rabss2 3685 |
. . . . . . 7
|
57 | 4, 56 | ax-mp 5 |
. . . . . 6
|
58 | 57 | sseli 3599 |
. . . . 5
|
59 | 55, 58 | impbid1 215 |
. . . 4
|
60 | 8, 9, 10, 59 | eqrd 3622 |
. . 3
|
61 | 60 | mpt2eq3ia 6720 |
. 2
|
62 | 1, 7, 61 | 3eqtri 2648 |
1
|