Step | Hyp | Ref
| Expression |
1 | | df-rab 2765 |
. . . . . 6
       
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
2 | | dfsbcq 3257 |
. . . . . . . . . . 11
  
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
3 | 2 | cbvrexv 3006 |
. . . . . . . . . 10
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
4 | 3 | anbi2i 708 |
. . . . . . . . 9
           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
5 | | r19.42v 2931 |
. . . . . . . . 9
           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
6 | 4, 5 | bitr4i 260 |
. . . . . . . 8
           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)            ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
7 | | simpll 768 |
. . . . . . . . . . . . . 14
   
         |
8 | | simpr 468 |
. . . . . . . . . . . . . 14
   
               |
9 | | simplr 770 |
. . . . . . . . . . . . . 14
   
         |
10 | | rexrabdioph.1 |
. . . . . . . . . . . . . . 15
   |
11 | 10 | mapfzcons 35629 |
. . . . . . . . . . . . . 14
 
                      |
12 | 7, 8, 9, 11 | syl3anc 1292 |
. . . . . . . . . . . . 13
   
                      |
13 | 12 | adantrr 731 |
. . . . . . . . . . . 12
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                  |
14 | 10 | mapfzcons2 35632 |
. . . . . . . . . . . . . . . . 17
       
              |
15 | 8, 9, 14 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
   
                    |
16 | 15 | eqcomd 2477 |
. . . . . . . . . . . . . . 15
   
                    |
17 | 10 | mapfzcons1 35630 |
. . . . . . . . . . . . . . . . . 18
                      |
18 | 17 | adantl 473 |
. . . . . . . . . . . . . . . . 17
   
                      |
19 | 18 | eqcomd 2477 |
. . . . . . . . . . . . . . . 16
   
                      |
20 | 19 | sbceq1d 3260 |
. . . . . . . . . . . . . . 15
   
          ![]. ].](_drbrack.gif)
               ![]. ].](_drbrack.gif)    |
21 | 16, 20 | sbceqbid 3262 |
. . . . . . . . . . . . . 14
   
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
             ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)    |
22 | 21 | biimpd 212 |
. . . . . . . . . . . . 13
   
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)              ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)    |
23 | 22 | impr 631 |
. . . . . . . . . . . 12
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)   |
24 | 19 | adantrr 731 |
. . . . . . . . . . . 12
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                  |
25 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
                         |
26 | | reseq1 5105 |
. . . . . . . . . . . . . . . 16
                             |
27 | 26 | sbceq1d 3260 |
. . . . . . . . . . . . . . 15
                 ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)    |
28 | 25, 27 | sbceqbid 3262 |
. . . . . . . . . . . . . 14
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)              ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)    |
29 | 26 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
              
                |
30 | 28, 29 | anbi12d 725 |
. . . . . . . . . . . . 13
                ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                      ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)                  |
31 | 30 | rspcev 3136 |
. . . . . . . . . . . 12
                             ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)                               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)          |
32 | 13, 23, 24, 31 | syl12anc 1290 |
. . . . . . . . . . 11
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                  ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)          |
33 | 32 | ex 441 |
. . . . . . . . . 10
 
           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
              ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)           |
34 | 33 | rexlimdva 2871 |
. . . . . . . . 9

           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)           |
35 | | elmapi 7511 |
. . . . . . . . . . . . . 14
                 |
36 | | nn0p1nn 10933 |
. . . . . . . . . . . . . . . 16

    |
37 | 10, 36 | syl5eqel 2553 |
. . . . . . . . . . . . . . 15

  |
38 | | elfz1end 11855 |
. . . . . . . . . . . . . . 15

      |
39 | 37, 38 | sylib 201 |
. . . . . . . . . . . . . 14

      |
40 | | ffvelrn 6035 |
. . . . . . . . . . . . . 14
              
      |
41 | 35, 39, 40 | syl2anr 486 |
. . . . . . . . . . . . 13
 
             |
42 | 41 | adantr 472 |
. . . . . . . . . . . 12
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)               |
43 | | simprr 774 |
. . . . . . . . . . . . 13
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)         
       |
44 | 10 | mapfzcons1cl 35631 |
. . . . . . . . . . . . . 14
                     |
45 | 44 | ad2antlr 741 |
. . . . . . . . . . . . 13
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                       |
46 | 43, 45 | eqeltrd 2549 |
. . . . . . . . . . . 12
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                 |
47 | | simprl 772 |
. . . . . . . . . . . . 13
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)   |
48 | | dfsbcq 3257 |
. . . . . . . . . . . . . . 15
        
 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)    |
49 | 48 | sbcbidv 3310 |
. . . . . . . . . . . . . 14
              ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)    |
