Step | Hyp | Ref
| Expression |
1 | | simprlr 773 |
. . . . . . . . . . . 12
 
 
                   |
2 | | simprll 772 |
. . . . . . . . . . . . 13
 
 
               |
3 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
4 | 3 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
               |
5 | 4 | eleq1d 2513 |
. . . . . . . . . . . . . . 15
                 |
6 | 5 | rabbidv 3036 |
. . . . . . . . . . . . . 14
                   |
7 | | vitali.6 |
. . . . . . . . . . . . . 14
           |
8 | | reex 9630 |
. . . . . . . . . . . . . . 15
 |
9 | 8 | rabex 4554 |
. . . . . . . . . . . . . 14
         |
10 | 6, 7, 9 | fvmpt 5948 |
. . . . . . . . . . . . 13
               |
11 | 2, 10 | syl 17 |
. . . . . . . . . . . 12
 
 
                           |
12 | 1, 11 | eleqtrd 2531 |
. . . . . . . . . . 11
 
 
                       |
13 | | oveq1 6297 |
. . . . . . . . . . . . 13
               |
14 | 13 | eleq1d 2513 |
. . . . . . . . . . . 12
                 |
15 | 14 | elrab 3196 |
. . . . . . . . . . 11
        
          |
16 | 12, 15 | sylib 200 |
. . . . . . . . . 10
 
 
              
        |
17 | 16 | simpld 461 |
. . . . . . . . 9
 
 
               |
18 | 17 | recnd 9669 |
. . . . . . . 8
 
 
               |
19 | | vitali.5 |
. . . . . . . . . . . . 13
         ![[,] [,]](_icc.gif)     |
20 | | f1of 5814 |
. . . . . . . . . . . . 13
         ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)     |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
         ![[,] [,]](_icc.gif)     |
22 | | inss1 3652 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)    |
23 | | fss 5737 |
. . . . . . . . . . . 12
          ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)  
       |
24 | 21, 22, 23 | sylancl 668 |
. . . . . . . . . . 11
       |
25 | 24 | adantr 467 |
. . . . . . . . . 10
 
 
                   |
26 | 25, 2 | ffvelrnd 6023 |
. . . . . . . . 9
 
 
                   |
27 | | qcn 11278 |
. . . . . . . . 9
           |
28 | 26, 27 | syl 17 |
. . . . . . . 8
 
 
                   |
29 | | simprrl 774 |
. . . . . . . . . 10
 
 
               |
30 | 25, 29 | ffvelrnd 6023 |
. . . . . . . . 9
 
 
                   |
31 | | qcn 11278 |
. . . . . . . . 9
           |
32 | 30, 31 | syl 17 |
. . . . . . . 8
 
 
                   |
33 | | vitali.1 |
. . . . . . . . . . . . 13
   
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        |
34 | 33 | vitalilem1 22566 |
. . . . . . . . . . . 12
  ![[,] [,]](_icc.gif)   |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
 
 
               ![[,] [,]](_icc.gif)    |
36 | | vitali.2 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)    |
37 | | vitali.3 |
. . . . . . . . . . . . . . . . 17
   |
38 | | vitali.4 |
. . . . . . . . . . . . . . . . 17
          |
39 | | vitali.7 |
. . . . . . . . . . . . . . . . 17
      |
40 | 33, 36, 37, 38, 19, 7, 39 | vitalilem2 22567 |
. . . . . . . . . . . . . . . 16
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)     |
41 | 40 | simp1d 1020 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
42 | 41 | adantr 467 |
. . . . . . . . . . . . . 14
 
 
               ![[,] [,]](_icc.gif)    |
43 | 16 | simprd 465 |
. . . . . . . . . . . . . 14
 
 
                     |
44 | 42, 43 | sseldd 3433 |
. . . . . . . . . . . . 13
 
 
                     ![[,] [,]](_icc.gif)    |
45 | | simprrr 775 |
. . . . . . . . . . . . . . . . 17
 
 
                   |
