Step | Hyp | Ref
| Expression |
1 | | f1od2.2 |
. . . 4
 

 
  |
2 | 1 | ralrimivva 2559 |
. . 3
  
  |
3 | | f1od2.1 |
. . . 4
 
  |
4 | 3 | fnmpo 6202 |
. . 3
 


   |
5 | 2, 4 | syl 14 |
. 2
     |
6 | | f1od2.3 |
. . . . . 6
 
 
   |
7 | | opelxpi 4658 |
. . . . . 6
 
        |
8 | 6, 7 | syl 14 |
. . . . 5
 
   
    |
9 | 8 | ralrimiva 2550 |
. . . 4
         |
10 | | eqid 2177 |
. . . . 5
           |
11 | 10 | fnmpt 5342 |
. . . 4
 
            |
12 | 9, 11 | syl 14 |
. . 3
        |
13 | | elxp7 6170 |
. . . . . . . 8
  
                |
14 | 13 | anbi1i 458 |
. . . . . . 7
   
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
15 | | anass 401 |
. . . . . . . . 9
                      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
                    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
16 | | f1od2.4 |
. . . . . . . . . . . . 13
     


     |
17 | 16 | sbcbidv 3021 |
. . . . . . . . . . . 12
        ![]. ].](_drbrack.gif)    
      ![]. ].](_drbrack.gif)        |
18 | 17 | sbcbidv 3021 |
. . . . . . . . . . 11
        ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)        |
19 | | sbcan 3005 |
. . . . . . . . . . . . . 14
       ![]. ].](_drbrack.gif)  


       ![]. ].](_drbrack.gif) 
       ![]. ].](_drbrack.gif)
   |
20 | | sbcan 3005 |
. . . . . . . . . . . . . . . 16
       ![]. ].](_drbrack.gif) 
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
   |
21 | | vex 2740 |
. . . . . . . . . . . . . . . . . . 19
 |
22 | | 2ndexg 6168 |
. . . . . . . . . . . . . . . . . . 19
       |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
     |
24 | | sbcg 3032 |
. . . . . . . . . . . . . . . . . 18
            ![]. ].](_drbrack.gif)
   |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
       ![]. ].](_drbrack.gif)
  |
26 | | sbcel1v 3025 |
. . . . . . . . . . . . . . . . 17
       ![]. ].](_drbrack.gif)
      |
27 | 25, 26 | anbi12i 460 |
. . . . . . . . . . . . . . . 16
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
         |
28 | 20, 27 | bitri 184 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif) 
         |
29 | | sbceq2g 3079 |
. . . . . . . . . . . . . . . 16
            ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)    |
30 | 23, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)   |
31 | 28, 30 | anbi12i 460 |
. . . . . . . . . . . . . 14
        ![]. ].](_drbrack.gif) 

      ![]. ].](_drbrack.gif)
              ![]_ ]_](_urbrack.gif)    |
32 | 19, 31 | bitri 184 |
. . . . . . . . . . . . 13
       ![]. ].](_drbrack.gif)  


      
      ![]_ ]_](_urbrack.gif)    |
33 | 32 | sbcbii 3022 |
. . . . . . . . . . . 12
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    
      ![]. ].](_drbrack.gif)       
      ![]_ ]_](_urbrack.gif)    |
34 | | sbcan 3005 |
. . . . . . . . . . . 12
       ![]. ].](_drbrack.gif)              ![]_ ]_](_urbrack.gif)         ![]. ].](_drbrack.gif)      
      ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)    |
35 | | sbcan 3005 |
. . . . . . . . . . . . . 14
       ![]. ].](_drbrack.gif)      
       ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)        |
36 | | sbcel1v 3025 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif)
      |
37 | | 1stexg 6167 |
. . . . . . . . . . . . . . . . 17
       |
38 | 21, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     |
39 | | sbcg 3032 |
. . . . . . . . . . . . . . . 16
            ![]. ].](_drbrack.gif)    
       |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif)           |
41 | 36, 40 | anbi12i 460 |
. . . . . . . . . . . . . 14
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)     
            |
