Step | Hyp | Ref
| Expression |
1 | | simpll 760 |
. 2
        ↾t   ↾t      |
2 | | simpll 760 |
. . . . . . . 8
             |
3 | | ssun1 3597 |
. . . . . . . . . 10

  |
4 | | sseq2 3454 |
. . . . . . . . . 10
   

    |
5 | 3, 4 | mpbiri 237 |
. . . . . . . . 9
     |
6 | 5 | ad2antlr 733 |
. . . . . . . 8
             |
7 | | uncmp.1 |
. . . . . . . . 9
  |
8 | 7 | cmpsub 20415 |
. . . . . . . 8
     ↾t 
   
          |
9 | 2, 6, 8 | syl2anc 667 |
. . . . . . 7
             ↾t 
              |
10 | | simprr 766 |
. . . . . . . . 9
              |
11 | 6, 10 | sseqtrd 3468 |
. . . . . . . 8
              |
12 | | unieq 4206 |
. . . . . . . . . . . 12
     |
13 | 12 | sseq2d 3460 |
. . . . . . . . . . 11
  
    |
14 | | pweq 3954 |
. . . . . . . . . . . . 13
 
   |
15 | 14 | ineq1d 3633 |
. . . . . . . . . . . 12
  
      |
16 | 15 | rexeqdv 2994 |
. . . . . . . . . . 11
  
 
  
         |
17 | 13, 16 | imbi12d 322 |
. . . . . . . . . 10
        
   
          |
18 | 17 | rspcv 3146 |
. . . . . . . . 9
                
 
       |
19 | 18 | ad2antrl 734 |
. . . . . . . 8
                         
 
       |
20 | 11, 19 | mpid 42 |
. . . . . . 7
                                |
21 | 9, 20 | sylbid 219 |
. . . . . 6
             ↾t           |
22 | | ssun2 3598 |
. . . . . . . . . 10

  |
23 | | sseq2 3454 |
. . . . . . . . . 10
   

    |
24 | 22, 23 | mpbiri 237 |
. . . . . . . . 9
     |
25 | 24 | ad2antlr 733 |
. . . . . . . 8
             |
26 | 7 | cmpsub 20415 |
. . . . . . . 8
     ↾t 
   
          |
27 | 2, 25, 26 | syl2anc 667 |
. . . . . . 7
             ↾t 
              |
28 | 25, 10 | sseqtrd 3468 |
. . . . . . . 8
              |
29 | | unieq 4206 |
. . . . . . . . . . . 12
     |
30 | 29 | sseq2d 3460 |
. . . . . . . . . . 11
  
    |
31 | | pweq 3954 |
. . . . . . . . . . . . 13
 
   |
32 | 31 | ineq1d 3633 |
. . . . . . . . . . . 12
  
      |
33 | 32 | rexeqdv 2994 |
. . . . . . . . . . 11
  
 
  
         |
34 | 30, 33 | imbi12d 322 |
. . . . . . . . . 10
        
   
          |
35 | 34 | rspcv 3146 |
. . . . . . . . 9
                
 
       |
36 | 35 | ad2antrl 734 |
. . . . . . . 8
                         
 
       |
37 | 28, 36 | mpid 42 |
. . . . . . 7
                                |
38 | 27, 37 | sylbid 219 |
. . . . . 6
             ↾t           |
39 | | reeanv 2958 |
. . . . . . 7
      
 
   
                  |
40 | | elin 3617 |
. . . . . . . . . . . . . . . . 17
   
     |
41 | 40 | simplbi 462 |
. . . . . . . . . . . . . . . 16
       |
42 | 41 | elpwid 3961 |
. . . . . . . . . . . . . . 15
      |
43 | | elin 3617 |
. . . . . . . . . . . . . . . . 17
   
     |
44 | 43 | simplbi 462 |
. . . . . . . . . . . . . . . 16
       |
45 | 44 | elpwid 3961 |
. . . . . . . . . . . . . . 15
      |
46 | 42, 45 | anim12i 570 |
. . . . . . . . . . . . . 14
    
 
 
    |
47 | 46 | ad2antrl 734 |
. . . . . . . . . . . . 13
   

   
            

    
   |
48 | | unss 3608 |
. . . . . . . . . . . . 13
 

    |
