Step | Hyp | Ref
| Expression |
1 | | df-br 4403 |
. . . 4
    
 
  
       
    |
2 | 1 | a1i 11 |
. . 3
 
          
             |
3 | | trclfv 13064 |
. . . . 5
               |
4 | 3 | breqd 4413 |
. . . 4
              
      |
5 | 4 | 3ad2ant3 1031 |
. . 3
 
                     |
6 | | elimasng 5194 |
. . . 4
 
     
 
              
     |
7 | 6 | 3adant3 1028 |
. . 3
 
     
 
              
     |
8 | 2, 5, 7 | 3bitr4d 289 |
. 2
 
        
   
 
          |
9 | | intimasn 36249 |
. . . . 5
    
 
           
 
            |
10 | 9 | 3ad2ant1 1029 |
. . . 4
 
                  
 
            |
11 | | simpl3 1013 |
. . . . . . . . . . . . . 14
  

           |
12 | | snex 4641 |
. . . . . . . . . . . . . . 15
 
 |
13 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
14 | 12, 13 | xpex 6595 |
. . . . . . . . . . . . . 14
     |
15 | | unexg 6592 |
. . . . . . . . . . . . . 14
               |
16 | 11, 14, 15 | sylancl 668 |
. . . . . . . . . . . . 13
  

         
  
    |
17 | | trclfvlb 13072 |
. . . . . . . . . . . . . 14
                 
  
     |
18 | 17 | unssad 3611 |
. . . . . . . . . . . . 13
      
             |
19 | 16, 18 | syl 17 |
. . . . . . . . . . . 12
  

             
        |
20 | | trclfvcotrg 13080 |
. . . . . . . . . . . . 13
     
  
       
                   |
21 | 20 | a1i 11 |
. . . . . . . . . . . 12
  

              
          
                    |
22 | | simpl1 1011 |
. . . . . . . . . . . . . . . . 17
  

           |
23 | | snidg 3994 |
. . . . . . . . . . . . . . . . 17
     |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
  

             |
25 | | inelcm 3819 |
. . . . . . . . . . . . . . . 16
               |
26 | 24, 24, 25 | syl2anc 667 |
. . . . . . . . . . . . . . 15
  

                 |
27 | | xpima2 5281 |
. . . . . . . . . . . . . . 15
                   |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
  

                     |
29 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
  

         
  
      
  
     |
30 | 29 | unssbd 3612 |
. . . . . . . . . . . . . . 15
  

            
             |
31 | | imass1 5203 |
. . . . . . . . . . . . . . 15
         
  
                                |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . 14
  

                        
             |
33 | 28, 32 | eqsstr3d 3467 |
. . . . . . . . . . . . 13
  

                            |
34 | | imaundir 5249 |
. . . . . . . . . . . . . . 15
                                     |
35 | | simpr 463 |
. . . . . . . . . . . . . . . 16
  

              
 
  |
36 | | imassrn 5179 |
. . . . . . . . . . . . . . . . . 18
                 |
37 | | rnxpss 5269 |
. . . . . . . . . . . . . . . . . 18
   
 |
38 | 36, 37 | sstri 3441 |
. . . . . . . . . . . . . . . . 17
             |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . 16
  

                       |
40 | 35, 39 | unssd 3610 |
. . . . . . . . . . . . . . 15
  

                                 |
41 | 34, 40 | syl5eqss 3476 |
. . . . . . . . . . . . . 14
  

                         |
42 | | trclimalb2 36318 |
. . . . . . . . . . . . . 14
                            
             |
43 | 16, 41, 42 | syl2anc 667 |
. . . . . . . . . . . . 13
  

              
             |
44 | 33, 43 | eqssd 3449 |
. . . . . . . . . . . 12
  

                            |
45 | | sbcan 3310 |
. . . . . . . . . . . . . 14
      
       ![]. ].](_drbrack.gif)     
             
  
    ![]. ].](_drbrack.gif)    
             ![]. ].](_drbrack.gif)
         |
46 | | sbcan 3310 |
. . . . . . . . . . . . . . . 16
      
       ![]. ].](_drbrack.gif)           
  
    ![]. ].](_drbrack.gif)              ![]. ].](_drbrack.gif)      |
47 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . 19
            |
48 | | sbcssg 3880 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  
    ![]. ].](_drbrack.gif)      
       ![]_ ]_](_urbrack.gif)      
  
    ![]_ ]_](_urbrack.gif)    |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
      
       ![]. ].](_drbrack.gif)      
       ![]_ ]_](_urbrack.gif)      
  
    ![]_ ]_](_urbrack.gif)   |
50 | | csbconstg 3376 |
. . . . . . . . . . . . . . . . . . . 20
     
  
                ![]_ ]_](_urbrack.gif)   |
51 | 47, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     
  
    ![]_ ]_](_urbrack.gif)  |
