Step | Hyp | Ref
| Expression |
1 | | zfz1isolem1.xz |
. . . . . 6

  |
2 | 1 | ssdifssd 3274 |
. . . . 5
       |
3 | | zfz1isolem1.xf |
. . . . . 6
   |
4 | | zfz1isolem1.mx |
. . . . . 6
   |
5 | | diffisn 6893 |
. . . . . 6
 
       |
6 | 3, 4, 5 | syl2anc 411 |
. . . . 5
       |
7 | | zfz1isolem1.k |
. . . . . 6
   |
8 | | zfz1isolem1.xs |
. . . . . 6
   |
9 | | dif1en 6879 |
. . . . . 6
 
       |
10 | 7, 8, 4, 9 | syl3anc 1238 |
. . . . 5
       |
11 | 2, 6, 10 | jca31 309 |
. . . 4
      
            |
12 | | zfz1isolem1.h |
. . . . 5
      
      ♯        |
13 | | sseq1 3179 |
. . . . . . . . . 10
             |
14 | | eleq1 2240 |
. . . . . . . . . 10
             |
15 | 13, 14 | anbi12d 473 |
. . . . . . . . 9
                     |
16 | | breq1 4007 |
. . . . . . . . 9
             |
17 | 15, 16 | anbi12d 473 |
. . . . . . . 8
       
 
                   |
18 | | fveq2 5516 |
. . . . . . . . . . . 12
     ♯  ♯        |
19 | 18 | oveq2d 5891 |
. . . . . . . . . . 11
        ♯      ♯         |
20 | | isoeq4 5805 |
. . . . . . . . . . 11
    ♯      ♯            ♯         ♯            |
21 | 19, 20 | syl 14 |
. . . . . . . . . 10
          ♯         ♯            |
22 | | isoeq5 5806 |
. . . . . . . . . 10
          ♯        
    ♯                |
23 | 21, 22 | bitrd 188 |
. . . . . . . . 9
          ♯         ♯                |
24 | 23 | exbidv 1825 |
. . . . . . . 8
           ♯    

    ♯                |
25 | 17, 24 | imbi12d 234 |
. . . . . . 7
        
  
    ♯     
               
      ♯                 |
26 | 25 | spcgv 2825 |
. . . . . 6
            

    ♯                       
    ♯                 |
27 | 6, 26 | syl 14 |
. . . . 5
        

    ♯                       
    ♯                 |
28 | 12, 27 | mpd 13 |
. . . 4
                  
    ♯                |
29 | 11, 28 | mpd 13 |
. . 3
      ♯               |
30 | | isoeq1 5802 |
. . . 4
 
    ♯            
    ♯                |
31 | 30 | cbvexv 1918 |
. . 3
      ♯            

    ♯               |
32 | 29, 31 | sylib 122 |
. 2
      ♯               |
33 | | df-isom 5226 |
. . . . . . . . 9
     ♯                   ♯            
    ♯            ♯        
            |
34 | 33 | biimpi 120 |
. . . . . . . 8
     ♯                   ♯             
   ♯        
   ♯        
            |
35 | 34 | adantl 277 |
. . . . . . 7
 
    ♯                    ♯             
   ♯        
   ♯        
            |
36 | 35 | simpld 112 |
. . . . . 6
 
    ♯                   ♯               |
37 | | hashcl 10761 |
. . . . . . . . 9
 ♯    |
38 | 3, 37 | syl 14 |
. . . . . . . 8
 ♯    |
39 | 38 | adantr 276 |
. . . . . . 7
 
    ♯              ♯    |
40 | 4 | adantr 276 |
. . . . . . 7
 
    ♯                |
41 | | f1osng 5503 |
. . . . . . 7
  ♯     ♯        ♯         |
42 | 39, 40, 41 | syl2anc 411 |
. . . . . 6
 
    ♯                ♯        ♯         |
43 | | hashdifsn 10799 |
. . . . . . . . . . . . 13
 
 ♯       ♯     |
44 | 3, 4, 43 | syl2anc 411 |
. . . . . . . . . . . 12
 ♯       ♯     |
45 | 44 | oveq1d 5890 |
. . . . . . . . . . 11
  ♯         ♯      |
46 | 38 | nn0cnd 9231 |
. . . . . . . . . . . 12
 ♯    |
47 | | 1cnd 7973 |
. . . . . . . . . . . 12
   |
48 | 46, 47 | npcand 8272 |
. . . . . . . . . . 11
   ♯    ♯    |
49 | 45, 48 | eqtrd 2210 |
. . . . . . . . . 10
  ♯       ♯    |
50 | 49 | sneqd 3606 |
. . . . . . . . 9
   ♯         ♯     |