42 | 35, 41 | bitri 184 |
. . . . . . . . . . . . 13
       ![]. ].](_drbrack.gif)      
            |
43 | | sbceq2g 3079 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
44 | 38, 43 | ax-mp 5 |
. . . . . . . . . . . . 13
       ![]. ].](_drbrack.gif)       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
45 | 42, 44 | anbi12i 460 |
. . . . . . . . . . . 12
        ![]. ].](_drbrack.gif) 
           ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif) 
          
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
46 | 33, 34, 45 | 3bitri 206 |
. . . . . . . . . . 11
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    
          
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
47 | | sbcan 3005 |
. . . . . . . . . . . . . 14
       ![]. ].](_drbrack.gif)  
 
       ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)      |
48 | | sbcg 3032 |
. . . . . . . . . . . . . . . 16
            ![]. ].](_drbrack.gif)
   |
49 | 23, 48 | ax-mp 5 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif)
  |
50 | | sbcan 3005 |
. . . . . . . . . . . . . . . 16
       ![]. ].](_drbrack.gif) 
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
   |
51 | | sbcg 3032 |
. . . . . . . . . . . . . . . . . 18
            ![]. ].](_drbrack.gif)
   |
52 | 23, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
       ![]. ].](_drbrack.gif)
  |
53 | | sbceq1g 3077 |
. . . . . . . . . . . . . . . . . . 19
            ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)
   |
54 | 23, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
       ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)
  |
55 | | csbvarg 3085 |
. . . . . . . . . . . . . . . . . . . 20
           ![]_ ]_](_urbrack.gif)       |
56 | 23, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
      ![]_ ]_](_urbrack.gif)      |
57 | 56 | eqeq1i 2185 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)
      |
58 | 54, 57 | bitri 184 |
. . . . . . . . . . . . . . . . 17
       ![]. ].](_drbrack.gif)
      |
59 | 52, 58 | anbi12i 460 |
. . . . . . . . . . . . . . . 16
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)
         |
60 | 50, 59 | bitri 184 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif) 
         |
61 | 49, 60 | anbi12i 460 |
. . . . . . . . . . . . . 14
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif) 
 

         |
62 | 47, 61 | bitri 184 |
. . . . . . . . . . . . 13
       ![]. ].](_drbrack.gif)  
 

         |
63 | 62 | sbcbii 3022 |
. . . . . . . . . . . 12
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    
      ![]. ].](_drbrack.gif)           |
64 | | sbcan 3005 |
. . . . . . . . . . . 12
       ![]. ].](_drbrack.gif)  
             ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
        |
65 | | sbcg 3032 |
. . . . . . . . . . . . . 14
            ![]. ].](_drbrack.gif)
   |
66 | 38, 65 | ax-mp 5 |
. . . . . . . . . . . . 13
       ![]. ].](_drbrack.gif)
  |
67 | | sbcan 3005 |
. . . . . . . . . . . . . 14
       ![]. ].](_drbrack.gif)      
       ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)        |
68 | | sbceq1g 3077 |
. . . . . . . . . . . . . . . . 17
            ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)
   |
69 | 38, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
       ![]. ].](_drbrack.gif)
      ![]_ ]_](_urbrack.gif)
  |
70 | | csbvarg 3085 |
. . . . . . . . . . . . . . . . . 18
           ![]_ ]_](_urbrack.gif)       |
71 | 38, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
      ![]_ ]_](_urbrack.gif)      |
72 | 71 | eqeq1i 2185 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)
      |
73 | 69, 72 | bitri 184 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif)
      |
74 | | sbcg 3032 |
. . . . . . . . . . . . . . . 16
            ![]. ].](_drbrack.gif)    
       |
75 | 38, 74 | ax-mp 5 |
. . . . . . . . . . . . . . 15
       ![]. ].](_drbrack.gif)           |
76 | 73, 75 | anbi12i 460 |
. . . . . . . . . . . . . 14
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)     
            |
77 | 67, 76 | bitri 184 |
. . . . . . . . . . . . 13
       ![]. ].](_drbrack.gif)      
            |
