Step | Hyp | Ref
| Expression |
1 | | txcmp.r |
. . 3
   |
2 | | id 22 |
. . . . . . . . 9
   |
3 | | txcmp.a |
. . . . . . . . 9
   |
4 | | opelxpi 4980 |
. . . . . . . . 9
 
        |
5 | 2, 3, 4 | syl2anr 478 |
. . . . . . . 8
 
   
    |
6 | | txcmp.u |
. . . . . . . . 9
      |
7 | 6 | adantr 465 |
. . . . . . . 8
 
      |
8 | 5, 7 | eleqtrd 2544 |
. . . . . . 7
 
   
   |
9 | | eluni2 4204 |
. . . . . . 7
    

  
  |
10 | 8, 9 | sylib 196 |
. . . . . 6
 
 
  
  |
11 | | txcmp.w |
. . . . . . . . . . . 12

    |
12 | 11 | adantr 465 |
. . . . . . . . . . 11
 
     |
13 | 12 | sselda 3465 |
. . . . . . . . . 10
         |
14 | | txcmp.s |
. . . . . . . . . . . . 13
   |
15 | | eltx 19274 |
. . . . . . . . . . . . 13
     



  
      |
16 | 1, 14, 15 | syl2anc 661 |
. . . . . . . . . . . 12
    


         |
17 | 16 | adantr 465 |
. . . . . . . . . . 11
 
   



  
      |
18 | 17 | biimpa 484 |
. . . . . . . . . 10
       


  
     |
19 | 13, 18 | syldan 470 |
. . . . . . . . 9
     


  
     |
20 | | eleq1 2526 |
. . . . . . . . . . . 12
               |
21 | 20 | anbi1d 704 |
. . . . . . . . . . 11
          
            |
22 | 21 | 2rexbidv 2880 |
. . . . . . . . . 10
     

  
    
            |
23 | 22 | rspccv 3176 |
. . . . . . . . 9
 


    
     

            |
24 | 19, 23 | syl 16 |
. . . . . . . 8
        


            |
25 | | opelxp1 4981 |
. . . . . . . . . . . . 13
     
  |
26 | 25 | ad2antrl 727 |
. . . . . . . . . . . 12
   


            |
27 | | opelxp2 4982 |
. . . . . . . . . . . . . . . 16
     
  |
28 | 27 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
   


            |
29 | 28 | snssd 4127 |
. . . . . . . . . . . . . 14
   


              |
30 | | xpss2 5058 |
. . . . . . . . . . . . . 14
           |
31 | 29, 30 | syl 16 |
. . . . . . . . . . . . 13
   


                  |
32 | | simprr 756 |
. . . . . . . . . . . . 13
   


              |
33 | 31, 32 | sstrd 3475 |
. . . . . . . . . . . 12
   


                |
34 | 26, 33 | jca 532 |
. . . . . . . . . . 11
   


                  |
35 | 34 | ex 434 |
. . . . . . . . . 10
                        |
36 | 35 | rexlimdvw 2950 |
. . . . . . . . 9
      
                  |
37 | 36 | reximdv 2933 |
. . . . . . . 8
      

         

        |
38 | 24, 37 | syld 44 |
. . . . . . 7
        


        |
39 | 38 | reximdva 2934 |
. . . . . 6
 
  
  



        |
40 | 10, 39 | mpd 15 |
. . . . 5
 
 


       |
41 | | rexcom 2988 |
. . . . . 6
  
       

       |
42 | | r19.42v 2981 |
. . . . . . 7
         
       |
43 | 42 | rexbii 2862 |
. . . . . 6
  
       
        |
44 | 41, 43 | bitri 249 |
. . . . 5
  
       
        |
45 | 40, 44 | sylib 196 |
. . . 4
 
 


       |
46 | 45 | ralrimiva 2830 |
. . 3
  

        |
47 | | txcmp.x |
. . . 4
  |
48 | | sseq2 3487 |
. . . 4
                     |
49 | 47, 48 | cmpcovf 19127 |
. . 3
  

                      
            |
50 | 1, 46, 49 | syl2anc 661 |
. 2
               
            |
51 | | txcmp.y |
. . . . . . . 8
  |
52 | 1 | ad2antrr 725 |
. . . . . . . 8
       
      
          
  |
53 | | cmptop 19131 |
. . . . . . . . . 10

  |
54 | 14, 53 | syl 16 |
. . . . . . . . 9
   |
55 | 54 | ad2antrr 725 |
. . . . . . . 8
       
      
          
  |
56 | | cmptop 19131 |
. . . . . . . . . . 11

  |
