Step | Hyp | Ref
| Expression |
1 | | xp1st 6842 |
. . . . . 6
         |
2 | 1 | adantl 473 |
. . . . 5
 

        |
3 | | xpf1o.1 |
. . . . . . . 8
         |
4 | | eqid 2471 |
. . . . . . . . 9
     |
5 | 4 | f1ompt 6059 |
. . . . . . . 8
      
 


   |
6 | 3, 5 | sylib 201 |
. . . . . . 7
    
   |
7 | 6 | simpld 466 |
. . . . . 6
 
  |
8 | 7 | adantr 472 |
. . . . 5
 

  
  |
9 | | nfcsb1v 3365 |
. . . . . . 7
        ![]_ ]_](_urbrack.gif)  |
10 | 9 | nfel1 2626 |
. . . . . 6
        ![]_ ]_](_urbrack.gif)
 |
11 | | csbeq1a 3358 |
. . . . . . 7
    
      ![]_ ]_](_urbrack.gif)   |
12 | 11 | eleq1d 2533 |
. . . . . 6
    

      ![]_ ]_](_urbrack.gif)
   |
13 | 10, 12 | rspc 3130 |
. . . . 5
      
      ![]_ ]_](_urbrack.gif)
   |
14 | 2, 8, 13 | sylc 61 |
. . . 4
 

        ![]_ ]_](_urbrack.gif)   |
15 | | xp2nd 6843 |
. . . . . 6
         |
16 | 15 | adantl 473 |
. . . . 5
 

        |
17 | | xpf1o.2 |
. . . . . . . 8
         |
18 | | eqid 2471 |
. . . . . . . . 9
     |
19 | 18 | f1ompt 6059 |
. . . . . . . 8
      
 


   |
20 | 17, 19 | sylib 201 |
. . . . . . 7
    
   |
21 | 20 | simpld 466 |
. . . . . 6
 
  |
22 | 21 | adantr 472 |
. . . . 5
 

  
  |
23 | | nfcsb1v 3365 |
. . . . . . 7
        ![]_ ]_](_urbrack.gif)  |
24 | 23 | nfel1 2626 |
. . . . . 6
        ![]_ ]_](_urbrack.gif)
 |
25 | | csbeq1a 3358 |
. . . . . . 7
    
      ![]_ ]_](_urbrack.gif)   |
26 | 25 | eleq1d 2533 |
. . . . . 6
    

      ![]_ ]_](_urbrack.gif)
   |
27 | 24, 26 | rspc 3130 |
. . . . 5
      
      ![]_ ]_](_urbrack.gif)
   |
28 | 16, 22, 27 | sylc 61 |
. . . 4
 

        ![]_ ]_](_urbrack.gif)   |
29 | | opelxpi 4871 |
. . . 4
        ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)
        ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
    |
30 | 14, 28, 29 | syl2anc 673 |
. . 3
 

         ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)      |
31 | 30 | ralrimiva 2809 |
. 2
            ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
    |
32 | 6 | simprd 470 |
. . . . . . . . . 10
  
  |
33 | 32 | r19.21bi 2776 |
. . . . . . . . 9
 
 
  |
34 | | reu6 3215 |
. . . . . . . . 9
 



   |
35 | 33, 34 | sylib 201 |
. . . . . . . 8
 
 


   |
36 | 20 | simprd 470 |
. . . . . . . . . 10
  
  |
37 | 36 | r19.21bi 2776 |
. . . . . . . . 9
 
 
  |
38 | | reu6 3215 |
. . . . . . . . 9
 



   |
39 | 37, 38 | sylib 201 |
. . . . . . . 8
 
 


   |
40 | 35, 39 | anim12dan 855 |
. . . . . . 7
 

     




    |
41 | | reeanv 2944 |
. . . . . . . 8
  
 
     
 


 


    |
42 | | pm4.38 889 |
. . . . . . . . . . . . . . 15
               |
