Step | Hyp | Ref
| Expression |
1 | | elmapi 7460 |
. . . 4
|
2 | | compss.a |
. . . . . 6
|
3 | 2 | isf34lem7 8780 |
. . . . 5
|
4 | 3 | 3expia 1198 |
. . . 4
|
5 | 1, 4 | sylan2 474 |
. . 3
|
6 | 5 | ralrimiva 2871 |
. 2
|
7 | | elmapex 7459 |
. . . . . . . . . . 11
|
8 | 7 | simpld 459 |
. . . . . . . . . 10
|
9 | | pwexb 6611 |
. . . . . . . . . 10
|
10 | 8, 9 | sylibr 212 |
. . . . . . . . 9
|
11 | 2 | isf34lem2 8774 |
. . . . . . . . 9
|
12 | 10, 11 | syl 16 |
. . . . . . . 8
|
13 | | elmapi 7460 |
. . . . . . . 8
|
14 | | fco 5746 |
. . . . . . . 8
|
15 | 12, 13, 14 | syl2anc 661 |
. . . . . . 7
|
16 | | elmapg 7452 |
. . . . . . . 8
|
17 | 7, 16 | syl 16 |
. . . . . . 7
|
18 | 15, 17 | mpbird 232 |
. . . . . 6
|
19 | | fveq1 5870 |
. . . . . . . . . 10
|
20 | | fveq1 5870 |
. . . . . . . . . 10
|
21 | 19, 20 | sseq12d 3532 |
. . . . . . . . 9
|
22 | 21 | ralbidv 2896 |
. . . . . . . 8
|
23 | | rneq 5233 |
. . . . . . . . . . 11
|
24 | | rnco2 5519 |
. . . . . . . . . . 11
|
25 | 23, 24 | syl6eq 2514 |
. . . . . . . . . 10
|
26 | 25 | unieqd 4259 |
. . . . . . . . 9
|
27 | 26, 25 | eleq12d 2539 |
. . . . . . . 8
|
28 | 22, 27 | imbi12d 320 |
. . . . . . 7
|
29 | 28 | rspccv 3207 |
. . . . . 6
|
30 | 18, 29 | syl5 32 |
. . . . 5
|
31 | | sscon 3637 |
. . . . . . . . 9
|
32 | 10 | adantr 465 |
. . . . . . . . . . 11
|
33 | 13 | ffvelrnda 6031 |
. . . . . . . . . . . 12
|
34 | 33 | elpwid 4022 |
. . . . . . . . . . 11
|
35 | 2 | isf34lem1 8773 |
. . . . . . . . . . 11
|
36 | 32, 34, 35 | syl2anc 661 |
. . . . . . . . . 10
|
37 | | peano2 6720 |
. . . . . . . . . . . . 13
|
38 | | ffvelrn 6029 |
. . . . . . . . . . . . 13
|
39 | 13, 37, 38 | syl2an 477 |
. . . . . . . . . . . 12
|
40 | 39 | elpwid 4022 |
. . . . . . . . . . 11
|
41 | 2 | isf34lem1 8773 |
. . . . . . . . . . 11
|
42 | 32, 40, 41 | syl2anc 661 |
. . . . . . . . . 10
|
43 | 36, 42 | sseq12d 3532 |
. . . . . . . . 9
|
44 | 31, 43 | syl5ibr 221 |
. . . . . . . 8
|
45 | | fvco3 5950 |
. . . . . . . . . 10
|
46 | 13, 45 | sylan 471 |
. . . . . . . . 9
|
47 | | fvco3 5950 |
. . . . . . . . . 10
|
48 | 13, 37, 47 | syl2an 477 |
. . . . . . . . 9
|
49 | 46, 48 | sseq12d 3532 |
. . . . . . . 8
|
50 | 44, 49 | sylibrd 234 |
. . . . . . 7
|
51 | 50 | ralimdva 2865 |
. . . . . 6
|
52 | | ffn 5736 |
. . . . . . . . 9
|
53 | 12, 52 | syl 16 |
. . . . . . . 8
|
54 | | imassrn 5353 |
. . . . . . . . 9
|
55 | | frn 5742 |
. . . . . . . . . 10
|
56 | 12, 55 | syl 16 |
. . . . . . . . 9
|
57 | 54, 56 | syl5ss 3514 |
. . . . . . . 8
|
58 | | fnfvima 6150 |
. . . . . . . . 9
|
59 | 58 | 3expia 1198 |
. . . . . . . 8
|
60 | 53, 57, 59 | syl2anc 661 |
. . . . . . 7
|
61 | | incom 3690 |
. . . . . . . . . . . . 13
|
62 | | frn 5742 |
. . . . . . . . . . . . . . . 16
|
63 | 13, 62 | syl 16 |
. . . . . . . . . . . . . . 15
|
64 | | fdm 5740 |
. . . . . . . . . . . . . . . 16
|
65 | 12, 64 | syl 16 |
. . . . . . . . . . . . . . 15
|
66 | 63, 65 | sseqtr4d 3540 |
. . . . . . . . . . . . . 14
|
67 | | df-ss 3489 |
. . . . . . . . . . . . . 14
|
68 | 66, 67 | sylib 196 |
. . . . . . . . . . . . 13
|
69 | 61, 68 | syl5eq 2510 |
. . . . . . . . . . . 12
|
70 | | fdm 5740 |
. . . . . . . . . . . . . . 15
|
71 | 13, 70 | syl 16 |
. . . . . . . . . . . . . 14
|
72 | | peano1 6719 |
. . . . . . . . . . . . . . 15
|
73 | | ne0i 3790 |
. . . . . . . . . . . . . . 15
|
74 | 72, 73 | mp1i 12 |
. . . . . . . . . . . . . 14
|
75 | 71, 74 | eqnetrd 2750 |
. . . . . . . . . . . . 13
|
76 | | dm0rn0 5224 |
. . . . . . . . . . . . . 14
|
77 | 76 | necon3bii 2725 |
. . . . . . . . . . . . 13
|
78 | 75, 77 | sylib 196 |
. . . . . . . . . . . 12
|
79 | 69, 78 | eqnetrd 2750 |
. . . . . . . . . . 11
|
80 | | imadisj 5361 |
. . . . . . . . . . . 12
|
81 | 80 | necon3bii 2725 |
. . . . . . . . . . 11
|
82 | 79, 81 | sylibr 212 |
. . . . . . . . . 10
|
83 | 2 | isf34lem4 8778 |
. . . . . . . . . 10
|
84 | 10, 57, 82, 83 | syl12anc 1226 |
. . . . . . . . 9
|
85 | 2 | isf34lem3 8776 |
. . . . . . . . . . 11
|
86 | 10, 63, 85 | syl2anc 661 |
. . . . . . . . . 10
|
87 | 86 | inteqd 4291 |
. . . . . . . . 9
|
88 | 84, 87 | eqtrd 2498 |
. . . . . . . 8
|
89 | 88, 86 | eleq12d 2539 |
. . . . . . 7
|
90 | 60, 89 | sylibd 214 |
. . . . . 6
|
91 | 51, 90 | imim12d 74 |
. . . . 5
|
92 | 30, 91 | sylcom 29 |
. . . 4
|
93 | 92 | ralrimiv 2869 |
. . 3
|
94 | | isfin3-3 8769 |
. . 3
|
95 | 93, 94 | syl5ibr 221 |
. 2
|
96 | 6, 95 | impbid2 204 |
1
|