Step | Hyp | Ref
| Expression |
1 | | isacs 15557 |
. 2
 ACS   Moore                           |
2 | | iunss 4319 |
. . . . . . . . 9
 
       
           |
3 | | ffun 5731 |
. . . . . . . . . . 11
         |
4 | | funiunfv 6153 |
. . . . . . . . . . 11

                   |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
                     
    |
6 | 5 | sseq1d 3459 |
. . . . . . . . 9
                            |
7 | 2, 6 | syl5rbbr 264 |
. . . . . . . 8
                            |
8 | 7 | bibi2d 320 |
. . . . . . 7
                 

             |
9 | 8 | ralbidv 2827 |
. . . . . 6
          
       
            
    |
10 | 9 | pm5.32i 643 |
. . . . 5
       
  
       
                         |
11 | 10 | exbii 1718 |
. . . 4
                      
         
          
    |
12 | | simpll 760 |
. . . . . . . . . . . . 13
   Moore      
Moore    |
13 | | inss1 3652 |
. . . . . . . . . . . . . . . 16
     |
14 | 13 | sseli 3428 |
. . . . . . . . . . . . . . 15
       |
15 | | elpwi 3960 |
. . . . . . . . . . . . . . 15
 
  |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
      |
17 | 16 | adantl 468 |
. . . . . . . . . . . . 13
   Moore      
  |
18 | | simplr 762 |
. . . . . . . . . . . . 13
   Moore         |
19 | | isacs2.f |
. . . . . . . . . . . . . 14
mrCls   |
20 | 19 | mrcsscl 15526 |
. . . . . . . . . . . . 13
  Moore         |
21 | 12, 17, 18, 20 | syl3anc 1268 |
. . . . . . . . . . . 12
   Moore          
  |
22 | 21 | ralrimiva 2802 |
. . . . . . . . . . 11
  Moore              |
23 | 22 | adantlr 721 |
. . . . . . . . . 10
   Moore   
            |
24 | 23 | adantllr 725 |
. . . . . . . . 9
    Moore         
          
    
            |
25 | | simplll 768 |
. . . . . . . . . . . . . . . . . 18
    Moore         
          
    
    Moore    |
26 | 16 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
    Moore         
          
    
      |
27 | | elpwi 3960 |
. . . . . . . . . . . . . . . . . . . 20
 
  |
28 | 27 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . 19
    Moore         
          
    
      |
29 | 26, 28 | sstrd 3442 |
. . . . . . . . . . . . . . . . . 18
    Moore         
          
    
      |
30 | 25, 19, 29 | mrcssidd 15531 |
. . . . . . . . . . . . . . . . 17
    Moore         
          
    
          |
31 | | vex 3048 |
. . . . . . . . . . . . . . . . . 18
 |
32 | 31 | elpw 3957 |
. . . . . . . . . . . . . . . . 17
     
      |
33 | 30, 32 | sylibr 216 |
. . . . . . . . . . . . . . . 16
    Moore         
          
    
           |
34 | | inss2 3653 |
. . . . . . . . . . . . . . . . . 18
    |
35 | 34 | sseli 3428 |
. . . . . . . . . . . . . . . . 17
      |
36 | 35 | adantl 468 |
. . . . . . . . . . . . . . . 16
    Moore         
          
    
      |
37 | 33, 36 | elind 3618 |
. . . . . . . . . . . . . . 15
    Moore         
          
    
             |
38 | 19 | mrccl 15517 |
. . . . . . . . . . . . . . . . 17
  Moore         |
39 | 25, 29, 38 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    Moore         
          
    
          |
40 | | mresspw 15498 |
. . . . . . . . . . . . . . . . . . 19
 Moore 
   |
41 | 40 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . 18
    Moore         
          
    
       |
42 | 41, 39 | sseldd 3433 |
. . . . . . . . . . . . . . . . 17
    Moore         
          
    
           |
43 | | simprr 766 |
. . . . . . . . . . . . . . . . . 18
  Moore        
  
                           |
44 | 43 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
    Moore         
          
    
                   |
45 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . 19
     
       |
46 | | pweq 3954 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
47 | 46 | ineq1d 3633 |
. . . . . . . . . . . . . . . . . . . 20
      
          |
48 | | sseq2 3454 |
. . . . . . . . . . . . . . . . . . . 20
         
           |
49 | 47, 48 | raleqbidv 3001 |
. . . . . . . . . . . . . . . . . . 19
      
 
     
                    |
50 | 45, 49 | bibi12d 323 |
. . . . . . . . . . . . . . . . . 18
               
     
                     |
51 | 50 | rspcva 3148 |
. . . . . . . . . . . . . . . . 17
                         
                    |
52 | 42, 44, 51 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    Moore         
          
    
                             |
53 | 39, 52 | mpbid 214 |
. . . . . . . . . . . . . . 15
    Moore         
          
    
                       |