43 | 42 | ex 441 |
. . . . . . . . . . . . . 14
 
      

     |
44 | 43 | ralimdv 2806 |
. . . . . . . . . . . . 13
 
  

 
  

     |
45 | 44 | com12 31 |
. . . . . . . . . . . 12
 

       

     |
46 | 45 | ralimdv 2806 |
. . . . . . . . . . 11
 

  
   
  

     |
47 | 46 | impcom 437 |
. . . . . . . . . 10
         

 
 
    |
48 | 47 | reximi 2852 |
. . . . . . . . 9
          


 
 
    |
49 | 48 | reximi 2852 |
. . . . . . . 8
  
 
      



 
 
    |
50 | 41, 49 | sylbir 218 |
. . . . . . 7
   
       



 
 
    |
51 | 40, 50 | syl 17 |
. . . . . 6
 

  



  

    |
52 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
53 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
54 | 52, 53 | op1std 6822 |
. . . . . . . . . . . . . 14
          |
55 | 54 | csbeq1d 3356 |
. . . . . . . . . . . . 13
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
56 | 55 | eqeq2d 2481 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
57 | 52, 53 | op2ndd 6823 |
. . . . . . . . . . . . . 14
          |
58 | 57 | csbeq1d 3356 |
. . . . . . . . . . . . 13
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
59 | 58 | eqeq2d 2481 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
60 | 56, 59 | anbi12d 725 |
. . . . . . . . . . 11
            ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
61 | | eqeq1 2475 |
. . . . . . . . . . 11
       
   |
62 | 60, 61 | bibi12d 328 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 

    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
  
    |
63 | 62 | ralxp 4981 |
. . . . . . . . 9
 
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 



    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
  
   |
64 | | nfv 1769 |
. . . . . . . . . 10
     
  
  |
65 | | nfcv 2612 |
. . . . . . . . . . 11
   |
66 | | nfcsb1v 3365 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
67 | 66 | nfeq2 2627 |
. . . . . . . . . . . . 13

  ![]_ ]_](_urbrack.gif)  |
68 | | nfv 1769 |
. . . . . . . . . . . . 13

  ![]_ ]_](_urbrack.gif)  |
69 | 67, 68 | nfan 2031 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
70 | | nfv 1769 |
. . . . . . . . . . . 12
      |
71 | 69, 70 | nfbi 2037 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
  
  |
72 | 65, 71 | nfral 2789 |
. . . . . . . . . 10
  
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
  
  |
73 | | nfv 1769 |
. . . . . . . . . . . 12
    
  
  |
74 | | nfv 1769 |
. . . . . . . . . . . . . 14
  |
75 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . 15
  
 ![]_ ]_](_urbrack.gif)  |
76 | 75 | nfeq2 2627 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)  |
77 | 74, 76 | nfan 2031 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)   |
78 | | nfv 1769 |
. . . . . . . . . . . . 13
      |
79 | 77, 78 | nfbi 2037 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif) 
  
  |
80 | | csbeq1a 3358 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)   |
81 | 80 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
 
  ![]_ ]_](_urbrack.gif)    |
82 | 81 | anbi2d 718 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)     |
83 | | opeq2 4159 |
. . . . . . . . . . . . . 14
         |
84 | 83 | eqeq1d 2473 |
. . . . . . . . . . . . 13
    
  
   |
85 | 82, 84 | bibi12d 328 |
. . . . . . . . . . . 12
    
  
     ![]_ ]_](_urbrack.gif) 
  
    |
86 | 73, 79, 85 | cbvral 3001 |
. . . . . . . . . . 11
 
     
      ![]_ ]_](_urbrack.gif)    
   |
87 | | csbeq1a 3358 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)   |
88 | 87 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
 
  ![]_ ]_](_urbrack.gif)    |
89 | 88 | anbi1d 719 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
90 | | opeq1 4158 |
. . . . . . . . . . . . . 14
         |