50 | 49 | ad2antll 743 |
. . . . . . . . . . . . 13
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)    |
51 | 47, 50 | mpbird 240 |
. . . . . . . . . . . 12
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)               ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
52 | | dfsbcq 3257 |
. . . . . . . . . . . . . 14
      
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
53 | 52 | anbi2d 718 |
. . . . . . . . . . . . 13
               ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
54 | 53 | rspcev 3136 |
. . . . . . . . . . . 12
                   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)             ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
55 | 42, 46, 51, 54 | syl12anc 1290 |
. . . . . . . . . . 11
                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
56 | 55 | ex 441 |
. . . . . . . . . 10
 
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)        
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
57 | 56 | rexlimdva 2871 |
. . . . . . . . 9

                ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)       
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
58 | 34, 57 | impbid 195 |
. . . . . . . 8

           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)           |
59 | 6, 58 | syl5bb 265 |
. . . . . . 7

           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)                 ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)           |
60 | 59 | abbidv 2589 |
. . . . . 6

           ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
              ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)           |
61 | 1, 60 | syl5eq 2517 |
. . . . 5

       
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
              ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)           |
62 | | nfcv 2612 |
. . . . . 6
  
      |
63 | | nfcv 2612 |
. . . . . 6
  
      |
64 | | nfv 1769 |
. . . . . 6
    |
65 | | nfcv 2612 |
. . . . . . 7
   |
66 | | nfcv 2612 |
. . . . . . . 8
   |
67 | | nfsbc1v 3275 |
. . . . . . . 8
  
 ![]. ].](_drbrack.gif)  |
68 | 66, 67 | nfsbc 3277 |
. . . . . . 7
  
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  |
69 | 65, 68 | nfrex 2848 |
. . . . . 6
  
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  |
70 | | sbceq1a 3266 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)    |
71 | 70 | rexbidv 2892 |
. . . . . . 7
  
   ![]. ].](_drbrack.gif)    |
72 | | nfv 1769 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)  |
73 | | nfsbc1v 3275 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  |
74 | | sbceq1a 3266 |
. . . . . . . 8
  
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
75 | 72, 73, 74 | cbvrex 3002 |
. . . . . . 7
    ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
76 | 71, 75 | syl6bb 269 |
. . . . . 6
  
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
77 | 62, 63, 64, 69, 76 | cbvrab 3029 |
. . . . 5
                   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
78 | | fveq1 5878 |
. . . . . . . 8
           |
79 | | reseq1 5105 |
. . . . . . . . 9
               |
80 | 79 | sbceq1d 3260 |
. . . . . . . 8
          ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)    |
81 | 78, 80 | sbceqbid 3262 |
. . . . . . 7
        ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)    |
82 | 81 | rexrab 3190 |
. . . . . 6
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)   
     
              ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)          |
83 | 82 | abbii 2587 |
. . . . 5
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                          ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)          |
84 | 61, 77, 83 | 3eqtr4g 2530 |
. . . 4

                        ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)            |
85 | | fvex 5889 |
. . . . . . . . 9
     |
86 | | vex 3034 |
. . . . . . . . . 10
 |
87 | 86 | resex 5154 |
. . . . . . . . 9
       |
88 | | rexrabdioph.2 |
. . . . . . . . . 10
         |
89 | | rexrabdioph.3 |
. . . . . . . . . 10
           |
90 | 88, 89 | sylan9bb 714 |
. . . . . . . . 9
     
       
   |
91 | 85, 87, 90 | sbc2ie 3323 |
. . . . . . . 8
       ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)   |
92 | 91 | a1i 11 |
. . . . . . 7
              ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)    |
93 | 92 | rabbiia 3019 |
. . . . . 6
             ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif) 
         |
94 | 93 | rexeqi 2978 |
. . . . 5
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)   
     
         
       |
95 | 94 | abbii 2587 |
. . . 4
               ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)                             |
96 | 84, 95 | syl6eq 2521 |
. . 3

                             |
97 | 96 | adantr 472 |
. 2
          Dioph   
                            |
98 | | simpl 464 |
. . 3
          Dioph  
  |
99 | | nn0z 10984 |
. . . . . 6

  |
100 | | uzid 11197 |
. . . . . 6
       |
101 | | peano2uz 11235 |
. . . . . 6
    
        |
102 | 99, 100, 101 | 3syl 18 |
. . . . 5

        |
103 | 10, 102 | syl5eqel 2553 |
. . . 4

      |
104 | 103 | adantr 472 |
. . 3
          Dioph  
      |
105 | | simpr 468 |
. . 3
          Dioph           Dioph    |
106 | | diophrex 35689 |
. . 3
 
            Dioph    
                Dioph    |
107 | 98, 104, 105, 106 | syl3anc 1292 |
. 2
          Dioph    
                Dioph    |
108 | 97, 107 | eqeltrd 2549 |
1
          Dioph   
        Dioph    |