Step | Hyp | Ref
| Expression |
1 | | zfz1isolem1.xz |
. . . . . 6
|
2 | 1 | ssdifssd 3209 |
. . . . 5
|
3 | | zfz1isolem1.xf |
. . . . . 6
|
4 | | zfz1isolem1.mx |
. . . . . 6
|
5 | | diffisn 6780 |
. . . . . 6
|
6 | 3, 4, 5 | syl2anc 408 |
. . . . 5
|
7 | | zfz1isolem1.k |
. . . . . 6
|
8 | | zfz1isolem1.xs |
. . . . . 6
|
9 | | dif1en 6766 |
. . . . . 6
|
10 | 7, 8, 4, 9 | syl3anc 1216 |
. . . . 5
|
11 | 2, 6, 10 | jca31 307 |
. . . 4
|
12 | | zfz1isolem1.h |
. . . . 5
♯ |
13 | | sseq1 3115 |
. . . . . . . . . 10
|
14 | | eleq1 2200 |
. . . . . . . . . 10
|
15 | 13, 14 | anbi12d 464 |
. . . . . . . . 9
|
16 | | breq1 3927 |
. . . . . . . . 9
|
17 | 15, 16 | anbi12d 464 |
. . . . . . . 8
|
18 | | fveq2 5414 |
. . . . . . . . . . . 12
♯ ♯ |
19 | 18 | oveq2d 5783 |
. . . . . . . . . . 11
♯ ♯ |
20 | | isoeq4 5698 |
. . . . . . . . . . 11
♯ ♯ ♯ ♯ |
21 | 19, 20 | syl 14 |
. . . . . . . . . 10
♯ ♯ |
22 | | isoeq5 5699 |
. . . . . . . . . 10
♯
♯ |
23 | 21, 22 | bitrd 187 |
. . . . . . . . 9
♯ ♯ |
24 | 23 | exbidv 1797 |
. . . . . . . 8
♯
♯ |
25 | 17, 24 | imbi12d 233 |
. . . . . . 7
♯
♯ |
26 | 25 | spcgv 2768 |
. . . . . 6
♯
♯ |
27 | 6, 26 | syl 14 |
. . . . 5
♯
♯ |
28 | 12, 27 | mpd 13 |
. . . 4
♯ |
29 | 11, 28 | mpd 13 |
. . 3
♯ |
30 | | isoeq1 5695 |
. . . 4
♯
♯ |
31 | 30 | cbvexv 1890 |
. . 3
♯
♯ |
32 | 29, 31 | sylib 121 |
. 2
♯ |
33 | | df-isom 5127 |
. . . . . . . . 9
♯ ♯
♯ ♯
|
34 | 33 | biimpi 119 |
. . . . . . . 8
♯ ♯
♯
♯
|
35 | 34 | adantl 275 |
. . . . . . 7
♯ ♯
♯
♯
|
36 | 35 | simpld 111 |
. . . . . 6
♯ ♯ |
37 | | hashcl 10520 |
. . . . . . . . 9
♯ |
38 | 3, 37 | syl 14 |
. . . . . . . 8
♯ |
39 | 38 | adantr 274 |
. . . . . . 7
♯ ♯ |
40 | 4 | adantr 274 |
. . . . . . 7
♯ |
41 | | f1osng 5401 |
. . . . . . 7
♯ ♯ ♯ |
42 | 39, 40, 41 | syl2anc 408 |
. . . . . 6
♯ ♯ ♯ |
43 | | fzp1disj 9853 |
. . . . . . . 8
♯ ♯ |
44 | | hashdifsn 10558 |
. . . . . . . . . . . . 13
♯ ♯ |
45 | 3, 4, 44 | syl2anc 408 |
. . . . . . . . . . . 12
♯ ♯ |
46 | 45 | oveq1d 5782 |
. . . . . . . . . . 11
♯ ♯ |
47 | 38 | nn0cnd 9025 |
. . . . . . . . . . . 12
♯ |
48 | | 1cnd 7775 |
. . . . . . . . . . . 12
|
49 | 47, 48 | npcand 8070 |
. . . . . . . . . . 11
♯ ♯ |
50 | 46, 49 | eqtrd 2170 |
. . . . . . . . . 10
♯ ♯ |
51 | 50 | sneqd 3535 |
. . . . . . . . 9
♯ ♯ |
52 | 51 | ineq2d 3272 |
. . . . . . . 8
♯ ♯ ♯ ♯ |
53 | 43, 52 | syl5reqr 2185 |
. . . . . . 7
♯ ♯ |
54 | 53 | adantr 274 |
. . . . . 6
♯ ♯ ♯ |
55 | | incom 3263 |
. . . . . . . 8
|
56 | | disjdif 3430 |
. . . . . . . 8
|
57 | 55, 56 | eqtri 2158 |
. . . . . . 7
|
58 | 57 | a1i 9 |
. . . . . 6
♯
|
59 | | f1oun 5380 |
. . . . . 6
♯
♯ ♯ ♯ ♯
♯ ♯ ♯ |
60 | 36, 42, 54, 58, 59 | syl22anc 1217 |
. . . . 5
♯ ♯ ♯ ♯ |
61 | 3, 4 | zfz1isolemsplit 10574 |
. . . . . . 7
♯ ♯ ♯ |
62 | | fidifsnid 6758 |
. . . . . . . . 9
|
63 | 3, 4, 62 | syl2anc 408 |
. . . . . . . 8
|
64 | 63 | eqcomd 2143 |
. . . . . . 7
|
65 | | f1oeq23 5354 |
. . . . . . 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 519 |
. . . . . 6
♯ ♯
♯
♯ |
75 | | simprl 520 |
. . . . . 6
♯ ♯
♯
♯ |
76 | | simprr 521 |
. . . . . 6
♯ ♯
♯
♯ |
77 | 69, 70, 71, 73, 74, 75, 76 | zfz1isolemiso 10575 |
. . . . 5
♯ ♯
♯
♯
♯ |
78 | 77 | ralrimivva 2512 |
. . . 4
♯ ♯ ♯
♯
♯ |
79 | | df-isom 5127 |
. . . 4
♯ ♯ ♯ ♯ ♯
♯
♯
♯ |
80 | 68, 78, 79 | sylanbrc 413 |
. . 3
♯ ♯ ♯ |
81 | | vex 2684 |
. . . . . . 7
|
82 | 81 | a1i 9 |
. . . . . 6
|
83 | | opexg 4145 |
. . . . . . . 8
♯ ♯ |
84 | 38, 4, 83 | syl2anc 408 |
. . . . . . 7
♯
|
85 | | snexg 4103 |
. . . . . . 7
♯
♯ |
86 | 84, 85 | syl 14 |
. . . . . 6
♯ |
87 | | unexg 4359 |
. . . . . 6
♯ ♯ |
88 | 82, 86, 87 | syl2anc 408 |
. . . . 5
♯ |
89 | | isoeq1 5695 |
. . . . . 6
♯ ♯ ♯ ♯ |
90 | 89 | spcegv 2769 |
. . . . 5
♯ ♯ ♯
♯ |
91 | 88, 90 | syl 14 |
. . . 4
♯ ♯
♯ |
92 | 91 | adantr 274 |
. . 3
♯ ♯ ♯
♯ |
93 | 80, 92 | mpd 13 |
. 2
♯ ♯ |
94 | 32, 93 | exlimddv 1870 |
1
♯ |