91 | 90 | eqeq1d 2473 |
. . . . . . . . . . . . 13
    
  
   |
92 | 89, 91 | bibi12d 328 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif) 
  
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
  
    |
93 | 92 | ralbidv 2829 |
. . . . . . . . . . 11
  
    ![]_ ]_](_urbrack.gif) 
  
      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
  
    |
94 | 86, 93 | syl5bb 265 |
. . . . . . . . . 10
  
  
  
      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
  
    |
95 | 64, 72, 94 | cbvral 3001 |
. . . . . . . . 9
 

     
  
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    
   |
96 | 63, 95 | bitr4i 260 |
. . . . . . . 8
 
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 



 
       |
97 | | eqeq2 2482 |
. . . . . . . . . . 11
                 |
98 | | vex 3034 |
. . . . . . . . . . . 12
 |
99 | | vex 3034 |
. . . . . . . . . . . 12
 |
100 | 98, 99 | opth 4676 |
. . . . . . . . . . 11
           |
101 | 97, 100 | syl6bb 269 |
. . . . . . . . . 10
             |
102 | 101 | bibi2d 325 |
. . . . . . . . 9
      
    
 
 
     |
103 | 102 | 2ralbidv 2832 |
. . . . . . . 8
     

 
    


 
 
     |
104 | 96, 103 | syl5bb 265 |
. . . . . . 7
                 ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif) 



 
 
     |
105 | 104 | rexxp 4982 |
. . . . . 6
     
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 





 
 
    |
106 | 51, 105 | sylibr 217 |
. . . . 5
 

  
   
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
   |
107 | | reu6 3215 |
. . . . 5
            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
                ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif) 
   |
108 | 106, 107 | sylibr 217 |
. . . 4
 

  
          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
109 | 108 | ralrimivva 2814 |
. . 3
  

          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
110 | | eqeq1 2475 |
. . . . . 6
            ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)     |
111 | | vex 3034 |
. . . . . . 7
 |
112 | | vex 3034 |
. . . . . . 7
 |
113 | 111, 112 | opth 4676 |
. . . . . 6
           ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
114 | 110, 113 | syl6bb 269 |
. . . . 5
            ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
115 | 114 | reubidv 2961 |
. . . 4
                ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
           ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)     |
116 | 115 | ralxp 4981 |
. . 3
 
              ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
 

          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
117 | 109, 116 | sylibr 217 |
. 2
                ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    |
118 | | nfcv 2612 |
. . . . 5
      |
119 | | nfcv 2612 |
. . . . 5
      |
120 | | nfcsb1v 3365 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)  |
121 | | nfcv 2612 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)  |
122 | 120, 121 | nfop 4174 |
. . . . 5
     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
123 | | nfcv 2612 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)  |
124 | | nfcsb1v 3365 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)  |
125 | 123, 124 | nfop 4174 |
. . . . 5
     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
126 | | csbeq1a 3358 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)   |
127 | | csbeq1a 3358 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)   |
128 | | opeq12 4160 |
. . . . . 6
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
129 | 126, 127,
128 | syl2an 485 |
. . . . 5
 
       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
130 | 118, 119,
122, 125, 129 | cbvmpt2 6389 |
. . . 4
       
 
 ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
131 | 111, 112 | op1std 6822 |
. . . . . . 7
          |
132 | 131 | csbeq1d 3356 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
133 | 111, 112 | op2ndd 6823 |
. . . . . . 7
          |
134 | 133 | csbeq1d 3356 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
135 | 132, 134 | opeq12d 4166 |
. . . . 5
           ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif) 
  ![]_ ]_](_urbrack.gif)    |
136 | 135 | mpt2mpt 6407 |
. . . 4
          ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    
   ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)    |
137 | 130, 136 | eqtr4i 2496 |
. . 3
                ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)    |
138 | 137 | f1ompt 6059 |
. 2
    
                      ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif) 
                 ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)     |
139 | 31, 117, 138 | sylanbrc 677 |
1
  
              |