78 | 66, 77 | anbi12i 460 |
. . . . . . . . . . . 12
        ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif) 
                    |
79 | 63, 64, 78 | 3bitri 206 |
. . . . . . . . . . 11
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    

             |
80 | 18, 46, 79 | 3bitr3g 222 |
. . . . . . . . . 10
                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 

              |
81 | 80 | anbi2d 464 |
. . . . . . . . 9
                      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
                   |
82 | 15, 81 | bitrid 192 |
. . . . . . . 8
     
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
                   |
83 | | xpss 4734 |
. . . . . . . . . . . 12
  
  |
84 | | simprr 531 |
. . . . . . . . . . . . 13
 

          |
85 | 8 | adantrr 479 |
. . . . . . . . . . . . 13
 

       
    |
86 | 84, 85 | eqeltrd 2254 |
. . . . . . . . . . . 12
 

         |
87 | 83, 86 | sselid 3153 |
. . . . . . . . . . 11
 

         |
88 | 87 | ex 115 |
. . . . . . . . . 10
            |
89 | 88 | pm4.71rd 394 |
. . . . . . . . 9
          
        |
90 | | eqop 6177 |
. . . . . . . . . . 11
  
                 |
91 | 90 | anbi2d 464 |
. . . . . . . . . 10
  
 
   

              |
92 | 91 | pm5.32i 454 |
. . . . . . . . 9
    
    
                  |
93 | 89, 92 | bitr2di 197 |
. . . . . . . 8
                  
       |
94 | 82, 93 | bitrd 188 |
. . . . . . 7
     
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 

       |
95 | 14, 94 | bitrid 192 |
. . . . . 6
    
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 

       |
96 | 95 | opabbidv 4069 |
. . . . 5
    
  
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      

       |
97 | | df-mpo 5879 |
. . . . . . . 8
         
 

   |
98 | 3, 97 | eqtri 2198 |
. . . . . . 7
     
       |
99 | 98 | cnveqi 4802 |
. . . . . 6
       
       |
100 | | nfv 1528 |
. . . . . . . 8

   |
101 | | nfcsb1v 3090 |
. . . . . . . . 9
        ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
102 | 101 | nfeq2 2331 |
. . . . . . . 8

      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
103 | 100, 102 | nfan 1565 |
. . . . . . 7
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
104 | | nfv 1528 |
. . . . . . . 8
    |
105 | | nfcv 2319 |
. . . . . . . . . 10
       |
106 | | nfcsb1v 3090 |
. . . . . . . . . 10
        ![]_ ]_](_urbrack.gif)  |
107 | 105, 106 | nfcsb 3094 |
. . . . . . . . 9
        ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
108 | 107 | nfeq2 2331 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
109 | 104, 108 | nfan 1565 |
. . . . . . 7
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
110 | | eleq1 2240 |
. . . . . . . . 9
               |
111 | | opelxp 4656 |
. . . . . . . . 9
          |
112 | 110, 111 | bitrdi 196 |
. . . . . . . 8
            |
113 | | csbopeq1a 6188 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
  |
114 | 113 | eqeq2d 2189 |
. . . . . . . 8
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
115 | 112, 114 | anbi12d 473 |
. . . . . . 7
              ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
 

    |
116 | | xpss 4734 |
. . . . . . . . 9
  
  |
117 | 116 | sseli 3151 |
. . . . . . . 8
       |
118 | 117 | adantr 276 |
. . . . . . 7
   
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
119 | 103, 109,
115, 118 | cnvoprab 6234 |
. . . . . 6
      
         
  
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
120 | 99, 119 | eqtri 2198 |
. . . . 5
    
  
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
121 | | df-mpt 4066 |
. . . . 5
                |
122 | 96, 120, 121 | 3eqtr4g 2235 |
. . . 4
 
       |
123 | 122 | fneq1d 5306 |
. . 3
           |
124 | 12, 123 | mpbird 167 |
. 2
 
  |
125 | | dff1o4 5469 |
. 2
        

    |
126 | 5, 124, 125 | sylanbrc 417 |
1
         |