Proof of Theorem br8d
Step | Hyp | Ref
| Expression |
1 | | br8d.10 |
. . . 4
     







              
   
    |
2 | 1 | breqd 4427 |
. . 3
                                    







              
   
               |
3 | | opex 4678 |
. . . 4
          |
4 | | opex 4678 |
. . . 4
          |
5 | | eqeq1 2466 |
. . . . . . . . . 10
         
     
                         |
6 | 5 | 3anbi1d 1352 |
. . . . . . . . 9
         
               
   
                        
   
    |
7 | 6 | rexbidv 2913 |
. . . . . . . 8
         
 
              
   
                         
   
    |
8 | 7 | 2rexbidv 2920 |
. . . . . . 7
         
 


              
   
  

                       
   
    |
9 | 8 | 2rexbidv 2920 |
. . . . . 6
         
 




              
   
  



                       
   
    |
10 | 9 | 2rexbidv 2920 |
. . . . 5
         
 






              
   
  





                       
   
    |
11 | 10 | rexbidv 2913 |
. . . 4
         
 







              
   
  






                       
   
    |
12 | | eqeq1 2466 |
. . . . . . . . . 10
         
     
                         |
13 | 12 | 3anbi2d 1353 |
. . . . . . . . 9
         
                        
   
                      
          
   
    |
14 | 13 | rexbidv 2913 |
. . . . . . . 8
         
 
                       
   
                       
          
   
    |
15 | 14 | 2rexbidv 2920 |
. . . . . . 7
         
 


                       
   
  

                     
          
   
    |
16 | 15 | 2rexbidv 2920 |
. . . . . 6
         
 




                       
   
  



                     
          
   
    |
17 | 16 | 2rexbidv 2920 |
. . . . 5
         
 






                       
   
  





                     
          
   
    |
18 | 17 | rexbidv 2913 |
. . . 4
         
 







                       
   
  






                     
          
   
    |
19 | | eqid 2462 |
. . . 4
    







              
   
 
    







              
   
   |
20 | 3, 4, 11, 18, 19 | brab 4738 |
. . 3
              








     
   
    
   
             






                     
          
   
   |
21 | 2, 20 | syl6bb 269 |
. 2
                       






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

  
                         
          
   
    |
73 | 72 | rexlimdva 2891 |
. . . . . . . 8
      


 
 
 
 

  
   
                     
          
   
    |
74 | 73 | rexlimdvva 2898 |
. . . . . . 7
     
 


 
 
  
 
 


                     
          
   
    |
75 | 74 | rexlimdvva 2898 |
. . . . . 6
      
 
   
 
 




                     
          
   
    |
76 | 75 | rexlimdvva 2898 |
. . . . 5
     
 
    






                     
          
   
    |
77 | 76 | rexlimdva 2891 |
. . . 4
  


 
 
 







                     
          
   
    |
78 | | simpl1l 1065 |
. . . . . 6
     
 
     |
79 | | simpl1r 1066 |
. . . . . 6
     
 
     |
80 | | simpl21 1092 |
. . . . . 6
     
 
     |
81 | | simpl22 1093 |
. . . . . . 7
     
 
     |
82 | | simpl23 1094 |
. . . . . . 7
     
 
     |
83 | | simpl31 1095 |
. . . . . . 7
     
 
     |
84 | | simpl32 1096 |
. . . . . . . 8
     
 
     |
85 | | simpl33 1097 |
. . . . . . . 8
     
 
     |
86 | | eqidd 2463 |
. . . . . . . 8
     
 
                       |
87 | | eqidd 2463 |
. . . . . . . 8
     
 
                       |
88 | | simpr 467 |
. . . . . . . 8
     
 
     |
89 | | opeq1 4180 |
. . . . . . . . . . . 12
   
     |
90 | 89 | opeq2d 4187 |
. . . . . . . . . . 11
                     |
91 | 90 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
92 | 91, 63 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                 
                   
                 
    |
93 | | opeq2 4181 |
. . . . . . . . . . . 12
         |
94 | 93 | opeq2d 4187 |
. . . . . . . . . . 11
                     |
95 | 94 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
96 | 95, 64 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                 
                   
                 
    |
97 | 92, 96 | rspc2ev 3173 |
. . . . . . . 8
 
                  
                 
 


   
              
                 
   |
98 | 84, 85, 86, 87, 88, 97 | syl113anc 1288 |
. . . . . . 7
     
 
    
                  
                 
   |
99 | | opeq2 4181 |
. . . . . . . . . . . 12
         |
