Step | Hyp | Ref
| Expression |
1 | | ipodrsima.a |
. . 3
       |
2 | | elex 3040 |
. . 3
           |
3 | 1, 2 | syl 17 |
. 2
       |
4 | | ipodrsima.d |
. . . . 5
 toInc  Dirset |
5 | | isipodrs 16485 |
. . . . 5
 toInc  Dirset
         |
6 | 4, 5 | sylib 201 |
. . . 4
  


     |
7 | 6 | simp2d 1043 |
. . 3
   |
8 | | ipodrsima.f |
. . . . 5
    |
9 | | ipodrsima.s |
. . . . 5

   |
10 | | fnimaeq0 5707 |
. . . . 5
  
 
        |
11 | 8, 9, 10 | syl2anc 673 |
. . . 4
         |
12 | 11 | necon3bid 2687 |
. . 3
     
   |
13 | 7, 12 | mpbird 240 |
. 2
       |
14 | 6 | simp3d 1044 |
. . . 4
  

 
  |
15 | | simplll 776 |
. . . . . . . . . . . 12
   
 
     |
16 | | simpr 468 |
. . . . . . . . . . . 12
   
 
     |
17 | 9 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
    
 
   |
18 | | simprr 774 |
. . . . . . . . . . . . . . 15
    
 
  |
19 | 17, 18 | sseldd 3419 |
. . . . . . . . . . . . . 14
    
 
   |
20 | 19 | elpwid 3952 |
. . . . . . . . . . . . 13
    
 
  |
21 | 20 | adantr 472 |
. . . . . . . . . . . 12
   
 
     |
22 | | vex 3034 |
. . . . . . . . . . . . 13
 |
23 | | vex 3034 |
. . . . . . . . . . . . 13
 |
24 | | sseq12 3441 |
. . . . . . . . . . . . . . . 16
 
     |
25 | | sseq1 3439 |
. . . . . . . . . . . . . . . . 17
 
   |
26 | 25 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
     |
27 | 24, 26 | anbi12d 725 |
. . . . . . . . . . . . . . 15
 
         |
28 | 27 | anbi2d 718 |
. . . . . . . . . . . . . 14
 
   
  

     |
29 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
30 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
31 | | sseq12 3441 |
. . . . . . . . . . . . . . 15
                                       |
32 | 29, 30, 31 | syl2an 485 |
. . . . . . . . . . . . . 14
 
                     |
33 | 28, 32 | imbi12d 327 |
. . . . . . . . . . . . 13
 
    
 
           
 
            |
34 | | ipodrsima.m |
. . . . . . . . . . . . 13
 
      
      |
35 | 22, 23, 33, 34 | vtocl2 3088 |
. . . . . . . . . . . 12
 
      
      |
36 | 15, 16, 21, 35 | syl12anc 1290 |
. . . . . . . . . . 11
   
 
             |
37 | 36 | ex 441 |
. . . . . . . . . 10
    
 

           |
38 | | simplll 776 |
. . . . . . . . . . . 12
   
 
     |
39 | | simpr 468 |
. . . . . . . . . . . 12
   
 
     |
40 | 20 | adantr 472 |
. . . . . . . . . . . 12
   
 
     |
41 | | vex 3034 |
. . . . . . . . . . . . 13
 |
42 | | sseq12 3441 |
. . . . . . . . . . . . . . . 16
 
     |
43 | 25 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
     |
44 | 42, 43 | anbi12d 725 |
. . . . . . . . . . . . . . 15
 
         |
45 | 44 | anbi2d 718 |
. . . . . . . . . . . . . 14
 
   
  

     |
46 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
47 | | sseq12 3441 |
. . . . . . . . . . . . . . 15
                                       |
48 | 46, 30, 47 | syl2an 485 |
. . . . . . . . . . . . . 14
 
                     |
49 | 45, 48 | imbi12d 327 |
. . . . . . . . . . . . 13
 
    
 
           
 
            |
50 | 41, 23, 49, 34 | vtocl2 3088 |
. . . . . . . . . . . 12
 
      
      |
51 | 38, 39, 40, 50 | syl12anc 1290 |
. . . . . . . . . . 11
   
 
             |
52 | 51 | ex 441 |
. . . . . . . . . 10
    
 

           |
53 | 37, 52 | anim12d 572 |
. . . . . . . . 9
    
 
 
             
        |
54 | | unss 3599 |
. . . . . . . . 9
 

    |
55 | | unss 3599 |
. . . . . . . . 9
     
            
                |
56 | 53, 54, 55 | 3imtr3g 277 |
. . . . . . . 8
    
 
                    |
57 | 56 | anassrs 660 |
. . . . . . 7
   


   
                 |
58 | 57 | reximdva 2858 |
. . . . . 6
      
 
                  |
59 | 58 | ralimdva 2805 |
. . . . 5
 
  

 
 
                 |
60 | 59 | ralimdva 2805 |
. . . 4
        

         
       |
61 | 14, 60 | mpd 15 |
. . 3
  

         
      |
62 | | uneq1 3572 |
. . . . . . . . 9
               |
63 | 62 | sseq1d 3445 |
. . . . . . . 8
       
         |
64 | 63 | rexbidv 2892 |
. . . . . . 7
      
      
               |
65 | 64 | ralbidv 2829 |
. . . . . 6
      
            
                     |
66 | 65 | ralima 6163 |
. . . . 5
  
 
 
                    
                    |
67 | 8, 9, 66 | syl2anc 673 |
. . . 4
                       
                    |
68 | | uneq2 3573 |
. . . . . . . . . 10
                       |
69 | 68 | sseq1d 3445 |
. . . . . . . . 9
           
             |
70 | 69 | rexbidv 2892 |
. . . . . . . 8
      
          
                   |
71 | 70 | ralima 6163 |
. . . . . . 7
  
 
 
                  
                  |
72 | 8, 9, 71 | syl2anc 673 |
. . . . . 6
                     
                  |
73 | | sseq2 3440 |
. . . . . . . . 9
               
                 |
74 | 73 | rexima 6162 |
. . . . . . . 8
  
 
 
                         
       |
75 | 8, 9, 74 | syl2anc 673 |
. . . . . . 7
                                    |
76 | 75 | ralbidv 2829 |
. . . . . 6
                    
                 |
77 | 72, 76 | bitrd 261 |
. . . . 5
                     
                 |
78 | 77 | ralbidv 2829 |
. . . 4
                      

                 |
79 | 67, 78 | bitrd 261 |
. . 3
                       

                 |
80 | 61, 79 | mpbird 240 |
. 2
                    
  |
81 | | isipodrs 16485 |
. 2
 toInc      Dirset
    
    
                      |
82 | 3, 13, 80, 81 | syl3anbrc 1214 |
1
 toInc      Dirset |