52 | | csbvarg 3792 |
. . . . . . . . . . . . . . . . . . . 20
     
  
                ![]_ ]_](_urbrack.gif)              |
53 | 47, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     
  
    ![]_ ]_](_urbrack.gif)     
  
    |
54 | 51, 53 | sseq12i 3458 |
. . . . . . . . . . . . . . . . . 18
      
       ![]_ ]_](_urbrack.gif)      
  
    ![]_ ]_](_urbrack.gif)
    
  
     |
55 | 49, 54 | bitri 253 |
. . . . . . . . . . . . . . . . 17
      
       ![]. ].](_drbrack.gif)              |
56 | | sbcssg 3880 |
. . . . . . . . . . . . . . . . . . 19
     
  
         
  
    ![]. ].](_drbrack.gif)        
       ![]_ ]_](_urbrack.gif)        
  
    ![]_ ]_](_urbrack.gif)    |
57 | 47, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
      
       ![]. ].](_drbrack.gif)        
       ![]_ ]_](_urbrack.gif)        
  
    ![]_ ]_](_urbrack.gif)   |
58 | | csbcog 36241 |
. . . . . . . . . . . . . . . . . . . . 21
     
  
                ![]_ ]_](_urbrack.gif)         
  
    ![]_ ]_](_urbrack.gif)      
       ![]_ ]_](_urbrack.gif)    |
59 | 47, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
     
  
    ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)   |
60 | 53, 53 | coeq12i 4998 |
. . . . . . . . . . . . . . . . . . . 20
      
       ![]_ ]_](_urbrack.gif)      
       ![]_ ]_](_urbrack.gif)                           |
61 | 59, 60 | eqtri 2473 |
. . . . . . . . . . . . . . . . . . 19
     
  
    ![]_ ]_](_urbrack.gif)        
          
        |
62 | 61, 53 | sseq12i 3458 |
. . . . . . . . . . . . . . . . . 18
      
       ![]_ ]_](_urbrack.gif)        
  
    ![]_ ]_](_urbrack.gif)
     
  
       
                    |
63 | 57, 62 | bitri 253 |
. . . . . . . . . . . . . . . . 17
      
       ![]. ].](_drbrack.gif)        
          
                    |
64 | 55, 63 | anbi12i 703 |
. . . . . . . . . . . . . . . 16
               ![]. ].](_drbrack.gif)      
  
    ![]. ].](_drbrack.gif)         
                             
              |
65 | 46, 64 | bitri 253 |
. . . . . . . . . . . . . . 15
      
       ![]. ].](_drbrack.gif)          
                             
              |
66 | | sbceq2g 3779 |
. . . . . . . . . . . . . . . . 17
     
  
         
  
    ![]. ].](_drbrack.gif)      
     
       ![]_ ]_](_urbrack.gif)          |
67 | 47, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
      
       ![]. ].](_drbrack.gif)      
     
       ![]_ ]_](_urbrack.gif)         |
68 | | csbima12 5185 |
. . . . . . . . . . . . . . . . . 18
     
  
    ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)     |
69 | 53 | imaeq1i 5165 |
. . . . . . . . . . . . . . . . . 18
      
       ![]_ ]_](_urbrack.gif)        
  
    ![]_ ]_](_urbrack.gif)         
  
          
       ![]_ ]_](_urbrack.gif)     |
70 | | csbconstg 3376 |
. . . . . . . . . . . . . . . . . . . 20
     
  
                ![]_ ]_](_urbrack.gif)  
    |
71 | 47, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     
  
    ![]_ ]_](_urbrack.gif)      |
72 | 71 | imaeq2i 5166 |
. . . . . . . . . . . . . . . . . 18
     
  
          
       ![]_ ]_](_urbrack.gif)         
  
         |
73 | 68, 69, 72 | 3eqtri 2477 |
. . . . . . . . . . . . . . . . 17
     
  
    ![]_ ]_](_urbrack.gif)                         |
74 | 73 | eqeq2i 2463 |
. . . . . . . . . . . . . . . 16
              ![]_ ]_](_urbrack.gif)      
                   |
75 | 67, 74 | bitri 253 |
. . . . . . . . . . . . . . 15
      
       ![]. ].](_drbrack.gif)      
                   |
76 | 65, 75 | anbi12i 703 |
. . . . . . . . . . . . . 14
               ![]. ].](_drbrack.gif)          
       ![]. ].](_drbrack.gif)       
                                         
  
         
              |
77 | 45, 76 | bitr2i 254 |
. . . . . . . . . . . . 13
       
  
                          
                             
             ![]. ].](_drbrack.gif)     
         |
78 | 77 | biimpi 198 |
. . . . . . . . . . . 12
       
  
                          
                                   
       ![]. ].](_drbrack.gif)     
         |