57 | 52, 56 | syl 16 |
. . . . . . . . . 10
       
      
          
  |
58 | | txtop 19275 |
. . . . . . . . . 10
 
     |
59 | 57, 55, 58 | syl2anc 661 |
. . . . . . . . 9
       
      
          
    |
60 | | simprrl 763 |
. . . . . . . . . . 11
       
      
          
      |
61 | | frn 5674 |
. . . . . . . . . . 11
    
  |
62 | 60, 61 | syl 16 |
. . . . . . . . . 10
       
      
          
  |
63 | 11 | ad2antrr 725 |
. . . . . . . . . 10
       
      
          
    |
64 | 62, 63 | sstrd 3475 |
. . . . . . . . 9
       
      
          

   |
65 | | uniopn 18643 |
. . . . . . . . 9
   
        |
66 | 59, 64, 65 | syl2anc 661 |
. . . . . . . 8
       
      
          
     |
67 | | simprrr 764 |
. . . . . . . . . 10
       
      
          

          |
68 | | ss2iun 4295 |
. . . . . . . . . 10
 
             
      |
69 | 67, 68 | syl 16 |
. . . . . . . . 9
       
      
          
            |
70 | | simprl 755 |
. . . . . . . . . . . 12
       
      
          
   |
71 | | uniiun 4332 |
. . . . . . . . . . . 12
   |
72 | 70, 71 | syl6eq 2511 |
. . . . . . . . . . 11
       
      
          
   |
73 | 72 | xpeq1d 4972 |
. . . . . . . . . 10
       
      
          
     
     |
74 | | xpiundir 5003 |
. . . . . . . . . 10
 
         |
75 | 73, 74 | syl6req 2512 |
. . . . . . . . 9
       
      
          
           |
76 | | ffn 5668 |
. . . . . . . . . . 11
       |
77 | 60, 76 | syl 16 |
. . . . . . . . . 10
       
      
          
  |
78 | | fniunfv 6074 |
. . . . . . . . . 10
 
       |
79 | 77, 78 | syl 16 |
. . . . . . . . 9
       
      
          
        |
80 | 69, 75, 79 | 3sstr3d 3507 |
. . . . . . . 8
       
      
          
       |
81 | 3 | ad2antrr 725 |
. . . . . . . 8
       
      
          
  |
82 | 47, 51, 52, 55, 66, 80, 81 | txtube 19346 |
. . . . . . 7
       
      
          


      |
83 | | vex 3081 |
. . . . . . . . . . . . . 14
 |
84 | 83 | rnex 6623 |
. . . . . . . . . . . . 13
 |
85 | 84 | elpw 3975 |
. . . . . . . . . . . 12
 
  |
86 | 62, 85 | sylibr 212 |
. . . . . . . . . . 11
       
      
          
   |
87 | | inss2 3680 |
. . . . . . . . . . . . 13
    |
88 | | simplr 754 |
. . . . . . . . . . . . 13
       
      
          
     |
89 | 87, 88 | sseldi 3463 |
. . . . . . . . . . . 12
       
      
          
  |
90 | | dffn4 5735 |
. . . . . . . . . . . . 13

      |
91 | 77, 90 | sylib 196 |
. . . . . . . . . . . 12
       
      
          
      |
92 | | fofi 7709 |
. . . . . . . . . . . 12
      
  |
93 | 89, 91, 92 | syl2anc 661 |
. . . . . . . . . . 11
       
      
          
  |
94 | 86, 93 | elind 3649 |
. . . . . . . . . 10
       
      
          
     |
95 | | unieq 4208 |
. . . . . . . . . . . . 13
 
   |
96 | 95 | sseq2d 3493 |
. . . . . . . . . . . 12
           |
97 | 96 | rspcev 3179 |
. . . . . . . . . . 11
                   |
98 | 97 | ex 434 |
. . . . . . . . . 10
                   |
99 | 94, 98 | syl 16 |
. . . . . . . . 9
       
      
          
               |
100 | 99 | anim2d 565 |
. . . . . . . 8
       
      
          
 


 

            |
101 | 100 | reximdv 2933 |
. . . . . . 7
       
      
          
 



 


            |
102 | 82, 101 | mpd 15 |
. . . . . 6
       
      
          


           |
103 | 102 | expr 615 |
. . . . 5
               
        


            |
104 | 103 | exlimdv 1691 |
. . . 4
                           

            |
105 | 104 | expimpd 603 |
. . 3
 
                          
            |
106 | 105 | rexlimdva 2947 |
. 2
                
          

            |
107 | 50, 106 | mpd 15 |
1
  
           |