Step | Hyp | Ref
| Expression |
1 | | bren 6741 |
. . 3

       |
2 | | f1odm 5461 |
. . . . . . 7
    
  |
3 | | vex 2740 |
. . . . . . . 8
 |
4 | 3 | dmex 4889 |
. . . . . . 7
 |
5 | 2, 4 | eqeltrrdi 2269 |
. . . . . 6
    
  |
6 | | pwexg 4177 |
. . . . . 6
 
  |
7 | | inex1g 4136 |
. . . . . 6
         |
8 | 5, 6, 7 | 3syl 17 |
. . . . 5
    
       |
9 | | f1ofo 5464 |
. . . . . . . 8
    
      |
10 | | forn 5437 |
. . . . . . . 8
    
  |
11 | 9, 10 | syl 14 |
. . . . . . 7
    
  |
12 | 3 | rnex 4890 |
. . . . . . 7
 |
13 | 11, 12 | eqeltrrdi 2269 |
. . . . . 6
    
  |
14 | | pwexg 4177 |
. . . . . 6
 
  |
15 | | inex1g 4136 |
. . . . . 6
         |
16 | 13, 14, 15 | 3syl 17 |
. . . . 5
    
       |
17 | | f1of1 5456 |
. . . . . . . . . . 11
    
      |
18 | 17 | adantr 276 |
. . . . . . . . . 10
             |
19 | 13 | adantr 276 |
. . . . . . . . . 10
      
  |
20 | | simpr 110 |
. . . . . . . . . 10
      
  |
21 | | vex 2740 |
. . . . . . . . . . 11
 |
22 | 21 | a1i 9 |
. . . . . . . . . 10
         |
23 | | f1imaen2g 6787 |
. . . . . . . . . 10
                 |
24 | 18, 19, 20, 22, 23 | syl22anc 1239 |
. . . . . . . . 9
          
  |
25 | | entr 6778 |
. . . . . . . . 9
     
    
  |
26 | 24, 25 | sylan 283 |
. . . . . . . 8
      
 
      |
27 | 26 | expl 378 |
. . . . . . 7
    
 
    
   |
28 | | imassrn 4977 |
. . . . . . . . 9
     |
29 | 28, 10 | sseqtrid 3205 |
. . . . . . . 8
        
  |
30 | 9, 29 | syl 14 |
. . . . . . 7
    
      |
31 | 27, 30 | jctild 316 |
. . . . . 6
    
 
         
    |
32 | | elin 3318 |
. . . . . . 7
             |
33 | 21 | elpw 3580 |
. . . . . . . 8
 
  |
34 | | breq1 4003 |
. . . . . . . . 9
 
   |
35 | 21, 34 | elab 2881 |
. . . . . . . 8
     |
36 | 33, 35 | anbi12i 460 |
. . . . . . 7
  

      |
37 | 32, 36 | bitri 184 |
. . . . . 6
      
   |
38 | | elin 3318 |
. . . . . . 7
                         |
39 | 3 | imaex 4979 |
. . . . . . . . 9
     |
40 | 39 | elpw 3580 |
. . . . . . . 8
     
      |
41 | | breq1 4003 |
. . . . . . . . 9
     
       |
42 | 39, 41 | elab 2881 |
. . . . . . . 8
             |
43 | 40, 42 | anbi12i 460 |
. . . . . . 7
           
              |
44 | 38, 43 | bitri 184 |
. . . . . 6
                  
   |
45 | 31, 37, 44 | 3imtr4g 205 |
. . . . 5
    
                  |
46 | | f1ocnv 5470 |
. . . . . . 7
    
       |
47 | | f1of1 5456 |
. . . . . . . . . . . 12
             |
48 | | f1f1orn 5468 |
. . . . . . . . . . . 12
              |
49 | | f1of1 5456 |
. . . . . . . . . . . 12
               |
50 | 47, 48, 49 | 3syl 17 |
. . . . . . . . . . 11
              |
51 | | vex 2740 |
. . . . . . . . . . . 12
 |
52 | 51 | f1imaen 6788 |
. . . . . . . . . . 11
       
     
  |
53 | 50, 52 | sylan 283 |
. . . . . . . . . 10
      
        |
54 | | entr 6778 |
. . . . . . . . . 10
      
        |
55 | 53, 54 | sylan 283 |
. . . . . . . . 9
              
  |
56 | 55 | expl 378 |
. . . . . . . 8
        
        |
57 | | f1ofo 5464 |
. . . . . . . . 9
             |
58 | | imassrn 4977 |
. . . . . . . . . 10
    
  |
59 | | forn 5437 |
. . . . . . . . . 10
         |
60 | 58, 59 | sseqtrid 3205 |
. . . . . . . . 9
             |
61 | 57, 60 | syl 14 |
. . . . . . . 8
             |
62 | 56, 61 | jctild 316 |
. . . . . . 7
        
     
    
    |