54 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
55 | 54 | sseq1d 3459 |
. . . . . . . . . . . . . . . 16
     
   
           |
56 | 55 | rspcva 3148 |
. . . . . . . . . . . . . . 15
       
                  
          |
57 | 37, 53, 56 | syl2anc 667 |
. . . . . . . . . . . . . 14
    Moore         
          
    
              |
58 | | sstr2 3439 |
. . . . . . . . . . . . . 14
             
       |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
    Moore         
          
    
                |
60 | 59 | ralimdva 2796 |
. . . . . . . . . . . 12
   Moore        
  
               
 
     
        
   |
61 | 60 | imp 431 |
. . . . . . . . . . 11
    Moore         
          
             
            |
62 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
63 | 62 | sseq1d 3459 |
. . . . . . . . . . . 12
     
       |
64 | 63 | cbvralv 3019 |
. . . . . . . . . . 11
 
       
           |
65 | 61, 64 | sylib 200 |
. . . . . . . . . 10
    Moore         
          
             
            |
66 | | simplr 762 |
. . . . . . . . . . 11
    Moore         
          
             
    |
67 | 43 | ad2antrr 732 |
. . . . . . . . . . 11
    Moore         
          
             
                |
68 | | eleq1 2517 |
. . . . . . . . . . . . 13
 
   |
69 | | pweq 3954 |
. . . . . . . . . . . . . . 15
 
   |
70 | 69 | ineq1d 3633 |
. . . . . . . . . . . . . 14
  
      |
71 | | sseq2 3454 |
. . . . . . . . . . . . . 14
     
       |
72 | 70, 71 | raleqbidv 3001 |
. . . . . . . . . . . . 13
  
 
     
            |
73 | 68, 72 | bibi12d 323 |
. . . . . . . . . . . 12
           
 
             |
74 | 73 | rspcva 3148 |
. . . . . . . . . . 11
                 
            |
75 | 66, 67, 74 | syl2anc 667 |
. . . . . . . . . 10
    Moore         
          
             
          
   |
76 | 65, 75 | mpbird 236 |
. . . . . . . . 9
    Moore         
          
             
   |
77 | 24, 76 | impbida 843 |
. . . . . . . 8
   Moore        
  
              
            |
78 | 77 | ralrimiva 2802 |
. . . . . . 7
  Moore        
  
                           |
79 | 78 | ex 436 |
. . . . . 6
 Moore 
       
  
           
               |
80 | 79 | exlimdv 1779 |
. . . . 5
 Moore 
                          
             |
81 | 19 | mrcf 15515 |
. . . . . . . 8
 Moore 
       |
82 | 81, 40 | fssd 5738 |
. . . . . . 7
 Moore 
        |
83 | | fvex 5875 |
. . . . . . . . 9
mrCls   |
84 | 19, 83 | eqeltri 2525 |
. . . . . . . 8
 |
85 | | feq1 5710 |
. . . . . . . . 9
       
         |
86 | | fveq1 5864 |
. . . . . . . . . . . . . . 15
           |
87 | 86 | sseq1d 3459 |
. . . . . . . . . . . . . 14
     
       |
88 | 87 | ralbidv 2827 |
. . . . . . . . . . . . 13
  
 
     
            |
89 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
90 | 89 | sseq1d 3459 |
. . . . . . . . . . . . . 14
     
       |
91 | 90 | cbvralv 3019 |
. . . . . . . . . . . . 13
 
       
           |
92 | 88, 91 | syl6bb 265 |
. . . . . . . . . . . 12
  
 
     
            |
93 | 92 | bibi2d 320 |
. . . . . . . . . . 11
           
 
             |
94 | 93 | ralbidv 2827 |
. . . . . . . . . 10
  
                            |
95 | | sseq2 3454 |
. . . . . . . . . . . . 13
     
       |
96 | 70, 95 | raleqbidv 3001 |
. . . . . . . . . . . 12
  
 
     
            |
97 | 68, 96 | bibi12d 323 |
. . . . . . . . . . 11
           
 
             |
98 | 97 | cbvralv 3019 |
. . . . . . . . . 10
 
          
            
   |
99 | 94, 98 | syl6bb 265 |
. . . . . . . . 9
  
                            |
100 | 85, 99 | anbi12d 717 |
. . . . . . . 8
         
          
                    
     |
101 | 84, 100 | spcev 3141 |
. . . . . . 7
       
  
                                    |
102 | 82, 101 | sylan 474 |
. . . . . 6
  Moore  
          
 
         
          
    |
103 | 102 | ex 436 |
. . . . 5
 Moore 
 
          
                           |
104 | 80, 103 | impbid 194 |
. . . 4
 Moore 
                       
  
             |
105 | 11, 104 | syl5bb 261 |
. . 3
 Moore 
                      
  
             |
106 | 105 | pm5.32i 643 |
. 2
  Moore                          Moore  
          
    |
107 | 1, 106 | bitri 253 |
1
 ACS   Moore                  |