Step | Hyp | Ref
| Expression |
1 | | dfac3 8570 |
. . 3
CHOICE
             |
2 | | nfra1 2785 |
. . . . . . 7
          |
3 | | rsp 2773 |
. . . . . . . . . . . . 13
 
                |
4 | | equid 1863 |
. . . . . . . . . . . . . . . . . . 19
 |
5 | | neeq1 2705 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
6 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
7 | 5, 6 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
8 | 7 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . 19
      
   |
9 | 4, 8 | mpanr2 698 |
. . . . . . . . . . . . . . . . . 18
   
    |
10 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
11 | 10 | preq1d 4048 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
12 | | preq2 4043 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
13 | 11, 12 | eqtr2d 2506 |
. . . . . . . . . . . . . . . . . . . 20
                 |
14 | 13 | anim2i 579 |
. . . . . . . . . . . . . . . . . . 19
                     |
15 | 14 | reximi 2852 |
. . . . . . . . . . . . . . . . . 18
    

                 |
16 | 9, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
                  |
17 | | prex 4642 |
. . . . . . . . . . . . . . . . . 18
        |
18 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . 20
               
                 |
19 | 18 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . 19
                 
                   |
20 | 19 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . 18
         

       

                   |
21 | 17, 20 | elab 3173 |
. . . . . . . . . . . . . . . . 17
          
        

                  |
22 | 16, 21 | sylibr 217 |
. . . . . . . . . . . . . . . 16
           
            |
23 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
24 | 23 | prid2 4072 |
. . . . . . . . . . . . . . . . 17
        |
25 | | fvex 5889 |
. . . . . . . . . . . . . . . . . 18
     |
26 | 25 | prid1 4071 |
. . . . . . . . . . . . . . . . 17
            |
27 | 24, 26 | pm3.2i 462 |
. . . . . . . . . . . . . . . 16
                     |
28 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . 18
        
          |
29 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . 18
            
              |
30 | 28, 29 | anbi12d 725 |
. . . . . . . . . . . . . . . . 17
                                      |
31 | 30 | rspcev 3136 |
. . . . . . . . . . . . . . . 16
                                         
  
                  |
32 | 22, 27, 31 | sylancl 675 |
. . . . . . . . . . . . . . 15
     
                  |
33 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
     
       |
34 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . 19
     
       |
35 | 34 | anbi2d 718 |
. . . . . . . . . . . . . . . . . 18
                 |
36 | 35 | rexbidv 2892 |
. . . . . . . . . . . . . . . . 17
      
             
  
                   |
37 | 33, 36 | anbi12d 725 |
. . . . . . . . . . . . . . . 16
         
          
         
                    |
38 | 25, 37 | spcev 3127 |
. . . . . . . . . . . . . . 15
                               
          
    |
39 | 32, 38 | sylan2 482 |
. . . . . . . . . . . . . 14
      
     
  
         
    |
40 | 39 | ex 441 |
. . . . . . . . . . . . 13
      
      
          
     |
41 | 3, 40 | syl8 71 |
. . . . . . . . . . . 12
 
         
      
          
       |
42 | 41 | impd 438 |
. . . . . . . . . . 11
 
       
   
     
          
      |
43 | 42 | pm2.43d 49 |
. . . . . . . . . 10
 
       
      
          
     |
44 | | df-rex 2762 |
. . . . . . . . . . . . . 14
               
    
               |
45 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . 20
 |
46 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . . . . . 22
        
          |
47 | 46 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . 21
          
            |
48 | 47 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . 20
  

       

            |
49 | 45, 48 | elab 3173 |
. . . . . . . . . . . . . . . . . . 19
   
        

           |
50 | | neeq1 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
51 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
52 | 51 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
       |
53 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
       |
54 | 52, 53 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
       |
55 | 50, 54 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       

        |
56 | 55 | rspccv 3133 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                |
57 | | elirrv 8130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
58 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
59 | 57, 58 | mtbii 309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
60 | 59 | con2i 124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32

  |
61 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
62 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
63 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
64 | 61, 23, 62, 63 | prel12 4143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                   
           |
65 | | ancom 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
 
   |
66 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        
          |
67 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        
          |
68 | 66, 67 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                              |
69 | 65, 68 | syl5rbbr 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                
             |
70 | 64, 69 | sylan9bbr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        

          

    |
71 | 60, 70 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
            
    |
72 | 71 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
     
          

    |
73 | 72 | pm5.32da 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                          
             |
74 | 61, 23, 62, 63 | preleq 8140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
               
   |
75 | 73, 74 | syl6bir 237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                
 
         |
76 | 51 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
       |
77 | 76 | biimparc 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
       |
78 | 75, 77 | syl6 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                
 
       |
79 | 78 | exp4c 619 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                          |
80 | 79 | com13 82 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                          |
81 | 56, 80 | syl8 71 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                               |
82 | 81 | com4r 88 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                  
           |
83 | 82 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . 22
                      
          |