46 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
47 | 46 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
               |
48 | 47 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . 20
                 |
49 | 48 | rabbidv 3036 |
. . . . . . . . . . . . . . . . . . 19
                   |
50 | 8 | rabex 4554 |
. . . . . . . . . . . . . . . . . . 19
         |
51 | 49, 7, 50 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . 18
               |
52 | 29, 51 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
 
                           |
53 | 45, 52 | eleqtrd 2531 |
. . . . . . . . . . . . . . . 16
 
 
                       |
54 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . 18
               |
55 | 54 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
                 |
56 | 55 | elrab 3196 |
. . . . . . . . . . . . . . . 16
        
          |
57 | 53, 56 | sylib 200 |
. . . . . . . . . . . . . . 15
 
 
              
        |
58 | 57 | simprd 465 |
. . . . . . . . . . . . . 14
 
 
                     |
59 | 42, 58 | sseldd 3433 |
. . . . . . . . . . . . 13
 
 
                     ![[,] [,]](_icc.gif)    |
60 | 44, 59 | jca 535 |
. . . . . . . . . . . 12
 
 
                      ![[,] [,]](_icc.gif)  
       ![[,] [,]](_icc.gif)     |
61 | 18, 28, 32 | nnncan1d 10020 |
. . . . . . . . . . . . 13
 
 
                                       |
62 | | qsubcl 11283 |
. . . . . . . . . . . . . 14
                       |
63 | 30, 26, 62 | syl2anc 667 |
. . . . . . . . . . . . 13
 
 
                         |
64 | 61, 63 | eqeltrd 2529 |
. . . . . . . . . . . 12
 
 
                             |
65 | | oveq12 6299 |
. . . . . . . . . . . . . 14
       
                         |
66 | 65 | eleq1d 2513 |
. . . . . . . . . . . . 13
       
                 
         |
67 | 66, 33 | brab2ga 4910 |
. . . . . . . . . . . 12
                       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                    |
68 | 60, 64, 67 | sylanbrc 670 |
. . . . . . . . . . 11
 
 
                           |
69 | 35, 68 | erthi 7410 |
. . . . . . . . . 10
 
 
                              |
70 | 69 | fveq2d 5869 |
. . . . . . . . 9
 
 
                                     |
71 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
       
      |
72 | 71 | eceq1d 7400 |
. . . . . . . . . . . . . . . 16
                 |
73 | 72 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
            
           |
74 | 73, 71 | eqeq12d 2466 |
. . . . . . . . . . . . . 14
             
                     |
75 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
76 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ![[,] [,]](_icc.gif)   |
77 | | erex 7387 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)     |
78 | 34, 76, 77 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
79 | 78 | ecelqsi 7419 |
. . . . . . . . . . . . . . . . . . . . 21
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)  
  |
80 | 79, 36 | syl6eleqr 2540 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif)      |
81 | 80 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)       |
82 | 38 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)   

       |
83 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
84 | | erdm 7373 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    |
85 | 34, 84 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
  ![[,] [,]](_icc.gif)   |
86 | 85 | eleq2i 2521 |
. . . . . . . . . . . . . . . . . . . . 21

  ![[,] [,]](_icc.gif)    |
87 | | ecdmn0 7406 |
. . . . . . . . . . . . . . . . . . . . 21

    |
88 | 86, 87 | bitr3i 255 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif) 
    |
89 | 83, 88 | sylib 200 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)       |
90 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . . 21
  
      |
91 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
  
           |
92 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
  
   |
93 | 91, 92 | eleq12d 2523 |
. . . . . . . . . . . . . . . . . . . . 21
  
    
    
    |
94 | 90, 93 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
  
      
             |
95 | 94 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . 19
    

    
             |
96 | 81, 82, 89, 95 | syl3c 63 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)           |
97 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . 19
      |
98 | | vex 3048 |
. . . . . . . . . . . . . . . . . . 19
 |
