Proof of Theorem br8
Step | Hyp | Ref
| Expression |
1 | | opex 4678 |
. . 3
          |
2 | | opex 4678 |
. . 3
          |
3 | | eqeq1 2466 |
. . . . . . . . 9
         
     
                         |
4 | 3 | 3anbi1d 1352 |
. . . . . . . 8
         
               
   

   
          
   
    
   
    |
5 | 4 | rexbidv 2913 |
. . . . . . 7
         
 
              
   


   
          
   
    
   
    |
6 | 5 | 2rexbidv 2920 |
. . . . . 6
         
 


              
   




   
          
   
    
   
    |
7 | 6 | 2rexbidv 2920 |
. . . . 5
         
 




              
   






   
          
   
    
   
    |
8 | 7 | 2rexbidv 2920 |
. . . 4
         
 






              
   








   
          
   
    
   
    |
9 | 8 | 2rexbidv 2920 |
. . 3
         
 








              
   










   
          
   
    
   
    |
10 | | eqeq1 2466 |
. . . . . . . . 9
         
     
                         |
11 | 10 | 3anbi2d 1353 |
. . . . . . . 8
         
                        
   

   
          
   
                      |
12 | 11 | rexbidv 2913 |
. . . . . . 7
         
 
                       
   


   
          
   
                      |
13 | 12 | 2rexbidv 2920 |
. . . . . 6
         
 


                       
   




   
          
   
                      |
14 | 13 | 2rexbidv 2920 |
. . . . 5
         
 




                       
   






   
          
   
                      |
15 | 14 | 2rexbidv 2920 |
. . . 4
         
 






                       
   








   
          
   
                      |
16 | 15 | 2rexbidv 2920 |
. . 3
         
 








                       
   










   
          
   
                      |
17 | | br8.10 |
. . 3
   









     
   
    
   
   |
18 | 1, 2, 9, 16, 17 | brab 4738 |
. 2
                      







                     
          
   
   |
19 | | opex 4678 |
. . . . . . . . . . . . . 14
    |
20 | | opex 4678 |
. . . . . . . . . . . . . 14
    |
21 | 19, 20 | opth 4690 |
. . . . . . . . . . . . 13
                      
  
  
      |
22 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
23 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
24 | 22, 23 | opth 4690 |
. . . . . . . . . . . . . . 15
           |
25 | | br8.1 |
. . . . . . . . . . . . . . . 16
     |
26 | | br8.2 |
. . . . . . . . . . . . . . . 16
     |
27 | 25, 26 | sylan9bb 711 |
. . . . . . . . . . . . . . 15
 
 
   |
28 | 24, 27 | sylbi 200 |
. . . . . . . . . . . . . 14
       
   |
29 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
30 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
31 | 29, 30 | opth 4690 |
. . . . . . . . . . . . . . 15
           |
32 | | br8.3 |
. . . . . . . . . . . . . . . 16
     |
33 | | br8.4 |
. . . . . . . . . . . . . . . 16
     |
34 | 32, 33 | sylan9bb 711 |
. . . . . . . . . . . . . . 15
 
 
   |
35 | 31, 34 | sylbi 200 |
. . . . . . . . . . . . . 14
       
   |
36 | 28, 35 | sylan9bb 711 |
. . . . . . . . . . . . 13
          
        |
37 | 21, 36 | sylbi 200 |
. . . . . . . . . . . 12
                  
    |
38 | 37 | eqcoms 2470 |
. . . . . . . . . . 11
              
   
    |
39 | | opex 4678 |
. . . . . . . . . . . . . 14
    |
40 | | opex 4678 |
. . . . . . . . . . . . . 14
  
 |
41 | 39, 40 | opth 4690 |
. . . . . . . . . . . . 13
                      
  
  
      |
42 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
43 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
44 | 42, 43 | opth 4690 |
. . . . . . . . . . . . . . 15
           |
45 | | br8.5 |
. . . . . . . . . . . . . . . 16
     |
46 | | br8.6 |
. . . . . . . . . . . . . . . 16
     |
47 | 45, 46 | sylan9bb 711 |
. . . . . . . . . . . . . . 15
 
 
   |
48 | 44, 47 | sylbi 200 |
. . . . . . . . . . . . . 14
       
   |
49 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
50 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
51 | 49, 50 | opth 4690 |
. . . . . . . . . . . . . . 15
       
   |
52 | | br8.7 |
. . . . . . . . . . . . . . . 16
     |
