Step | Hyp | Ref
| Expression |
1 | | zfz1isolem1.xz |
. . . . . 6
|
2 | 1 | ssdifssd 3184 |
. . . . 5
|
3 | | zfz1isolem1.xf |
. . . . . 6
|
4 | | zfz1isolem1.mx |
. . . . . 6
|
5 | | diffisn 6755 |
. . . . . 6
|
6 | 3, 4, 5 | syl2anc 408 |
. . . . 5
|
7 | | zfz1isolem1.k |
. . . . . 6
|
8 | | zfz1isolem1.xs |
. . . . . 6
|
9 | | dif1en 6741 |
. . . . . 6
|
10 | 7, 8, 4, 9 | syl3anc 1201 |
. . . . 5
|
11 | 2, 6, 10 | jca31 307 |
. . . 4
|
12 | | zfz1isolem1.h |
. . . . 5
♯ |
13 | | sseq1 3090 |
. . . . . . . . . 10
|
14 | | eleq1 2180 |
. . . . . . . . . 10
|
15 | 13, 14 | anbi12d 464 |
. . . . . . . . 9
|
16 | | breq1 3902 |
. . . . . . . . 9
|
17 | 15, 16 | anbi12d 464 |
. . . . . . . 8
|
18 | | fveq2 5389 |
. . . . . . . . . . . 12
♯ ♯ |
19 | 18 | oveq2d 5758 |
. . . . . . . . . . 11
♯ ♯ |
20 | | isoeq4 5673 |
. . . . . . . . . . 11
♯ ♯ ♯ ♯ |
21 | 19, 20 | syl 14 |
. . . . . . . . . 10
♯ ♯ |
22 | | isoeq5 5674 |
. . . . . . . . . 10
♯
♯ |
23 | 21, 22 | bitrd 187 |
. . . . . . . . 9
♯ ♯ |
24 | 23 | exbidv 1781 |
. . . . . . . 8
♯
♯ |
25 | 17, 24 | imbi12d 233 |
. . . . . . 7
♯
♯ |
26 | 25 | spcgv 2747 |
. . . . . 6
♯
♯ |
27 | 6, 26 | syl 14 |
. . . . 5
♯
♯ |
28 | 12, 27 | mpd 13 |
. . . 4
♯ |
29 | 11, 28 | mpd 13 |
. . 3
♯ |
30 | | isoeq1 5670 |
. . . 4
♯
♯ |
31 | 30 | cbvexv 1872 |
. . 3
♯
♯ |
32 | 29, 31 | sylib 121 |
. 2
♯ |
33 | | df-isom 5102 |
. . . . . . . . 9
♯ ♯
♯ ♯
|
34 | 33 | biimpi 119 |
. . . . . . . 8
♯ ♯
♯
♯
|
35 | 34 | adantl 275 |
. . . . . . 7
♯ ♯
♯
♯
|
36 | 35 | simpld 111 |
. . . . . 6
♯ ♯ |
37 | | hashcl 10482 |
. . . . . . . . 9
♯ |
38 | 3, 37 | syl 14 |
. . . . . . . 8
♯ |
39 | 38 | adantr 274 |
. . . . . . 7
♯ ♯ |
40 | 4 | adantr 274 |
. . . . . . 7
♯ |
41 | | f1osng 5376 |
. . . . . . 7
♯ ♯ ♯ |
42 | 39, 40, 41 | syl2anc 408 |
. . . . . 6
♯ ♯ ♯ |
43 | | fzp1disj 9815 |
. . . . . . . 8
♯ ♯ |
44 | | hashdifsn 10520 |
. . . . . . . . . . . . 13
♯ ♯ |
45 | 3, 4, 44 | syl2anc 408 |
. . . . . . . . . . . 12
♯ ♯ |
46 | 45 | oveq1d 5757 |
. . . . . . . . . . 11
♯ ♯ |
47 | 38 | nn0cnd 8990 |
. . . . . . . . . . . 12
♯ |
48 | | 1cnd 7750 |
. . . . . . . . . . . 12
|
49 | 47, 48 | npcand 8045 |
. . . . . . . . . . 11
♯ ♯ |
50 | 46, 49 | eqtrd 2150 |
. . . . . . . . . 10
♯ ♯ |
51 | 50 | sneqd 3510 |
. . . . . . . . 9
♯ ♯ |
52 | 51 | ineq2d 3247 |
. . . . . . . 8
♯ ♯ ♯ ♯ |
53 | 43, 52 | syl5reqr 2165 |
. . . . . . 7
♯ ♯ |
54 | 53 | adantr 274 |
. . . . . 6
♯ ♯ ♯ |
55 | | incom 3238 |
. . . . . . . 8
|
56 | | disjdif 3405 |
. . . . . . . 8
|
57 | 55, 56 | eqtri 2138 |
. . . . . . 7
|
58 | 57 | a1i 9 |
. . . . . 6
♯
|
59 | | f1oun 5355 |
. . . . . 6
♯
♯ ♯ ♯ ♯
♯ ♯ ♯ |
60 | 36, 42, 54, 58, 59 | syl22anc 1202 |
. . . . 5
♯ ♯ ♯ ♯ |
61 | 3, 4 | zfz1isolemsplit 10536 |
. . . . . . 7
♯ ♯ ♯ |
62 | | fidifsnid 6733 |
. . . . . . . . 9
|
63 | 3, 4, 62 | syl2anc 408 |
. . . . . . . 8
|
64 | 63 | eqcomd 2123 |
. . . . . . 7
|
65 | | f1oeq23 5329 |
. . . . . . 7
♯ ♯ ♯
♯ ♯ ♯ ♯ ♯ |
66 | 61, 64, 65 | syl2anc 408 |
. . . . . 6
♯ ♯
♯ ♯ ♯ |
67 | 66 | adantr 274 |
. . . . 5
♯ ♯ ♯ ♯ ♯ ♯ |
68 | 60, 67 | mpbird 166 |
. . . 4
♯ ♯ ♯ |
69 | 3 | ad2antrr 479 |
. . . . . 6
♯ ♯
♯
|
70 | 1 | ad2antrr 479 |
. . . . . 6
♯ ♯
♯
|
71 | 4 | ad2antrr 479 |
. . . . . 6
♯ ♯
♯
|
72 | | zfz1isolem1.m |
. . . . . . 7
|
73 | 72 | ad2antrr 479 |
. . . . . 6
♯ ♯
♯
|
74 | | simplr 504 |
. . . . . 6
♯ ♯
♯
♯ |
75 | | simprl 505 |
. . . . . 6
♯ ♯
♯
♯ |
76 | | simprr 506 |
. . . . . 6
♯ ♯
♯
♯ |
77 | 69, 70, 71, 73, 74, 75, 76 | zfz1isolemiso 10537 |
. . . . 5
♯ ♯
♯
♯
♯ |
78 | 77 | ralrimivva 2491 |
. . . 4
♯ ♯ ♯
♯
♯ |
79 | | df-isom 5102 |
. . . 4
♯ ♯ ♯ ♯ ♯
♯
♯
♯ |
80 | 68, 78, 79 | sylanbrc 413 |
. . 3
♯ ♯ ♯ |
81 | | vex 2663 |
. . . . . . 7
|
82 | 81 | a1i 9 |
. . . . . 6
|
83 | | opexg 4120 |
. . . . . . . 8
♯ ♯ |
84 | 38, 4, 83 | syl2anc 408 |
. . . . . . 7
♯
|
85 | | snexg 4078 |
. . . . . . 7
♯
♯ |
86 | 84, 85 | syl 14 |
. . . . . 6
♯ |
87 | | unexg 4334 |
. . . . . 6
♯ ♯ |
88 | 82, 86, 87 | syl2anc 408 |
. . . . 5
♯ |
89 | | isoeq1 5670 |
. . . . . 6
♯ ♯ ♯ ♯ |
90 | 89 | spcegv 2748 |
. . . . 5
♯ ♯ ♯
♯ |
91 | 88, 90 | syl 14 |
. . . 4
♯ ♯
♯ |
92 | 91 | adantr 274 |
. . 3
♯ ♯ ♯
♯ |
93 | 80, 92 | mpd 13 |
. 2
♯ ♯ |
94 | 32, 93 | exlimddv 1854 |
1
♯ |