Step | Hyp | Ref
| Expression |
1 | | txcmp.r |
. . 3
   |
2 | | id 22 |
. . . . . . . . 9
   |
3 | | txcmp.a |
. . . . . . . . 9
   |
4 | | opelxpi 4871 |
. . . . . . . . 9
 
        |
5 | 2, 3, 4 | syl2anr 486 |
. . . . . . . 8
 
   
    |
6 | | txcmp.u |
. . . . . . . . 9
      |
7 | 6 | adantr 472 |
. . . . . . . 8
 
      |
8 | 5, 7 | eleqtrd 2551 |
. . . . . . 7
 
   
   |
9 | | eluni2 4194 |
. . . . . . 7
    

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

    |
12 | 11 | adantr 472 |
. . . . . . . . . . 11
 
     |
13 | 12 | sselda 3418 |
. . . . . . . . . 10
         |
14 | | txcmp.s |
. . . . . . . . . . . . 13
   |
15 | | eltx 20660 |
. . . . . . . . . . . . 13
     



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


         |
17 | 16 | adantr 472 |
. . . . . . . . . . 11
 
   



  
      |
18 | 17 | biimpa 492 |
. . . . . . . . . 10
       


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


  
     |
20 | | eleq1 2537 |
. . . . . . . . . . . 12
               |
21 | 20 | anbi1d 719 |
. . . . . . . . . . 11
          
            |
22 | 21 | 2rexbidv 2897 |
. . . . . . . . . 10
     

  
    
            |
23 | 22 | rspccv 3133 |
. . . . . . . . 9
 


    
     

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


            |
25 | | opelxp1 4872 |
. . . . . . . . . . . . 13
     
  |
26 | 25 | ad2antrl 742 |
. . . . . . . . . . . 12
   


            |
27 | | opelxp2 4873 |
. . . . . . . . . . . . . . . 16
     
  |
28 | 27 | ad2antrl 742 |
. . . . . . . . . . . . . . 15
   


            |
29 | 28 | snssd 4108 |
. . . . . . . . . . . . . 14
   


              |
30 | | xpss2 4949 |
. . . . . . . . . . . . . 14
           |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . 13
   


                  |
32 | | simprr 774 |
. . . . . . . . . . . . 13
   


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


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


                  |
35 | 34 | ex 441 |
. . . . . . . . . 10
                        |
36 | 35 | rexlimdvw 2874 |
. . . . . . . . 9
      
                  |
37 | 36 | reximdv 2857 |
. . . . . . . 8
      

         

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


        |
39 | 38 | reximdva 2858 |
. . . . . 6
 
  
  



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


       |
41 | | rexcom 2938 |
. . . . . 6
  
       

       |
42 | | r19.42v 2931 |
. . . . . . 7
         
       |
43 | 42 | rexbii 2881 |
. . . . . 6
  
       
        |
44 | 41, 43 | bitri 257 |
. . . . 5
  
       
        |
45 | 40, 44 | sylib 201 |
. . . 4
 
 


       |
46 | 45 | ralrimiva 2809 |
. . 3
  

        |
47 | | txcmp.x |
. . . 4
  |
48 | | sseq2 3440 |
. . . 4
                     |
49 | 47, 48 | cmpcovf 20483 |
. . 3
  

                      
            |
50 | 1, 46, 49 | syl2anc 673 |
. 2
               
            |
51 | | txcmp.y |
. . . . . . . 8
  |
52 | 1 | ad2antrr 740 |
. . . . . . . 8
       
      
          
  |
53 | | cmptop 20487 |
. . . . . . . . . 10

  |
54 | 14, 53 | syl 17 |
. . . . . . . . 9
   |
55 | 54 | ad2antrr 740 |
. . . . . . . 8
       
      
          
  |
56 | | cmptop 20487 |
. . . . . . . . . . 11

  |
57 | 52, 56 | syl 17 |
. . . . . . . . . 10
       
      
          
  |
58 | | txtop 20661 |
. . . . . . . . . 10
 
     |
