Step | Hyp | Ref
| Expression |
1 | | vex 3047 |
. . . . . . 7
 |
2 | | dfon2lem3 30424 |
. . . . . . 7
        

    |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
       

   |
4 | 3 | simpld 461 |
. . . . 5
         |
5 | 4 | ralimi 2780 |
. . . 4
 
      
  |
6 | | trint 4511 |
. . . 4
 
   |
7 | 5, 6 | syl 17 |
. . 3
 
         |
8 | 7 | adantl 468 |
. 2
  
          |
9 | 1 | dfon2lem7 30428 |
. . . . . . 7
                 |
10 | 9 | alrimiv 1772 |
. . . . . 6
             
     |
11 | 10 | ralimi 2780 |
. . . . 5
 
      
      
     |
12 | | df-ral 2741 |
. . . . . . 7
 
  
      
                |
13 | | 19.21v 1785 |
. . . . . . . 8
   

       

      
      |
14 | 13 | albii 1690 |
. . . . . . 7
                 
      
      |
15 | 12, 14 | bitr4i 256 |
. . . . . 6
 
  
      
    

          |
16 | | impexp 448 |
. . . . . . . 8
  

      

           |
17 | 16 | 2albii 1691 |
. . . . . . 7
      
    
  
    

          |
18 | | eluni2 4201 |
. . . . . . . . . . 11
 

  |
19 | 18 | biimpi 198 |
. . . . . . . . . 10
  
  |
20 | 19 | imim1i 60 |
. . . . . . . . 9
  
            
     |
21 | 20 | alimi 1683 |
. . . . . . . 8
    
   
                |
22 | | alcom 1922 |
. . . . . . . . 9
      
    
  
                |
23 | | 19.23v 1817 |
. . . . . . . . . . 11
            
              |
24 | | df-rex 2742 |
. . . . . . . . . . . 12
 
  
   |
25 | 24 | imbi1i 327 |
. . . . . . . . . . 11
  
      
              |
26 | 23, 25 | bitr4i 256 |
. . . . . . . . . 10
            
 
         |
27 | 26 | albii 1690 |
. . . . . . . . 9
      
    
  
       
     |
28 | 22, 27 | bitri 253 |
. . . . . . . 8
      
    
  
       
     |
29 | | df-ral 2741 |
. . . . . . . 8
 
       
       
     |
30 | 21, 28, 29 | 3imtr4i 270 |
. . . . . . 7
      
    
   
          |
31 | 17, 30 | sylbir 217 |
. . . . . 6
                     
    |
32 | 15, 31 | sylbi 199 |
. . . . 5
 
  
                  |
33 | 11, 32 | syl 17 |
. . . 4
 
                 |
34 | 33 | adantl 468 |
. . 3
  
       
          |
35 | | intssuni 4256 |
. . . . 5

    |
36 | | ssralv 3492 |
. . . . 5
            
            |
37 | 35, 36 | syl 17 |
. . . 4

 
                    |
38 | 37 | adantr 467 |
. . 3
  
                
            |
39 | 34, 38 | mpd 15 |
. 2
  
       
          |
40 | | dfon2lem6 30427 |
. . 3
   
                   |
41 | | intex 4558 |
. . . . . . . . . . 11
    |
42 | | dfon2lem3 30424 |
. . . . . . . . . . 11
 
    
            |
43 | 41, 42 | sylbi 199 |
. . . . . . . . . 10

                 |
44 | 43 | imp 431 |
. . . . . . . . 9
                  |
45 | 44 | simprd 465 |
. . . . . . . 8
               |
46 | | untelirr 30328 |
. . . . . . . 8
 

    |
47 | 45, 46 | syl 17 |
. . . . . . 7
          
    |
48 | 47 | adantlr 720 |
. . . . . 6
   
               
    |
49 | | risset 2914 |
. . . . . . . . . 10
 

   |
50 | 49 | notbii 298 |
. . . . . . . . 9
  
   |
51 | | ralnex 2833 |
. . . . . . . . 9
 


   |
52 | 50, 51 | bitr4i 256 |
. . . . . . . 8
  
   |
53 | | eqcom 2457 |
. . . . . . . . . . . 12
 
   |
54 | 53 | notbii 298 |
. . . . . . . . . . 11
     |
55 | 44 | simpld 461 |
. . . . . . . . . . . . 13
          
   |
56 | 55 | adantlr 720 |
. . . . . . . . . . . 12
   
               
   |
57 | | psseq2 3520 |
. . . . . . . . . . . . . . . . . . 19
 
   |
58 | 57 | anbi1d 710 |
. . . . . . . . . . . . . . . . . 18
   
     |
59 | | elequ2 1900 |
. . . . . . . . . . . . . . . . . 18
 
   |
60 | 58, 59 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
             |
61 | 60 | albidv 1766 |
. . . . . . . . . . . . . . . 16
       
         |
62 | 61 | rspccv 3146 |
. . . . . . . . . . . . . . 15
 
                |
63 | 62 | adantl 468 |
. . . . . . . . . . . . . 14
  
           
     |
64 | | intss1 4248 |
. . . . . . . . . . . . . . . 16
    |
65 | | dfpss2 3517 |
. . . . . . . . . . . . . . . . . . . 20
 
      |
66 | | psseq1 3519 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
   |
67 | | treq 4502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
    |
68 | 66, 67 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
69 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
70 | 68, 69 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
  
       |
71 | 70 | spcgv 3133 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
            |
72 | 41, 71 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . 22

                 |
73 | 72 | imp 431 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
74 | 73 | expd 438 |
. . . . . . . . . . . . . . . . . . . 20
                  |
75 | 65, 74 | syl5bir 222 |
. . . . . . . . . . . . . . . . . . 19
            
        |
76 | 75 | exp4b 611 |
. . . . . . . . . . . . . . . . . 18

        
           |
77 | 76 | com45 92 |
. . . . . . . . . . . . . . . . 17

        
           |
78 | 77 | com23 81 |
. . . . . . . . . . . . . . . 16

                    |
79 | 64, 78 | syl5 33 |
. . . . . . . . . . . . . . 15


                  |
80 | 79 | adantr 467 |
. . . . . . . . . . . . . 14
  
                  
       |
81 | 63, 80 | mpdd 41 |
. . . . . . . . . . . . 13
  
           
      |
82 | 81 | adantr 467 |
. . . . . . . . . . . 12
   
                
 
        |
83 | 56, 82 | mpid 42 |
. . . . . . . . . . 11
   
                
       |
84 | 54, 83 | syl7bi 234 |
. . . . . . . . . 10
   
                

      |
85 | 84 | ralrimiv 2799 |
. . . . . . . . 9
   
                 

    |
86 | | ralim 2776 |
. . . . . . . . 9
 

  
 
 
    |
87 | 85, 86 | syl 17 |
. . . . . . . 8
   
                 
 
    |
88 | 52, 87 | syl5bi 221 |
. . . . . . 7
   
                 
 
   |
89 | | elintg 4241 |
. . . . . . . . 9
 
        |
90 | 41, 89 | sylbi 199 |
. . . . . . . 8

 


    |
91 | 90 | ad2antrr 731 |
. . . . . . 7
   
                  

    |
92 | 88, 91 | sylibrd 238 |
. . . . . 6
   
                 
     |
93 | 48, 92 | mt3d 129 |
. . . . 5
   
                   |
94 | 93 | ex 436 |
. . . 4
  
               
    |
95 | 94 | ancld 556 |
. . 3
  
               
              |
96 | 40, 95 | syl5 33 |
. 2
  
                                  |
97 | 8, 39, 96 | mp2and 684 |
1
  
               
    |