63 | 46, 62 | syl 14 |
. . . . . 6
    
 
                |
64 | | elin 3318 |
. . . . . . 7
             |
65 | 51 | elpw 3580 |
. . . . . . . 8
 
  |
66 | | breq1 4003 |
. . . . . . . . 9
 
   |
67 | 51, 66 | elab 2881 |
. . . . . . . 8
     |
68 | 65, 67 | anbi12i 460 |
. . . . . . 7
  

      |
69 | 64, 68 | bitri 184 |
. . . . . 6
      
   |
70 | | elin 3318 |
. . . . . . 7
        
              
    |
71 | 3 | cnvex 5163 |
. . . . . . . . . 10
  |
72 | 71 | imaex 4979 |
. . . . . . . . 9
      |
73 | 72 | elpw 3580 |
. . . . . . . 8
           
  |
74 | | breq1 4003 |
. . . . . . . . 9
           
   |
75 | 72, 74 | elab 2881 |
. . . . . . . 8
      
     
  |
76 | 73, 75 | anbi12i 460 |
. . . . . . 7
                              |
77 | 70, 76 | bitri 184 |
. . . . . 6
        
            
   |
78 | 63, 69, 77 | 3imtr4g 205 |
. . . . 5
    
             
     |
79 | | simpl 109 |
. . . . . . . . . . 11
  

 
   |
80 | 79 | elpwid 3585 |
. . . . . . . . . 10
  

 
  |
81 | 64, 80 | sylbi 121 |
. . . . . . . . 9
        |
82 | | imaeq2 4962 |
. . . . . . . . . . . 12
                     |
83 | | f1orel 5460 |
. . . . . . . . . . . . . . . 16
    
  |
84 | | dfrel2 5075 |
. . . . . . . . . . . . . . . 16
  
  |
85 | 83, 84 | sylib 122 |
. . . . . . . . . . . . . . 15
    
 
  |
86 | 85 | imaeq1d 4965 |
. . . . . . . . . . . . . 14
    
                      |
87 | 86 | adantr 276 |
. . . . . . . . . . . . 13
                             |
88 | 46, 47 | syl 14 |
. . . . . . . . . . . . . 14
    
       |
89 | | f1imacnv 5474 |
. . . . . . . . . . . . . 14
       
             |
90 | 88, 89 | sylan 283 |
. . . . . . . . . . . . 13
                    |
91 | 87, 90 | eqtr3d 2212 |
. . . . . . . . . . . 12
                  |
92 | 82, 91 | sylan9eqr 2232 |
. . . . . . . . . . 11
      
             |
93 | 92 | eqcomd 2183 |
. . . . . . . . . 10
      
             |
94 | 93 | ex 115 |
. . . . . . . . 9
            
       |
95 | 81, 94 | sylan2 286 |
. . . . . . . 8
     
                   |
96 | 95 | adantrl 478 |
. . . . . . 7
                                |
97 | | simpl 109 |
. . . . . . . . . . 11
  

 
   |
98 | 97 | elpwid 3585 |
. . . . . . . . . 10
  

 
  |
99 | 32, 98 | sylbi 121 |
. . . . . . . . 9
        |
100 | | imaeq2 4962 |
. . . . . . . . . . . 12
                     |
101 | | f1imacnv 5474 |
. . . . . . . . . . . . 13
     
            |
102 | 17, 101 | sylan 283 |
. . . . . . . . . . . 12
                  |
103 | 100, 102 | sylan9eqr 2232 |
. . . . . . . . . . 11
      
     
       |
104 | 103 | eqcomd 2183 |
. . . . . . . . . 10
      
     
       |
105 | 104 | ex 115 |
. . . . . . . . 9
                    |
106 | 99, 105 | sylan2 286 |
. . . . . . . 8
     
                   |
107 | 106 | adantrr 479 |
. . . . . . 7
                       
        |
108 | 96, 107 | impbid 129 |
. . . . . 6
                        
       |
109 | 108 | ex 115 |
. . . . 5
    
    
 
                    |
110 | 8, 16, 45, 78, 109 | en3d 6763 |
. . . 4
    
    
       |
111 | 110 | exlimiv 1598 |
. . 3
            

    |
112 | 1, 111 | sylbi 121 |
. 2
  

 
       |
113 | | df-pw 3576 |
. . . 4
    |
114 | 113 | ineq1i 3332 |
. . 3
  
    

   |
115 | | inab 3403 |
. . 3
  

       |
116 | 114, 115 | eqtri 2198 |
. 2
  
       |
117 | | df-pw 3576 |
. . . 4
    |
118 | 117 | ineq1i 3332 |
. . 3
  
    

   |
119 | | inab 3403 |
. . 3
  

       |
120 | 118, 119 | eqtri 2198 |
. 2
  
       |
121 | 112, 116,
120 | 3brtr3g 4033 |
1
           |