51 | 50 | ineq2d 3337 |
. . . . . . . 8
     ♯         ♯             ♯        ♯      |
52 | | fzp1disj 10080 |
. . . . . . . 8
    ♯         ♯          |
53 | 51, 52 | eqtr3di 2225 |
. . . . . . 7
     ♯        ♯      |
54 | 53 | adantr 276 |
. . . . . 6
 
    ♯                  ♯        ♯      |
55 | | incom 3328 |
. . . . . . . 8
           
     |
56 | | disjdif 3496 |
. . . . . . . 8
         |
57 | 55, 56 | eqtri 2198 |
. . . . . . 7
         |
58 | 57 | a1i 9 |
. . . . . 6
 
    ♯                  
     |
59 | | f1oun 5482 |
. . . . . 6
        ♯            
  ♯        ♯             ♯        ♯        
        ♯            ♯        ♯                |
60 | 36, 42, 54, 58, 59 | syl22anc 1239 |
. . . . 5
 
    ♯                 ♯            ♯        ♯                |
61 | 3, 4 | zfz1isolemsplit 10818 |
. . . . . . 7
    ♯       ♯        ♯      |
62 | | fidifsnid 6871 |
. . . . . . . . 9
 
           |
63 | 3, 4, 62 | syl2anc 411 |
. . . . . . . 8
           |
64 | 63 | eqcomd 2183 |
. . . . . . 7
           |
65 | | f1oeq23 5453 |
. . . . . . 7
     ♯       ♯        ♯            
    ♯           ♯        ♯            ♯        ♯                 |
66 | 61, 64, 65 | syl2anc 411 |
. . . . . 6
     ♯           ♯    
   ♯            ♯        ♯                 |
67 | 66 | adantr 276 |
. . . . 5
 
    ♯                  ♯           ♯        ♯            ♯        ♯                 |
68 | 60, 67 | mpbird 167 |
. . . 4
 
    ♯                 ♯           ♯       |
69 | 3 | ad2antrr 488 |
. . . . . 6
       ♯                  ♯  
   ♯    
  |
70 | 1 | ad2antrr 488 |
. . . . . 6
       ♯                  ♯  
   ♯    
  |
71 | 4 | ad2antrr 488 |
. . . . . 6
       ♯                  ♯  
   ♯    
  |
72 | | zfz1isolem1.m |
. . . . . . 7
    |
73 | 72 | ad2antrr 488 |
. . . . . 6
       ♯                  ♯  
   ♯    

  |
74 | | simplr 528 |
. . . . . 6
       ♯                  ♯  
   ♯    
    ♯               |
75 | | simprl 529 |
. . . . . 6
       ♯                  ♯  
   ♯    
   ♯     |
76 | | simprr 531 |
. . . . . 6
       ♯                  ♯  
   ♯    
   ♯     |
77 | 69, 70, 71, 73, 74, 75, 76 | zfz1isolemiso 10819 |
. . . . 5
       ♯                  ♯  
   ♯    
     ♯        
    ♯            |
78 | 77 | ralrimivva 2559 |
. . . 4
 
    ♯                  ♯        ♯    
    ♯        
    ♯            |
79 | | df-isom 5226 |
. . . 4
    ♯          ♯         ♯           ♯         ♯    
   ♯    
    ♯        
    ♯             |
80 | 68, 78, 79 | sylanbrc 417 |
. . 3
 
    ♯                 ♯          ♯       |
81 | | vex 2741 |
. . . . . . 7
 |
82 | 81 | a1i 9 |
. . . . . 6
   |
83 | | opexg 4229 |
. . . . . . . 8
  ♯    ♯      |
84 | 38, 4, 83 | syl2anc 411 |
. . . . . . 7
  ♯   
  |
85 | | snexg 4185 |
. . . . . . 7
  ♯   
  ♯       |
86 | 84, 85 | syl 14 |
. . . . . 6
   ♯       |
87 | | unexg 4444 |
. . . . . 6
    ♯         ♯        |
88 | 82, 86, 87 | syl2anc 411 |
. . . . 5
    ♯        |
89 | | isoeq1 5802 |
. . . . . 6
    ♯           ♯        ♯          ♯        |
90 | 89 | spcegv 2826 |
. . . . 5
    ♯          ♯          ♯    

    ♯        |
91 | 88, 90 | syl 14 |
. . . 4
     ♯          ♯    

    ♯        |
92 | 91 | adantr 276 |
. . 3
 
    ♯                  ♯          ♯    

    ♯        |
93 | 80, 92 | mpd 13 |
. 2
 
    ♯                   ♯       |
94 | 32, 93 | exlimddv 1898 |
1
      ♯       |