Step | Hyp | Ref
| Expression |
1 | | alexsubALT.1 |
. . 3
  |
2 | 1 | alexsubALTlem1 21140 |
. 2

                   
     |
3 | 1 | alexsubALTlem4 21143 |
. . . . 5
              
 
 
 
        
 
 
     |
4 | | selpw 3949 |
. . . . . . . . 9
 
  |
5 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . 19
       |
6 | 5 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . 18
                 |
7 | | eluni 4193 |
. . . . . . . . . . . . . . . . . . . 20
 
  
   |
8 | | ssel 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
9 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           |
10 | | tg2 20057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     |
11 | 10 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           |
12 | 9, 11 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         

            |
13 | 8, 12 | sylan9r 670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                         |
14 | 13 | 3impia 1228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
          |
15 | | sseq2 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
16 | 15 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
  |
17 | 16 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    |
18 | 17 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
    |
19 | 18 | anim2d 575 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             


    |
20 | 19 | reximdv 2857 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
       
           |
21 | 14, 20 | syld 44 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
           |
22 | 21 | 3expia 1233 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          |
23 | 22 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . 22
                          |
24 | 23 | impd 438 |
. . . . . . . . . . . . . . . . . . . . 21
            

       
    |
25 | 24 | exlimdv 1787 |
. . . . . . . . . . . . . . . . . . . 20
                       
    |
26 | 7, 25 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . 19
                         |
27 | 26 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . 18
                          |
28 | 6, 27 | sylbid 223 |
. . . . . . . . . . . . . . . . 17
                         |
29 | | ssel 3412 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
30 | | elunii 4195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    |
31 | 30 | expcom 442 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
32 | 6 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
33 | 31, 32 | sylan9r 670 |
. . . . . . . . . . . . . . . . . . . . . 22
            
     |
34 | 29, 33 | syl9r 73 |
. . . . . . . . . . . . . . . . . . . . 21
            
       |
35 | 34 | rexlimdva 2871 |
. . . . . . . . . . . . . . . . . . . 20
                   |
36 | 35 | com23 80 |
. . . . . . . . . . . . . . . . . . 19
              
    |
37 | 36 | impd 438 |
. . . . . . . . . . . . . . . . . 18
              
    |
38 | 37 | rexlimdvw 2874 |
. . . . . . . . . . . . . . . . 17
                    
    |
39 | 28, 38 | impbid 195 |
. . . . . . . . . . . . . . . 16
                         |
40 | | elunirab 4202 |
. . . . . . . . . . . . . . . 16
       

       
   |
41 | 39, 40 | syl6bbr 271 |
. . . . . . . . . . . . . . 15
                   
    |
42 | 41 | eqrdv 2469 |
. . . . . . . . . . . . . 14
           
      
   |
43 | | ssrab2 3500 |
. . . . . . . . . . . . . . . 16
     
      |
44 | | fvex 5889 |
. . . . . . . . . . . . . . . . 17
     |
45 | 44 | elpw2 4565 |
. . . . . . . . . . . . . . . 16
      
     
     

      |
46 | 43, 45 | mpbir 214 |
. . . . . . . . . . . . . . 15
     
       |
47 | | unieq 4198 |
. . . . . . . . . . . . . . . . . 18
      

       
   |
48 | 47 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . 17
      

 
           |
49 | | pweq 3945 |
. . . . . . . . . . . . . . . . . . 19
      

       
   |
50 | 49 | ineq1d 3624 |
. . . . . . . . . . . . . . . . . 18
      

          
    |
51 | 50 | rexeqdv 2980 |
. . . . . . . . . . . . . . . . 17
      

     
                 |
52 | 48, 51 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
      

       
 
       

        
  
     |
53 | 52 | rspcv 3132 |
. . . . . . . . . . . . . . 15
      
       
           
  
      
         
  
     |
54 | 46, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
 
           
  
      
         
  
    |
55 | 42, 54 | syl5com 30 |
. . . . . . . . . . . . 13
                     
 
 
 
        
  
    |
56 | | elfpw 7894 |
. . . . . . . . . . . . . . 15
        
 
           |
57 | | ssel 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23
      

           |
58 | | sseq1 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
59 | 58 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
60 | 59 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      

    

   |
61 | 60 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
      


  |
62 | 57, 61 | syl6 33 |
. . . . . . . . . . . . . . . . . . . . . 22
      

 
   |
63 | 62 | ralrimiv 2808 |
. . . . . . . . . . . . . . . . . . . . 21
      



  |