59 | 57, 55, 58 | syl2anc 673 |
. . . . . . . . 9
       
      
          
    |
60 | | simprrl 782 |
. . . . . . . . . . 11
       
      
          
      |
61 | | frn 5747 |
. . . . . . . . . . 11
    
  |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
       
      
          
  |
63 | 11 | ad2antrr 740 |
. . . . . . . . . 10
       
      
          
    |
64 | 62, 63 | sstrd 3428 |
. . . . . . . . 9
       
      
          

   |
65 | | uniopn 20004 |
. . . . . . . . 9
   
        |
66 | 59, 64, 65 | syl2anc 673 |
. . . . . . . 8
       
      
          
     |
67 | | simprrr 783 |
. . . . . . . . . 10
       
      
          

          |
68 | | ss2iun 4285 |
. . . . . . . . . 10
 
             
      |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
       
      
          
            |
70 | | simprl 772 |
. . . . . . . . . . . 12
       
      
          
   |
71 | | uniiun 4322 |
. . . . . . . . . . . 12
   |
72 | 70, 71 | syl6eq 2521 |
. . . . . . . . . . 11
       
      
          
   |
73 | 72 | xpeq1d 4862 |
. . . . . . . . . 10
       
      
          
     
     |
74 | | xpiundir 4895 |
. . . . . . . . . 10
 
         |
75 | 73, 74 | syl6req 2522 |
. . . . . . . . 9
       
      
          
           |
76 | | ffn 5739 |
. . . . . . . . . . 11
       |
77 | 60, 76 | syl 17 |
. . . . . . . . . 10
       
      
          
  |
78 | | fniunfv 6170 |
. . . . . . . . . 10
 
       |
79 | 77, 78 | syl 17 |
. . . . . . . . 9
       
      
          
        |
80 | 69, 75, 79 | 3sstr3d 3460 |
. . . . . . . 8
       
      
          
       |
81 | 3 | ad2antrr 740 |
. . . . . . . 8
       
      
          
  |
82 | 47, 51, 52, 55, 66, 80, 81 | txtube 20732 |
. . . . . . 7
       
      
          


      |
83 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
84 | 83 | rnex 6746 |
. . . . . . . . . . . . 13
 |
85 | 84 | elpw 3948 |
. . . . . . . . . . . 12
 
  |
86 | 62, 85 | sylibr 217 |
. . . . . . . . . . 11
       
      
          
   |
87 | | inss2 3644 |
. . . . . . . . . . . . 13
    |
88 | | simplr 770 |
. . . . . . . . . . . . 13
       
      
          
     |
89 | 87, 88 | sseldi 3416 |
. . . . . . . . . . . 12
       
      
          
  |
90 | | dffn4 5812 |
. . . . . . . . . . . . 13

      |
91 | 77, 90 | sylib 201 |
. . . . . . . . . . . 12
       
      
          
      |
92 | | fofi 7878 |
. . . . . . . . . . . 12
      
  |
93 | 89, 91, 92 | syl2anc 673 |
. . . . . . . . . . 11
       
      
          
  |
94 | 86, 93 | elind 3609 |
. . . . . . . . . 10
       
      
          
     |
95 | | unieq 4198 |
. . . . . . . . . . . . 13
 
   |
96 | 95 | sseq2d 3446 |
. . . . . . . . . . . 12
           |
97 | 96 | rspcev 3136 |
. . . . . . . . . . 11
                   |
98 | 97 | ex 441 |
. . . . . . . . . 10
                   |
99 | 94, 98 | syl 17 |
. . . . . . . . 9
       
      
          
               |
100 | 99 | anim2d 575 |
. . . . . . . 8
       
      
          
 


 

            |
101 | 100 | reximdv 2857 |
. . . . . . 7
       
      
          
 



 


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


           |
103 | 102 | expr 626 |
. . . . 5
               
        


            |
104 | 103 | exlimdv 1787 |
. . . 4
                           

            |
105 | 104 | expimpd 614 |
. . 3
 
                          
            |
106 | 105 | rexlimdva 2871 |
. 2
                
          

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