Step | Hyp | Ref
| Expression |
1 | | sseq1 3465 |
. . . . . 6


   |
2 | 1 | anbi2d 715 |
. . . . 5

  Dirset

 Dirset
    |
3 | | raleq 2999 |
. . . . . 6

 
    |
4 | 3 | rexbidv 2913 |
. . . . 5

  
 
   |
5 | 2, 4 | imbi12d 326 |
. . . 4

   Dirset  

   Dirset
  
    |
6 | | sseq1 3465 |
. . . . . 6
 
   |
7 | 6 | anbi2d 715 |
. . . . 5
   Dirset 
 Dirset     |
8 | | raleq 2999 |
. . . . . 6
  

   |
9 | 8 | rexbidv 2913 |
. . . . 5
  



   |
10 | 7, 9 | imbi12d 326 |
. . . 4
    Dirset
  

 
Dirset  

    |
11 | | sseq1 3465 |
. . . . . 6
             |
12 | 11 | anbi2d 715 |
. . . . 5
       Dirset   Dirset         |
13 | | raleq 2999 |
. . . . . 6
      

        |
14 | 13 | rexbidv 2913 |
. . . . 5
      



        |
15 | 12, 14 | imbi12d 326 |
. . . 4
        Dirset
 

   Dirset      

         |
16 | | sseq1 3465 |
. . . . . 6
 
   |
17 | 16 | anbi2d 715 |
. . . . 5
   Dirset 
 Dirset     |
18 | | raleq 2999 |
. . . . . 6
  

   |
19 | 18 | rexbidv 2913 |
. . . . 5
  



   |
20 | 17, 19 | imbi12d 326 |
. . . 4
    Dirset
  

 
Dirset  

    |
21 | | drsbn0.b |
. . . . . . 7
     |
22 | 21 | drsbn0 16231 |
. . . . . 6
 Dirset   |
23 | | ral0 3886 |
. . . . . . . . 9
  |
24 | 23 | jctr 549 |
. . . . . . . 8
      |
25 | 24 | eximi 1718 |
. . . . . . 7
     
   |
26 | | n0 3753 |
. . . . . . 7
    |
27 | | df-rex 2755 |
. . . . . . 7
  
   
   |
28 | 25, 26, 27 | 3imtr4i 274 |
. . . . . 6


   |
29 | 22, 28 | syl 17 |
. . . . 5
 Dirset  
  |
30 | 29 | adantr 471 |
. . . 4
  Dirset


   |
31 | | ssun1 3609 |
. . . . . . . . 9
     |
32 | | sstr 3452 |
. . . . . . . . 9
 
        
  |
33 | 31, 32 | mpan 681 |
. . . . . . . 8
    
  |
34 | 33 | anim2i 577 |
. . . . . . 7
  Dirset
    
 Dirset    |
35 | | breq2 4420 |
. . . . . . . . . 10
 
   |
36 | 35 | ralbidv 2839 |
. . . . . . . . 9
  

   |
37 | 36 | cbvrexv 3032 |
. . . . . . . 8
  
 
  |
38 | | simplrr 776 |
. . . . . . . . . . . 12
    Dirset              

  |
39 | | drsprs 16230 |
. . . . . . . . . . . . . . . . 17
 Dirset  |
40 | 39 | ad5antr 745 |
. . . . . . . . . . . . . . . 16
      Dirset
    
         |
41 | 33 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . 19
   Dirset     
   |
42 | 41 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
    Dirset           
  |
43 | 42 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
     Dirset     
         |
44 | 43 | adantr 471 |
. . . . . . . . . . . . . . . 16
      Dirset
    
          |
45 | | simp-4r 782 |
. . . . . . . . . . . . . . . 16
      Dirset
    
          |
46 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
    Dirset           
  |
47 | 46 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
      Dirset
    
          |
48 | | simpr 467 |
. . . . . . . . . . . . . . . 16
      Dirset
    
          |
49 | | simprrl 779 |
. . . . . . . . . . . . . . . . 17
    Dirset           
  |
50 | 49 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
      Dirset
    
          |
51 | | drsdirfi.l |
. . . . . . . . . . . . . . . . 17
     |
52 | 21, 51 | prstr 16227 |
. . . . . . . . . . . . . . . 16
  
      |
53 | 40, 44, 45, 47, 48, 50, 52 | syl132anc 1294 |
. . . . . . . . . . . . . . 15
      Dirset
    
          |
54 | 53 | ex 440 |
. . . . . . . . . . . . . 14
     Dirset     
           |
55 | 54 | ralimdva 2808 |
. . . . . . . . . . . . 13
    Dirset           
 

   |
56 | 55 | adantlrr 732 |
. . . . . . . . . . . 12
    Dirset              
 

   |
57 | 38, 56 | mpd 15 |
. . . . . . . . . . 11
    Dirset              

  |
58 | | simprrr 780 |
. . . . . . . . . . . 12
    Dirset              
  |
59 | | vex 3060 |
. . . . . . . . . . . . 13
 |
60 | | breq1 4419 |
. . . . . . . . . . . . 13
 
   |
61 | 59, 60 | ralsn 4022 |
. . . . . . . . . . . 12
 
  
  |
62 | 58, 61 | sylibr 217 |
. . . . . . . . . . 11
    Dirset              
      |
63 | | ralun 3628 |
. . . . . . . . . . 11
  
             |
64 | 57, 62, 63 | syl2anc 671 |
. . . . . . . . . 10
    Dirset              
        |
65 | | simpll 765 |
. . . . . . . . . . 11
   Dirset     


  Dirset |
66 | | simprl 769 |
. . . . . . . . . . 11
   Dirset     


    |
67 | | ssun2 3610 |
. . . . . . . . . . . . . 14
 
     |
68 | | sstr 3452 |
. . . . . . . . . . . . . 14
              
  |
69 | 67, 68 | mpan 681 |
. . . . . . . . . . . . 13
         |
70 | 59 | snss 4109 |
. . . . . . . . . . . . 13

    |
71 | 69, 70 | sylibr 217 |
. . . . . . . . . . . 12
       |
72 | 71 | ad2antlr 738 |
. . . . . . . . . . 11
   Dirset     


    |
73 | 21, 51 | drsdir 16229 |
. . . . . . . . . . 11
  Dirset
 
    |
74 | 65, 66, 72, 73 | syl3anc 1276 |
. . . . . . . . . 10
   Dirset     


  
    |
75 | 64, 74 | reximddv 2875 |
. . . . . . . . 9
   Dirset     


  
        |
76 | 75 | rexlimdvaa 2892 |
. . . . . . . 8
  Dirset
    
 


         |
77 | 37, 76 | syl5bi 225 |
. . . . . . 7
  Dirset
    
 


         |
78 | 34, 77 | embantd 56 |
. . . . . 6
  Dirset
    
   Dirset  



         |
79 | 78 | com12 32 |
. . . . 5
   Dirset  


 
Dirset    
  
        |
80 | 79 | a1i 11 |
. . . 4
    Dirset
  
   Dirset      
          |
81 | 5, 10, 15, 20, 30, 80 | findcard2 7837 |
. . 3
   Dirset  

   |
82 | 81 | com12 32 |
. 2
  Dirset
 


   |
83 | 82 | 3impia 1212 |
1
  Dirset
  
  |