64 | | sseq2 3440 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       |
65 | 64 | ac6sfi 7833 |
. . . . . . . . . . . . . . . . . . . . . 22
   
        
       |
66 | 65 | ex 441 |
. . . . . . . . . . . . . . . . . . . . 21
  

       
        |
67 | 63, 66 | syl5 32 |
. . . . . . . . . . . . . . . . . . . 20
 
     

       
        |
68 | 67 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
            
       
        
        |
69 | | simprll 780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
       
              |
70 | | frn 5747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
       
       
  |
72 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
       
          |
73 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
74 | | dffn4 5812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

      |
75 | 73, 74 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
76 | 75 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
      |
77 | 76 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
       
              |
78 | | fodomfi 7868 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
  |
79 | 72, 77, 78 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
       
       
  |
80 | | domfi 7811 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
81 | 72, 79, 80 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
       
       
  |
82 | 71, 81 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
       
            |
83 | | elin 3608 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
84 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
85 | 84 | elpw2 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
  |
86 | 85 | anbi1i 709 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

   |
87 | 83, 86 | bitr2i 258 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
88 | 82, 87 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       
       
     |
89 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
       
           |
90 | | uniiun 4322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
91 | | simprlr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
       
        
      |
92 | | ss2iun 4285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   
 
      |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
       
        
       |
94 | 90, 93 | syl5eqss 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
       
         
      |
95 | | fniunfv 6170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
       |
96 | 69, 73, 95 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
       
                |
97 | 94, 96 | sseqtrd 3454 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
       
            |
98 | 89, 97 | eqsstrd 3452 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
       
           |
99 | | simpll2 1070 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
       
          |
100 | 71, 99 | sstrd 3428 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
       
       
  |
101 | | uniss 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

    |
102 | 101, 1 | syl6sseqr 3465 |
. . . . . . . . . . . . . . . . . . . . . . . 24

   |
103 | 100, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
       
           |
104 | 98, 103 | eqssd 3435 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       
           |
105 | | unieq 4198 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
106 | 105 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
107 | 106 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
108 | 88, 104, 107 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
             
       
            
   |
109 | 108 | exp32 616 |
. . . . . . . . . . . . . . . . . . . 20
            
       
     
     
     |
110 | 109 | exlimdv 1787 |
. . . . . . . . . . . . . . . . . . 19
            
              
            |
111 | 68, 110 | syld 44 |
. . . . . . . . . . . . . . . . . 18
            
       
 
     
     |
112 | 111 | ex 441 |
. . . . . . . . . . . . . . . . 17
                   
 
     
      |
113 | 112 | com23 80 |
. . . . . . . . . . . . . . . 16
                  
        
      |
114 | 113 | impd 438 |
. . . . . . . . . . . . . . 15
                   

             |
115 | 56, 114 | syl5bi 225 |
. . . . . . . . . . . . . 14
                    

       
     |
116 | 115 | rexlimdv 2870 |
. . . . . . . . . . . . 13
                     
  
     
    |
117 | 55, 116 | syld 44 |
. . . . . . . . . . . 12
                     
 
 
 
         |
118 | 117 | 3exp 1230 |
. . . . . . . . . . 11
             
           
             |
119 | 118 | com34 85 |
. . . . . . . . . 10
                   
 
 
 
             |
120 | 119 | com23 80 |
. . . . . . . . 9
                  
 
 
 

             |
121 | 4, 120 | syl7bi 238 |
. . . . . . . 8
                  
 
 
 
  
     
      |
122 | 121 | ralrimdv 2811 |
. . . . . . 7
                  
 
 
 
    
 
 
     |
123 | | fibas 20070 |
. . . . . . . . 9
     |
124 | | tgcl 20062 |
. . . . . . . . 9
               |
125 | 123, 124 | ax-mp 5 |
. . . . . . . 8
         |
126 | | eleq1 2537 |
. . . . . . . 8
                     |
127 | 125, 126 | mpbiri 241 |
. . . . . . 7
           |
128 | 122, 127 | jctild 552 |
. . . . . 6
                  
 
 
 
     
 
 
      |
129 | 1 | iscmp 20480 |
. . . . . 6


    
 
 
     |
130 | 128, 129 | syl6ibr 235 |
. . . . 5
                  
 
 
 
   |
131 | 3, 130 | syld 44 |
. . . 4
              
 
 
 
   |
132 | 131 | imp 436 |
. . 3
          
       
  
  |
133 | 132 | exlimiv 1784 |
. 2
                    
  
  |
134 | 2, 133 | impbii 192 |
1

               
 
 
     |