53 | | br8.8 |
. . . . . . . . . . . . . . . 16
     |
54 | 52, 53 | sylan9bb 711 |
. . . . . . . . . . . . . . 15
 
 
   |
55 | 51, 54 | sylbi 200 |
. . . . . . . . . . . . . 14
       
   |
56 | 48, 55 | sylan9bb 711 |
. . . . . . . . . . . . 13
              
    |
57 | 41, 56 | sylbi 200 |
. . . . . . . . . . . 12
                  
    |
58 | 57 | eqcoms 2470 |
. . . . . . . . . . 11
              
   
    |
59 | 38, 58 | sylan9bb 711 |
. . . . . . . . . 10
                      
          
         |
60 | 59 | biimp3a 1379 |
. . . . . . . . 9
                      
          
   
   |
61 | 60 | a1i 11 |
. . . . . . . 8
         
 
  
 

  
  
 
                       
          
   
    |
62 | 61 | rexlimdva 2891 |
. . . . . . 7
      


 
 

  
  
 

                         
          
   
    |
63 | 62 | rexlimdvva 2898 |
. . . . . 6
     
 


  
  
 

                           
          
   
    |
64 | 63 | rexlimdvva 2898 |
. . . . 5
    
 
 
  
 

                             
          
   
    |
65 | 64 | rexlimdvva 2898 |
. . . 4
     
 
  
 
 






                     
          
   
    |
66 | 65 | rexlimdvva 2898 |
. . 3
  


 
 
 








                     
          
   
    |
67 | | simpl11 1089 |
. . . . 5
     
 
     |
68 | | simpl12 1090 |
. . . . . 6
     
 
     |
69 | | simpl13 1091 |
. . . . . 6
     
 
     |
70 | | simpl21 1092 |
. . . . . 6
     
 
     |
71 | | simpl22 1093 |
. . . . . . 7
     
 
     |
72 | | simpl23 1094 |
. . . . . . 7
     
 
     |
73 | | simpl31 1095 |
. . . . . . 7
     
 
     |
74 | | simpl32 1096 |
. . . . . . . 8
     
 
     |
75 | | simpl33 1097 |
. . . . . . . 8
     
 
     |
76 | | eqidd 2463 |
. . . . . . . 8
     
 
                       |
77 | | eqidd 2463 |
. . . . . . . 8
     
 
                       |
78 | | simpr 467 |
. . . . . . . 8
     
 
     |
79 | | opeq1 4180 |
. . . . . . . . . . . 12
   
     |
80 | 79 | opeq2d 4187 |
. . . . . . . . . . 11
                     |
81 | 80 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
82 | 81, 52 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                 
                   
                 
    |
83 | | opeq2 4181 |
. . . . . . . . . . . 12
         |
84 | 83 | opeq2d 4187 |
. . . . . . . . . . 11
                     |
85 | 84 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
86 | 85, 53 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                 
                   
                 
    |
87 | 82, 86 | rspc2ev 3173 |
. . . . . . . 8
 
                  
                 
 


   
              
                 
   |
88 | 74, 75, 76, 77, 78, 87 | syl113anc 1288 |
. . . . . . 7
     
 
    
                  
                 
   |
89 | | opeq2 4181 |
. . . . . . . . . . . 12
         |
90 | 89 | opeq2d 4187 |
. . . . . . . . . . 11
                     |
91 | 90 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
92 | 91, 33 | 3anbi13d 1350 |
. . . . . . . . 9
                    
                                     
                      |
93 | 92 | 2rexbidv 2920 |
. . . . . . . 8
  

                  
                    
                  
                      |
94 | | opeq1 4180 |
. . . . . . . . . . . 12
         |
95 | 94 | opeq1d 4186 |
. . . . . . . . . . 11
            
        |
96 | 95 | eqeq2d 2472 |
. . . . . . . . . 10
                   
                     |
97 | 96, 45 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                                     
                 
    |
98 | 97 | 2rexbidv 2920 |
. . . . . . . 8
  

                  
                    
                  
                 
    |
99 | | opeq2 4181 |
. . . . . . . . . . . 12
         |
100 | 99 | opeq1d 4186 |
. . . . . . . . . . 11
                     |
101 | 100 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
102 | 101, 46 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                 
                   
                 
    |
103 | 102 | 2rexbidv 2920 |
. . . . . . . 8
  

                  
                 
  
                  
                 
    |