99 | 97, 98 | elec 7403 |
. . . . . . . . . . . . . . . . . 18
               |
100 | 96, 99 | sylib 200 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)          |
101 | 75, 100 | erthi 7410 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)             |
102 | 101 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)             |
103 | 102 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)            
       |
104 | 36, 74, 103 | ectocld 7430 |
. . . . . . . . . . . . 13
 
                |
105 | 104 | ralrimiva 2802 |
. . . . . . . . . . . 12
                 |
106 | | eceq1 7399 |
. . . . . . . . . . . . . . . 16
              |
107 | 106 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                     |
108 | | id 22 |
. . . . . . . . . . . . . . 15
           |
109 | 107, 108 | eqeq12d 2466 |
. . . . . . . . . . . . . 14
          
        
       |
110 | 109 | ralrn 6025 |
. . . . . . . . . . . . 13
  
     
                 |
111 | 37, 110 | syl 17 |
. . . . . . . . . . . 12
         
                |
112 | 105, 111 | mpbird 236 |
. . . . . . . . . . 11
          |
113 | 112 | adantr 467 |
. . . . . . . . . 10
 
 
                      |
114 | | eceq1 7399 |
. . . . . . . . . . . . 13
      
           |
115 | 114 | fveq2d 5869 |
. . . . . . . . . . . 12
      
    
             |
116 | | id 22 |
. . . . . . . . . . . 12
      

       |
117 | 115, 116 | eqeq12d 2466 |
. . . . . . . . . . 11
      
                          |
118 | 117 | rspcv 3146 |
. . . . . . . . . 10
                                   |
119 | 43, 113, 118 | sylc 62 |
. . . . . . . . 9
 
 
                                |
120 | | eceq1 7399 |
. . . . . . . . . . . . 13
      
           |
121 | 120 | fveq2d 5869 |
. . . . . . . . . . . 12
      
    
             |
122 | | id 22 |
. . . . . . . . . . . 12
      

       |
123 | 121, 122 | eqeq12d 2466 |
. . . . . . . . . . 11
      
                          |
124 | 123 | rspcv 3146 |
. . . . . . . . . 10
                                   |
125 | 58, 113, 124 | sylc 62 |
. . . . . . . . 9
 
 
                                |
126 | 70, 119, 125 | 3eqtr3d 2493 |
. . . . . . . 8
 
 
                           |
127 | 18, 28, 32, 126 | subcand 10027 |
. . . . . . 7
 
 
                       |
128 | 19 | adantr 467 |
. . . . . . . . 9
 
 
                     ![[,] [,]](_icc.gif)     |
129 | | f1of1 5813 |
. . . . . . . . 9
         ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)     |
130 | 128, 129 | syl 17 |
. . . . . . . 8
 
 
                     ![[,] [,]](_icc.gif)     |
131 | | f1fveq 6163 |
. . . . . . . 8
          ![[,] [,]](_icc.gif)                  |
132 | 130, 2, 29, 131 | syl12anc 1266 |
. . . . . . 7
 
 
                     
   |
133 | 127, 132 | mpbid 214 |
. . . . . 6
 
 
               |
134 | 133 | ex 436 |
. . . . 5
         
         |
135 | 134 | alrimivv 1774 |
. . . 4
             
         |
136 | | eleq1 2517 |
. . . . . 6
 
   |
137 | | fveq2 5865 |
. . . . . . 7
           |
138 | 137 | eleq2d 2514 |
. . . . . 6
     
       |
139 | 136, 138 | anbi12d 717 |
. . . . 5
                 |
140 | 139 | mo4 2346 |
. . . 4
        
      
           
   |
141 | 135, 140 | sylibr 216 |
. . 3
           |
142 | 141 | alrimiv 1773 |
. 2
             |
143 | | dfdisj2 4375 |
. 2
Disj    
            |
144 | 142, 143 | sylibr 216 |
1
 Disj
      |