84 | 83 | imp4a 600 |
. . . . . . . . . . . . . . . . . . . . 21
                    
 
          |
85 | 84 | com3l 83 |
. . . . . . . . . . . . . . . . . . . 20
                       
         |
86 | 85 | rexlimiv 2867 |
. . . . . . . . . . . . . . . . . . 19
                       
        |
87 | 49, 86 | sylbi 200 |
. . . . . . . . . . . . . . . . . 18
   
                     
        |
88 | 87 | expd 443 |
. . . . . . . . . . . . . . . . 17
   
                 
 
          |
89 | 88 | com13 82 |
. . . . . . . . . . . . . . . 16
 
         
            
         |
90 | 89 | imp4b 601 |
. . . . . . . . . . . . . . 15
             
                    |
91 | 90 | exlimdv 1787 |
. . . . . . . . . . . . . 14
               
                    |
92 | 44, 91 | syl5bi 225 |
. . . . . . . . . . . . 13
           
                     |
93 | 92 | expimpd 614 |
. . . . . . . . . . . 12
 
          
          
 
       |
94 | 93 | alrimiv 1781 |
. . . . . . . . . . 11
 
            
          
 
       |
95 | | mo2icl 3205 |
. . . . . . . . . . 11
     
  
         
 
          
          
    |
96 | 94, 95 | syl 17 |
. . . . . . . . . 10
 
           
          
    |
97 | 43, 96 | jctird 553 |
. . . . . . . . 9
 
       
                          
          
      |
98 | | df-reu 2763 |
. . . . . . . . . 10
  
  
         
      
          
    |
99 | | eu5 2345 |
. . . . . . . . . 10
      
          
        
          
 
     
          
     |
100 | 98, 99 | bitri 257 |
. . . . . . . . 9
  
  
         
     
  
         
 
     
          
     |
101 | 97, 100 | syl6ibr 235 |
. . . . . . . 8
 
       
 

                 |
102 | 101 | expd 443 |
. . . . . . 7
 
        

  
         
     |
103 | 2, 102 | ralrimi 2800 |
. . . . . 6
 
      


  
          
    |
104 | | vex 3034 |
. . . . . . . . . . . 12
 |
105 | 104 | rnex 6746 |
. . . . . . . . . . 11
 |
106 | | p0ex 4588 |
. . . . . . . . . . 11
   |
107 | 105, 106 | unex 6608 |
. . . . . . . . . 10
     |
108 | | vex 3034 |
. . . . . . . . . 10
 |
109 | 107, 108 | unex 6608 |
. . . . . . . . 9
       |
110 | 109 | pwex 4584 |
. . . . . . . 8
  
     |
111 | | ssun1 3588 |
. . . . . . . . . . . . . . 15
   
 
     |
112 | | fvrn0 5901 |
. . . . . . . . . . . . . . 15
         |
113 | 111, 112 | sselii 3415 |
. . . . . . . . . . . . . 14
           |
114 | | elun2 3593 |
. . . . . . . . . . . . . 14
         |
115 | | prssi 4119 |
. . . . . . . . . . . . . 14
           
                      |
116 | 113, 114,
115 | sylancr 676 |
. . . . . . . . . . . . 13
                |
117 | | prex 4642 |
. . . . . . . . . . . . . 14
        |
118 | 117 | elpw 3948 |
. . . . . . . . . . . . 13
                              |
119 | 116, 118 | sylibr 217 |
. . . . . . . . . . . 12
                 |
120 | | eleq1 2537 |
. . . . . . . . . . . 12
           
          
  
       |
121 | 119, 120 | syl5ibrcom 230 |
. . . . . . . . . . 11
                   |
122 | 121 | adantld 474 |
. . . . . . . . . 10
                     |
123 | 122 | rexlimiv 2867 |
. . . . . . . . 9
                    |
124 | 123 | abssi 3490 |
. . . . . . . 8
                    |
125 | 110, 124 | ssexi 4541 |
. . . . . . 7
             |
126 | | rexeq 2974 |
. . . . . . . . . 10
   
               
          
    |
127 | 126 | reubidv 2961 |
. . . . . . . . 9
   
                 
          
    |
128 | 127 | imbi2d 323 |
. . . . . . . 8
   
           


      
          
     |
129 | 128 | ralbidv 2829 |
. . . . . . 7
   
            


    

  
         
     |
130 | 125, 129 | spcev 3127 |
. . . . . 6
 
 

  
         
 
  
 


    |
131 | 103, 130 | syl 17 |
. . . . 5
 
        
 


    |
132 | 131 | exlimiv 1784 |
. . . 4
         
  
 


    |
133 | 132 | alimi 1692 |
. . 3
     

    
             |
134 | 1, 133 | sylbi 200 |
. 2
CHOICE              |
135 | | dfac2a 8578 |
. 2
     




  CHOICE |
136 | 134, 135 | impbii 192 |
1
CHOICE
             |