104 | 93, 98, 103 | rspc3ev 3175 |
. . . . . . 7
  



   
              
                 
 





   
              
                     |
105 | 71, 72, 73, 88, 104 | syl31anc 1279 |
. . . . . 6
     
 
    



                  
                     |
106 | | opeq1 4180 |
. . . . . . . . . . . . 13
         |
107 | 106 | opeq1d 4186 |
. . . . . . . . . . . 12
            
        |
108 | 107 | eqeq2d 2472 |
. . . . . . . . . . 11
                   
                     |
109 | 108, 25 | 3anbi13d 1350 |
. . . . . . . . . 10
                       
          
   

   
          
   
                      |
110 | 109 | rexbidv 2913 |
. . . . . . . . 9
  
                     
          
   


   
          
   
                      |
111 | 110 | 2rexbidv 2920 |
. . . . . . . 8
  


                     
          
   




   
          
   
                      |
112 | 111 | 2rexbidv 2920 |
. . . . . . 7
  




                     
          
   






   
          
   
                      |
113 | | opeq2 4181 |
. . . . . . . . . . . . 13
         |
114 | 113 | opeq1d 4186 |
. . . . . . . . . . . 12
            
        |
115 | 114 | eqeq2d 2472 |
. . . . . . . . . . 11
                   
                     |
116 | 115, 26 | 3anbi13d 1350 |
. . . . . . . . . 10
                       
          
   
                      
          
   
    |
117 | 116 | rexbidv 2913 |
. . . . . . . . 9
  
                     
          
   
                       
          
   
    |
118 | 117 | 2rexbidv 2920 |
. . . . . . . 8
  


                     
          
   
  

                     
          
   
    |
119 | 118 | 2rexbidv 2920 |
. . . . . . 7
  




                     
          
   
  



                     
          
   
    |
120 | | opeq1 4180 |
. . . . . . . . . . . . 13
         |
121 | 120 | opeq2d 4187 |
. . . . . . . . . . . 12
            
        |
122 | 121 | eqeq2d 2472 |
. . . . . . . . . . 11
                   
                     |
123 | 122, 32 | 3anbi13d 1350 |
. . . . . . . . . 10
                       
          
   
                   
                      |
124 | 123 | rexbidv 2913 |
. . . . . . . . 9
  
                     
          
   
                    
                      |
125 | 124 | 2rexbidv 2920 |
. . . . . . . 8
  


                     
          
   
  

                  
                      |
126 | 125 | 2rexbidv 2920 |
. . . . . . 7
  




                     
          
   
  



                  
                      |
127 | 112, 119,
126 | rspc3ev 3175 |
. . . . . 6
  






   
              
                    







   
          
   
                     |
128 | 68, 69, 70, 105, 127 | syl31anc 1279 |
. . . . 5
     
 
    






                     
          
   
   |
129 | | br8.9 |
. . . . . . 7
   |
130 | 129 | rexeqdv 3006 |
. . . . . . . . . . . . 13
  
                     
          
   


   
          
   
                      |
131 | 129, 130 | rexeqbidv 3014 |
. . . . . . . . . . . 12
  

                     
          
   



   
          
   
                      |
132 | 129, 131 | rexeqbidv 3014 |
. . . . . . . . . . 11
  


                     
          
   




   
          
   
                      |
133 | 129, 132 | rexeqbidv 3014 |
. . . . . . . . . 10
  



                     
          
   





   
          
   
                      |
134 | 129, 133 | rexeqbidv 3014 |
. . . . . . . . 9
  




                     
          
   






   
          
   
                      |
135 | 129, 134 | rexeqbidv 3014 |
. . . . . . . 8
  





                     
          
   







   
          
   
                      |
136 | 129, 135 | rexeqbidv 3014 |
. . . . . . 7
  






                     
          
   








   
          
   
                      |
137 | 129, 136 | rexeqbidv 3014 |
. . . . . 6
  







                     
          
   









   
          
   
                      |
138 | 137 | rspcev 3162 |
. . . . 5
   






                     
          
   
   







                     
          
   
   |
139 | 67, 128, 138 | syl2anc 671 |
. . . 4
     
 
    







                     
          
   
   |
140 | 139 | ex 440 |
. . 3
  


 
 
  







                     
          
   
    |
141 | 66, 140 | impbid 195 |
. 2
  


 
 
 








                     
          
   

   |
142 | 18, 141 | syl5bb 265 |
1
  


 
 
   
                    |