100 | 99 | opeq2d 4187 |
. . . . . . . . . . 11
                     |
101 | 100 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
102 | 101, 44 | 3anbi13d 1350 |
. . . . . . . . 9
                    
                                     
                      |
103 | 102 | 2rexbidv 2920 |
. . . . . . . 8
  

                  
                    
                  
                      |
104 | | opeq1 4180 |
. . . . . . . . . . . 12
         |
105 | 104 | opeq1d 4186 |
. . . . . . . . . . 11
            
        |
106 | 105 | eqeq2d 2472 |
. . . . . . . . . 10
                   
                     |
107 | 106, 56 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                                     
                 
    |
108 | 107 | 2rexbidv 2920 |
. . . . . . . 8
  

                  
                    
                  
                 
    |
109 | | opeq2 4181 |
. . . . . . . . . . . 12
         |
110 | 109 | opeq1d 4186 |
. . . . . . . . . . 11
                     |
111 | 110 | eqeq2d 2472 |
. . . . . . . . . 10
                                         |
112 | 111, 57 | 3anbi23d 1351 |
. . . . . . . . 9
                    
                 
                   
                 
    |
113 | 112 | 2rexbidv 2920 |
. . . . . . . 8
  

                  
                 
  
                  
                 
    |
114 | 103, 108,
113 | rspc3ev 3175 |
. . . . . . 7
  



   
              
                 
 





   
              
                     |
115 | 81, 82, 83, 98, 114 | syl31anc 1279 |
. . . . . 6
     
 
    



                  
                     |
116 | | opeq1 4180 |
. . . . . . . . . . . . 13
         |
117 | 116 | opeq1d 4186 |
. . . . . . . . . . . 12
            
        |
118 | 117 | eqeq2d 2472 |
. . . . . . . . . . 11
                   
                     |
119 | 118, 36 | 3anbi13d 1350 |
. . . . . . . . . 10
                       
          
   
                      
          
   
    |
120 | 119 | rexbidv 2913 |
. . . . . . . . 9
  
                     
          
   
                       
          
   
    |
121 | 120 | 2rexbidv 2920 |
. . . . . . . 8
  


                     
          
   
  

                     
          
   
    |
122 | 121 | 2rexbidv 2920 |
. . . . . . 7
  




                     
          
   
  



                     
          
   
    |
123 | | opeq2 4181 |
. . . . . . . . . . . . 13
         |
124 | 123 | opeq1d 4186 |
. . . . . . . . . . . 12
            
        |
125 | 124 | eqeq2d 2472 |
. . . . . . . . . . 11
                   
                     |
126 | 125, 37 | 3anbi13d 1350 |
. . . . . . . . . 10
                       
          
   
                      
          
   
    |
127 | 126 | rexbidv 2913 |
. . . . . . . . 9
  
                     
          
   
                       
          
   
    |
128 | 127 | 2rexbidv 2920 |
. . . . . . . 8
  


                     
          
   
  

                     
          
   
    |
129 | 128 | 2rexbidv 2920 |
. . . . . . 7
  




                     
          
   
  



                     
          
   
    |
130 | | opeq1 4180 |
. . . . . . . . . . . . 13
         |
131 | 130 | opeq2d 4187 |
. . . . . . . . . . . 12
            
        |
132 | 131 | eqeq2d 2472 |
. . . . . . . . . . 11
                   
                     |
133 | 132, 43 | 3anbi13d 1350 |
. . . . . . . . . 10
                       
          
   
                   
                      |
134 | 133 | rexbidv 2913 |
. . . . . . . . 9
  
                     
          
   
                    
                      |
135 | 134 | 2rexbidv 2920 |
. . . . . . . 8
  


                     
          
   
  

                  
                      |
136 | 135 | 2rexbidv 2920 |
. . . . . . 7
  




                     
          
   
  



                  
                      |
137 | 122, 129,
136 | rspc3ev 3175 |
. . . . . 6
  






   
              
                    







   
          
   
                     |
138 | 78, 79, 80, 115, 137 | syl31anc 1279 |
. . . . 5
     
 
    






                     
          
   
   |
139 | 138 | ex 440 |
. . . 4
  


 
 
  






                     
          
   
    |
140 | 77, 139 | impbid 195 |
. . 3
  


 
 
 







                     
          
   
    |
141 | 22, 23, 24, 25, 26, 27, 28, 29, 140 | syl233anc 1305 |
. 2
                               
          
   
    |
142 | 21, 141 | bitrd 261 |
1
                         |