79 | 19, 21, 44, 78 | syl21anc 1267 |
. . . . . . . . . . 11
  

              
  
    ![]. ].](_drbrack.gif)     
         |
80 | 79 | spesbcd 3350 |
. . . . . . . . . 10
  

               
         |
81 | 80 | ex 436 |
. . . . . . . . 9
 
             
 

          |
82 | | eqeq1 2455 |
. . . . . . . . . . . 12
                 |
83 | 82 | rexbidv 2901 |
. . . . . . . . . . 11
  
            
  
 
            |
84 | | imaeq1 5163 |
. . . . . . . . . . . . 13
               |
85 | 84 | eqeq2d 2461 |
. . . . . . . . . . . 12
                 |
86 | 85 | rexab2 3205 |
. . . . . . . . . . 11
              
      
         |
87 | 83, 86 | syl6bb 265 |
. . . . . . . . . 10
  
            
      
          |
88 | 13, 87 | elab 3185 |
. . . . . . . . 9
                
      
         |
89 | 81, 88 | syl6ibr 231 |
. . . . . . . 8
 
             
 
             |
90 | | intss1 4249 |
. . . . . . . 8
                     
 
            |
91 | 89, 90 | syl6 34 |
. . . . . . 7
 
                              |
92 | 91 | alrimiv 1773 |
. . . . . 6
 
                                |
93 | | ssintab 4251 |
. . . . . 6
     
 
                                                    |
94 | 92, 93 | sylibr 216 |
. . . . 5
 
                               |
95 | | ssintab 4251 |
. . . . . . 7
        
 
   
             
     
 
                   
   |
96 | 84 | eqeq2d 2461 |
. . . . . . . . . 10
                 |
97 | 96 | rexab2 3205 |
. . . . . . . . 9
              
      
         |
98 | | simpr 463 |
. . . . . . . . . . 11
    

               |
99 | | imass1 5203 |
. . . . . . . . . . . . . . 15
      
        |
100 | 99 | adantr 467 |
. . . . . . . . . . . . . 14
 
 
               |
101 | | imass1 5203 |
. . . . . . . . . . . . . . 15
                       |
102 | | imaco 5340 |
. . . . . . . . . . . . . . . 16
                   |
103 | | imass1 5203 |
. . . . . . . . . . . . . . . 16
                   |
104 | 102, 103 | syl5eqssr 3477 |
. . . . . . . . . . . . . . 15
                     |
105 | 101, 104 | sylan9ss 3445 |
. . . . . . . . . . . . . 14
 
 
                   |
106 | 100, 105 | jca 535 |
. . . . . . . . . . . . 13
 
 
                                 |
107 | 106 | adantr 467 |
. . . . . . . . . . . 12
    

                                       |
108 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
109 | | imaexg 6730 |
. . . . . . . . . . . . . 14
         |
110 | 108, 109 | ax-mp 5 |
. . . . . . . . . . . . 13
       |
111 | | imaundi 5248 |
. . . . . . . . . . . . . . . 16
     
               |
112 | 111 | sseq1i 3456 |
. . . . . . . . . . . . . . 15
                       |
113 | | unss 3608 |
. . . . . . . . . . . . . . 15
           
               |
114 | 112, 113 | bitr4i 256 |
. . . . . . . . . . . . . 14
                   
   |
115 | | imaeq2 5164 |
. . . . . . . . . . . . . . . 16
                       |
116 | | id 22 |
. . . . . . . . . . . . . . . 16
               |
117 | 115, 116 | sseq12d 3461 |
. . . . . . . . . . . . . . 15
                               |
118 | 117 | cleq2lem 36214 |
. . . . . . . . . . . . . 14
              
    
      
                          |
119 | 114, 118 | syl5bb 261 |
. . . . . . . . . . . . 13
                                                 |
120 | 110, 119 | elab 3185 |
. . . . . . . . . . . 12
             
 
                                 |
121 | 107, 120 | sylibr 216 |
. . . . . . . . . . 11
    

                   
 
   |
122 | 98, 121 | eqeltrd 2529 |
. . . . . . . . . 10
    

                   |
123 | 122 | exlimiv 1776 |
. . . . . . . . 9
       
      
      
 
   |
124 | 97, 123 | sylbi 199 |
. . . . . . . 8
                           |
125 | | intss1 4249 |
. . . . . . . 8
                        |
126 | 124, 125 | syl 17 |
. . . . . . 7
                         
  |
127 | 95, 126 | mpgbir 1673 |
. . . . . 6
          
    
 
           |
128 | 127 | a1i 11 |
. . . . 5
 
                               |
129 | 94, 128 | eqssd 3449 |
. . . 4
 
                         
 
   |
130 | 10, 129 | eqtrd 2485 |
. . 3
 
                     
 
   |
131 | 130 | eleq2d 2514 |
. 2
 
     
 
      
              |
132 | 8, 131 | bitrd 257 |
1
 
        
              |