Proof of Theorem isipodrs
Step | Hyp | Ref
| Expression |
1 | | eqid 2462 |
. . . . 5
   toInc      toInc    |
2 | 1 | drsbn0 16237 |
. . . 4
 toInc  Dirset    toInc     |
3 | 2 | neneqd 2640 |
. . 3
 toInc  Dirset    toInc     |
4 | | fvprc 5886 |
. . . . 5
 toInc    |
5 | 4 | fveq2d 5896 |
. . . 4
    toInc         |
6 | | base0 15217 |
. . . 4
     |
7 | 5, 6 | syl6eqr 2514 |
. . 3
    toInc     |
8 | 3, 7 | nsyl2 132 |
. 2
 toInc  Dirset   |
9 | | simp1 1014 |
. 2
  


  
  |
10 | | eqid 2462 |
. . . 4
   toInc      toInc    |
11 | 1, 10 | isdrs 16234 |
. . 3
 toInc  Dirset
 toInc     toInc       toInc    
   toInc        toInc         toInc        toInc        |
12 | | eqid 2462 |
. . . . . . . 8
toInc  toInc   |
13 | 12 | ipopos 16461 |
. . . . . . 7
toInc   |
14 | | posprs 16249 |
. . . . . . 7
 toInc  toInc   |
15 | 13, 14 | mp1i 13 |
. . . . . 6
 toInc   |
16 | | id 22 |
. . . . . 6
   |
17 | 15, 16 | 2thd 248 |
. . . . 5
  toInc     |
18 | 12 | ipobas 16456 |
. . . . . . 7
    toInc     |
19 | | neeq1 2698 |
. . . . . . . 8
    toInc   
   toInc      |
20 | | rexeq 3000 |
. . . . . . . . . 10
    toInc          toInc        toInc     
   toInc         toInc        toInc        |
21 | 20 | raleqbi1dv 3007 |
. . . . . . . . 9
    toInc           toInc        toInc     
   toInc        toInc         toInc        toInc        |
22 | 21 | raleqbi1dv 3007 |
. . . . . . . 8
    toInc            toInc        toInc     
   toInc        toInc        toInc         toInc        toInc        |
23 | 19, 22 | anbi12d 722 |
. . . . . . 7
    toInc             toInc        toInc          toInc   
   toInc        toInc        toInc         toInc        toInc         |
24 | 18, 23 | syl 17 |
. . . . . 6
   


     toInc        toInc     
    toInc   
   toInc        toInc        toInc         toInc        toInc         |
25 | | simpll 765 |
. . . . . . . . . . . 12
   
     |
26 | | simplrl 775 |
. . . . . . . . . . . 12
   
     |
27 | | simpr 467 |
. . . . . . . . . . . 12
   
     |
28 | 12, 10 | ipole 16459 |
. . . . . . . . . . . 12
 
      toInc   
   |
29 | 25, 26, 27, 28 | syl3anc 1276 |
. . . . . . . . . . 11
   
        toInc   
   |
30 | | simplrr 776 |
. . . . . . . . . . . 12
   
     |
31 | 12, 10 | ipole 16459 |
. . . . . . . . . . . 12
 
      toInc   
   |
32 | 25, 30, 27, 31 | syl3anc 1276 |
. . . . . . . . . . 11
   
        toInc       |
33 | 29, 32 | anbi12d 722 |
. . . . . . . . . 10
   
         toInc        toInc    
     |
34 | | unss 3620 |
. . . . . . . . . 10
 

    |
35 | 33, 34 | syl6bb 269 |
. . . . . . . . 9
   
         toInc        toInc    
     |
36 | 35 | rexbidva 2910 |
. . . . . . . 8
  
   
     toInc        toInc    

     |
37 | 36 | 2ralbidva 2842 |
. . . . . . 7
  


     toInc        toInc    



     |
38 | 37 | anbi2d 715 |
. . . . . 6
   


     toInc        toInc     
 


      |
39 | 24, 38 | bitr3d 263 |
. . . . 5
      toInc       toInc    
   toInc        toInc         toInc        toInc     
 


      |
40 | 17, 39 | anbi12d 722 |
. . . 4
   toInc      toInc   
   toInc        toInc        toInc         toInc        toInc      
  


       |
41 | | 3anass 995 |
. . . 4
  toInc 
   toInc   
   toInc        toInc        toInc         toInc        toInc       toInc      toInc       toInc    
   toInc        toInc         toInc        toInc         |
42 | | 3anass 995 |
. . . 4
  


   
 


      |
43 | 40, 41, 42 | 3bitr4g 296 |
. . 3
   toInc     toInc   
   toInc        toInc        toInc         toInc        toInc      
 



    |
44 | 11, 43 | syl5bb 265 |
. 2
  toInc  Dirset  


      |
45 | 8, 9, 44 | pm5.21nii 359 |
1
 toInc  Dirset
         |