Step | Hyp | Ref
| Expression |
1 | | txtube.r |
. . 3
   |
2 | | txtube.u |
. . . . . . . 8
       |
3 | 2 | adantr 471 |
. . . . . . 7
 
    
  |
4 | | id 22 |
. . . . . . . 8
   |
5 | | txtube.a |
. . . . . . . . 9
   |
6 | | snidg 4006 |
. . . . . . . . 9
     |
7 | 5, 6 | syl 17 |
. . . . . . . 8
     |
8 | | opelxpi 4888 |
. . . . . . . 8
 
     
      |
9 | 4, 7, 8 | syl2anr 485 |
. . . . . . 7
 
   
      |
10 | 3, 9 | sseldd 3445 |
. . . . . 6
 
   
  |
11 | | txtube.w |
. . . . . . . 8
     |
12 | | txtube.s |
. . . . . . . . 9
   |
13 | | eltx 20638 |
. . . . . . . . 9
   
 



  
      |
14 | 1, 12, 13 | syl2anc 671 |
. . . . . . . 8
    


         |
15 | 11, 14 | mpbid 215 |
. . . . . . 7
  

        |
16 | 15 | adantr 471 |
. . . . . 6
 
 


  
     |
17 | | eleq1 2528 |
. . . . . . . . 9
               |
18 | 17 | anbi1d 716 |
. . . . . . . 8
          
            |
19 | 18 | 2rexbidv 2920 |
. . . . . . 7
     

  
    
            |
20 | 19 | rspcv 3158 |
. . . . . 6
   
 


   

  
            |
21 | 10, 16, 20 | sylc 62 |
. . . . 5
 
 

           |
22 | | opelxp 4886 |
. . . . . . . . . 10
          |
23 | 22 | anbi1i 706 |
. . . . . . . . 9
      
           |
24 | | anass 659 |
. . . . . . . . 9
  

           |
25 | 23, 24 | bitri 257 |
. . . . . . . 8
      
           |
26 | 25 | rexbii 2901 |
. . . . . . 7
       
    
       |
27 | | r19.42v 2957 |
. . . . . . 7
   
 
   

      |
28 | 26, 27 | bitri 257 |
. . . . . 6
       
    

      |
29 | 28 | rexbii 2901 |
. . . . 5
  
     
    
 
 
    |
30 | 21, 29 | sylib 201 |
. . . 4
 
 



      |
31 | 30 | ralrimiva 2814 |
. . 3
  

 
 
    |
32 | | txtube.x |
. . . 4
  |
33 | | eleq2 2529 |
. . . . 5
     
       |
34 | | xpeq2 4871 |
. . . . . 6
               |
35 | 34 | sseq1d 3471 |
. . . . 5
       
         |
36 | 33, 35 | anbi12d 722 |
. . . 4
              
          |
37 | 32, 36 | cmpcovf 20461 |
. . 3
  

   

                 

               |
38 | 1, 31, 37 | syl2anc 671 |
. 2
               

               |
39 | | rint0 4289 |
. . . . . . . . . 10
      |
40 | 39 | adantl 472 |
. . . . . . . . 9
   
                
          
     |
41 | | txtube.y |
. . . . . . . . . . . 12
  |
42 | 41 | topopn 19991 |
. . . . . . . . . . 11
   |
43 | 12, 42 | syl 17 |
. . . . . . . . . 10
   |
44 | 43 | ad3antrrr 741 |
. . . . . . . . 9
   
                
          
  |
45 | 40, 44 | eqeltrd 2540 |
. . . . . . . 8
   
                
          
     |
46 | 12 | ad3antrrr 741 |
. . . . . . . . . . . . 13
   
                
          
  |
47 | | simprrl 779 |
. . . . . . . . . . . . . . 15
       
      
    
                |
48 | | frn 5762 |
. . . . . . . . . . . . . . 15
    
  |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
       
      
    
         
  |
50 | 49 | adantr 471 |
. . . . . . . . . . . . 13
   
                
          
  |
51 | | simpr 467 |
. . . . . . . . . . . . 13
   
                
          
  |
52 | | inss2 3665 |
. . . . . . . . . . . . . . . 16
    |
53 | | simplr 767 |
. . . . . . . . . . . . . . . 16
       
      
    
               |
54 | 52, 53 | sseldi 3442 |
. . . . . . . . . . . . . . 15
       
      
    
            |
55 | | ffn 5755 |
. . . . . . . . . . . . . . . . 17
       |
56 | 47, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
       
      
    
            |
57 | | dffn4 5826 |
. . . . . . . . . . . . . . . 16

      |
58 | 56, 57 | sylib 201 |
. . . . . . . . . . . . . . 15
       
      
    
                |
59 | | fofi 7891 |
. . . . . . . . . . . . . . 15
      
  |
60 | 54, 58, 59 | syl2anc 671 |
. . . . . . . . . . . . . 14
       
      
    
         
  |
61 | 60 | adantr 471 |
. . . . . . . . . . . . 13
   
                
          
  |
62 | | fiinopn 19986 |
. . . . . . . . . . . . . 14
  
 
   |