49 | 47, 48 | sylib 200 |
. . . . . . . . . . . 12
   

   
            

     
  |
50 | 40 | simprbi 466 |
. . . . . . . . . . . . . 14
      |
51 | 43 | simprbi 466 |
. . . . . . . . . . . . . 14
      |
52 | | unfi 7838 |
. . . . . . . . . . . . . 14
 
     |
53 | 50, 51, 52 | syl2an 480 |
. . . . . . . . . . . . 13
    
 
 
    |
54 | 53 | ad2antrl 734 |
. . . . . . . . . . . 12
   

   
            

        |
55 | 49, 54 | jca 535 |
. . . . . . . . . . 11
   

   
            

            |
56 | | elin 3617 |
. . . . . . . . . . . 12
     
    
    |
57 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
58 | 57 | elpw2 4567 |
. . . . . . . . . . . . 13
   
    |
59 | 58 | anbi1i 701 |
. . . . . . . . . . . 12
          

    |
60 | 56, 59 | bitr2i 254 |
. . . . . . . . . . 11
   

         |
61 | 55, 60 | sylib 200 |
. . . . . . . . . 10
   

   
            

           |
62 | | simpllr 769 |
. . . . . . . . . . . . 13
   

   
            

   
    |
63 | | ssun3 3599 |
. . . . . . . . . . . . . . . 16
        |
64 | | ssun4 3600 |
. . . . . . . . . . . . . . . 16
        |
65 | 63, 64 | anim12i 570 |
. . . . . . . . . . . . . . 15
 

 
            |
66 | 65 | ad2antll 735 |
. . . . . . . . . . . . . 14
   

   
            

      
 
 
     |
67 | | unss 3608 |
. . . . . . . . . . . . . 14
 
 
 
 
  
   
    |
68 | 66, 67 | sylib 200 |
. . . . . . . . . . . . 13
   

   
            

     
 
    |
69 | 62, 68 | eqsstrd 3466 |
. . . . . . . . . . . 12
   

   
            

          |
70 | | uniun 4217 |
. . . . . . . . . . . 12
        |
71 | 69, 70 | syl6sseqr 3479 |
. . . . . . . . . . 11
   

   
            

         |
72 | | elpwi 3960 |
. . . . . . . . . . . . . . 15
 
  |
73 | 72 | adantr 467 |
. . . . . . . . . . . . . 14
  
    |
74 | 73 | ad2antlr 733 |
. . . . . . . . . . . . 13
   

   
            

   
  |
75 | 49, 74 | sstrd 3442 |
. . . . . . . . . . . 12
   

   
            

     
  |
76 | | uniss 4219 |
. . . . . . . . . . . . 13
         |
77 | 76, 7 | syl6sseqr 3479 |
. . . . . . . . . . . 12
        |
78 | 75, 77 | syl 17 |
. . . . . . . . . . 11
   

   
            

      
  |
79 | 71, 78 | eqssd 3449 |
. . . . . . . . . 10
   

   
            

   
     |
80 | | unieq 4206 |
. . . . . . . . . . . 12
         |
81 | 80 | eqeq2d 2461 |
. . . . . . . . . . 11
   
       |
82 | 81 | rspcev 3150 |
. . . . . . . . . 10
      
 
          |
83 | 61, 79, 82 | syl2anc 667 |
. . . . . . . . 9
   

   
            

    
 
 
   |
84 | 83 | exp32 610 |
. . . . . . . 8
                                   |
85 | 84 | rexlimdvv 2885 |
. . . . . . 7
                          
 
 
    |
86 | 39, 85 | syl5bir 222 |
. . . . . 6
                              
    |
87 | 21, 38, 86 | syl2and 486 |
. . . . 5
              ↾t  
↾t       
    |
88 | 87 | impancom 442 |
. . . 4
        ↾t   ↾t                  |
89 | 88 | expd 438 |
. . 3
        ↾t   ↾t            
     |
90 | 89 | ralrimiv 2800 |
. 2
        ↾t   ↾t        
 
 
    |
91 | 7 | iscmp 20403 |
. 2


    
 
 
     |
92 | 1, 90, 91 | sylanbrc 670 |
1
        ↾t   ↾t      |