63 | 62 | imp 435 |
. . . . . . . . . . . . 13
  
 
   |
64 | 46, 50, 51, 61, 63 | syl13anc 1278 |
. . . . . . . . . . . 12
   
                
          

  |
65 | | elssuni 4241 |
. . . . . . . . . . . 12
      |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
   
                
          
    |
67 | 66, 41 | syl6sseqr 3491 |
. . . . . . . . . 10
   
                
          
   |
68 | | dfss1 3649 |
. . . . . . . . . 10
 
      |
69 | 67, 68 | sylib 201 |
. . . . . . . . 9
   
                
          
      |
70 | 69, 64 | eqeltrd 2540 |
. . . . . . . 8
   
                
          
     |
71 | 45, 70 | pm2.61dane 2723 |
. . . . . . 7
       
      
    
               |
72 | 5 | ad2antrr 737 |
. . . . . . . 8
       
      
    
            |
73 | | simprrr 780 |
. . . . . . . . . . 11
       
      
    
                         |
74 | | simpl 463 |
. . . . . . . . . . . 12
      
    
       |
75 | 74 | ralimi 2793 |
. . . . . . . . . . 11
 

           
      |
76 | 73, 75 | syl 17 |
. . . . . . . . . 10
       
      
    
                 |
77 | | eliin 4298 |
. . . . . . . . . . 11
 
    

       |
78 | 72, 77 | syl 17 |
. . . . . . . . . 10
       
      
    
           
            |
79 | 76, 78 | mpbird 240 |
. . . . . . . . 9
       
      
    
                 |
80 | | fniinfv 5952 |
. . . . . . . . . 10
 
       |
81 | 56, 80 | syl 17 |
. . . . . . . . 9
       
      
    
                  |
82 | 79, 81 | eleqtrd 2542 |
. . . . . . . 8
       
      
    
             |
83 | 72, 82 | elind 3630 |
. . . . . . 7
       
      
    
               |
84 | | simprl 769 |
. . . . . . . . . . 11
       
      
    
             |
85 | | uniiun 4345 |
. . . . . . . . . . 11
   |
86 | 84, 85 | syl6eq 2512 |
. . . . . . . . . 10
       
      
    
          
  |
87 | 86 | xpeq1d 4879 |
. . . . . . . . 9
       
      
    
           
           |
88 | | xpiundir 4912 |
. . . . . . . . 9
 
           |
89 | 87, 88 | syl6eq 2512 |
. . . . . . . 8
       
      
    
           
           |
90 | | simpr 467 |
. . . . . . . . . . . 12
      
    
      
  |
91 | 90 | ralimi 2793 |
. . . . . . . . . . 11
 

           
     
  |
92 | 73, 91 | syl 17 |
. . . . . . . . . 10
       
      
    
                
  |
93 | | inss2 3665 |
. . . . . . . . . . . . 13
     |
94 | 80 | adantr 471 |
. . . . . . . . . . . . . 14
 
 
       |
95 | | iinss2 4344 |
. . . . . . . . . . . . . . 15
 
          |
96 | 95 | adantl 472 |
. . . . . . . . . . . . . 14
 
 
   
      |
97 | 94, 96 | eqsstr3d 3479 |
. . . . . . . . . . . . 13
 
        |
98 | 93, 97 | syl5ss 3455 |
. . . . . . . . . . . 12
 
          |
99 | | xpss2 4966 |
. . . . . . . . . . . 12
            
        |
100 | | sstr2 3451 |
. . . . . . . . . . . 12
     
            
    
   |
101 | 98, 99, 100 | 3syl 18 |
. . . . . . . . . . 11
 
            
   |
102 | 101 | ralimdva 2808 |
. . . . . . . . . 10
  
     
     
   |
103 | 56, 92, 102 | sylc 62 |
. . . . . . . . 9
       
      
    
               
  |
104 | | iunss 4333 |
. . . . . . . . 9
 
    

       |
105 | 103, 104 | sylibr 217 |
. . . . . . . 8
       
      
    
               
  |
106 | 89, 105 | eqsstrd 3478 |
. . . . . . 7
       
      
    
           
     |
107 | | eleq2 2529 |
. . . . . . . . 9
           |
108 | | xpeq2 4871 |
. . . . . . . . . 10
             |
109 | 108 | sseq1d 3471 |
. . . . . . . . 9
           
   |
110 | 107, 109 | anbi12d 722 |
. . . . . . . 8
        
             |
111 | 110 | rspcev 3162 |
. . . . . . 7
                 
 
   |
112 | 71, 83, 106, 111 | syl12anc 1274 |
. . . . . 6
       
      
    
           
 
   |
113 | 112 | expr 624 |
. . . . 5
               

             
 
    |
114 | 113 | exlimdv 1790 |
. . . 4
                      
        

      |
115 | 114 | expimpd 612 |
. . 3
 
                   
         

 
    |
116 | 115 | rexlimdva 2891 |
. 2
                

            


      |
117 | 38, 116 | mpd 15 |
1
  
 
   |