Step | Hyp | Ref
| Expression |
1 | | bren 6746 |
. 2

       |
2 | | bren 6746 |
. 2

       |
3 | | eeanv 1932 |
. . 3
              
              |
4 | | f1odm 5465 |
. . . . . . . 8
    
  |
5 | | vex 2740 |
. . . . . . . . 9
 |
6 | 5 | dmex 4893 |
. . . . . . . 8
 |
7 | 4, 6 | eqeltrrdi 2269 |
. . . . . . 7
    
  |
8 | | f1odm 5465 |
. . . . . . . 8
    
  |
9 | | vex 2740 |
. . . . . . . . 9
 |
10 | 9 | dmex 4893 |
. . . . . . . 8
 |
11 | 8, 10 | eqeltrrdi 2269 |
. . . . . . 7
    
  |
12 | | fnmap 6654 |
. . . . . . . 8

  |
13 | | fnovex 5907 |
. . . . . . . 8
        |
14 | 12, 13 | mp3an1 1324 |
. . . . . . 7
 
     |
15 | 7, 11, 14 | syl2anr 290 |
. . . . . 6
               |
16 | | f1of 5461 |
. . . . . . . 8
    
      |
17 | | elmapg 6660 |
. . . . . . . . 9
 
           |
18 | 7, 11, 17 | syl2anr 290 |
. . . . . . . 8
             
       |
19 | 16, 18 | imbitrrid 156 |
. . . . . . 7
                     |
20 | 19 | abssdv 3229 |
. . . . . 6
                     |
21 | 15, 20 | ssexd 4143 |
. . . . 5
                
  |
22 | | f1ofo 5468 |
. . . . . . . . 9
    
      |
23 | | forn 5441 |
. . . . . . . . 9
       |
24 | 22, 23 | syl 14 |
. . . . . . . 8
    
  |
25 | 5 | rnex 4894 |
. . . . . . . 8
 |
26 | 24, 25 | eqeltrrdi 2269 |
. . . . . . 7
    
  |
27 | | f1ofo 5468 |
. . . . . . . . 9
    
      |
28 | | forn 5441 |
. . . . . . . . 9
    
  |
29 | 27, 28 | syl 14 |
. . . . . . . 8
    
  |
30 | 9 | rnex 4894 |
. . . . . . . 8
 |
31 | 29, 30 | eqeltrrdi 2269 |
. . . . . . 7
    
  |
32 | | fnovex 5907 |
. . . . . . . 8
        |
33 | 12, 32 | mp3an1 1324 |
. . . . . . 7
 
     |
34 | 26, 31, 33 | syl2anr 290 |
. . . . . 6
               |
35 | | f1of 5461 |
. . . . . . . 8
    
      |
36 | | elmapg 6660 |
. . . . . . . . 9
 
           |
37 | 26, 31, 36 | syl2anr 290 |
. . . . . . . 8
             
       |
38 | 35, 37 | imbitrrid 156 |
. . . . . . 7
                     |
39 | 38 | abssdv 3229 |
. . . . . 6
                     |
40 | 34, 39 | ssexd 4143 |
. . . . 5
                
  |
41 | | f1oco 5484 |
. . . . . . . . 9
                   |
42 | 41 | adantll 476 |
. . . . . . . 8
                
        |
43 | | f1ocnv 5474 |
. . . . . . . . 9
    
       |
44 | 43 | ad2antrr 488 |
. . . . . . . 8
                
       |
45 | | f1oco 5484 |
. . . . . . . 8
             
           |
46 | 42, 44, 45 | syl2anc 411 |
. . . . . . 7
                
           |
47 | 46 | ex 115 |
. . . . . 6
                            |
48 | | vex 2740 |
. . . . . . 7
 |
49 | | f1oeq1 5449 |
. . . . . . 7
     
       |
50 | 48, 49 | elab 2881 |
. . . . . 6
             |
51 | 5, 48 | coex 5174 |
. . . . . . . 8
   |
52 | 9 | cnvex 5167 |
. . . . . . . 8
  |
53 | 51, 52 | coex 5174 |
. . . . . . 7
      |
54 | | f1oeq1 5449 |
. . . . . . 7
                       |
55 | 53, 54 | elab 2881 |
. . . . . 6
                       |
56 | 47, 50, 55 | 3imtr4g 205 |
. . . . 5
                                |
57 | | f1ocnv 5474 |
. . . . . . . . 9
    
       |
58 | 57 | ad2antlr 489 |
. . . . . . . 8
                
       |
59 | | f1oco 5484 |
. . . . . . . . . 10
                   |
60 | 59 | ancoms 268 |
. . . . . . . . 9
                   |
61 | 60 | adantlr 477 |
. . . . . . . 8
                
        |
62 | | f1oco 5484 |
. . . . . . . 8
                         |
63 | 58, 61, 62 | syl2anc 411 |
. . . . . . 7
                
 
         |
64 | 63 | ex 115 |
. . . . . 6
                            |
65 | | vex 2740 |
. . . . . . 7
 |
66 | | f1oeq1 5449 |
. . . . . . 7
     
       |
67 | 65, 66 | elab 2881 |
. . . . . 6
             |
68 | 5 | cnvex 5167 |
. . . . . . . 8
  |
69 | 65, 9 | coex 5174 |
. . . . . . . 8
   |
70 | 68, 69 | coex 5174 |
. . . . . . 7
      |
71 | | f1oeq1 5449 |
. . . . . . 7
          
 
          |
72 | 70, 71 | elab 2881 |
. . . . . 6
  
                    |
73 | 64, 67, 72 | 3imtr4g 205 |
. . . . 5
                                |
74 | 50, 67 | anbi12i 460 |
. . . . . 6
              
            |
75 | | coass 5147 |
. . . . . . . . . . 11
               |
76 | | f1ococnv1 5490 |
. . . . . . . . . . . . . 14
    
 

   |
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . 13
                         
   |
78 | 77 | coeq2d 4789 |
. . . . . . . . . . . 12
                           
         |
79 | 42 | adantrr 479 |
. . . . . . . . . . . . 13
                               |
80 | | f1of 5461 |
. . . . . . . . . . . . 13
      
        |
81 | | fcoi1 5396 |
. . . . . . . . . . . . 13
                |
82 | 79, 80, 81 | 3syl 17 |
. . . . . . . . . . . 12
                                |
83 | 78, 82 | eqtrd 2210 |
. . . . . . . . . . 11
                           
      |
84 | 75, 83 | eqtr2id 2223 |
. . . . . . . . . 10
                                  |
85 | | coass 5147 |
. . . . . . . . . . 11
               |
86 | | f1ococnv2 5488 |
. . . . . . . . . . . . . 14
    
  
   |
87 | 86 | ad2antlr 489 |
. . . . . . . . . . . . 13
                         
   |
88 | 87 | coeq1d 4788 |
. . . . . . . . . . . 12
                              
      |
89 | 61 | adantrl 478 |
. . . . . . . . . . . . 13
                               |
90 | | f1of 5461 |
. . . . . . . . . . . . 13
      
        |
91 | | fcoi2 5397 |
. . . . . . . . . . . . 13
                |
92 | 89, 90, 91 | 3syl 17 |
. . . . . . . . . . . 12
                                |
93 | 88, 92 | eqtrd 2210 |
. . . . . . . . . . 11
                                  |
94 | 85, 93 | eqtr3id 2224 |
. . . . . . . . . 10
                         
        |
95 | 84, 94 | eqeq12d 2192 |
. . . . . . . . 9
                                             |
96 | | eqcom 2179 |
. . . . . . . . 9
         
           |
97 | 95, 96 | bitrdi 196 |
. . . . . . . 8
                                             |
98 | | f1of1 5460 |
. . . . . . . . . 10
    
      |
99 | 98 | ad2antlr 489 |
. . . . . . . . 9
                             |
100 | | f1of 5461 |
. . . . . . . . . 10
    
      |
101 | 100 | ad2antrl 490 |
. . . . . . . . 9
                             |
102 | 63 | adantrl 478 |
. . . . . . . . . 10
                                  |
103 | | f1of 5461 |
. . . . . . . . . 10
  
                  |
104 | 102, 103 | syl 14 |
. . . . . . . . 9
                                  |
105 | | cocan1 5787 |
. . . . . . . . 9
           
             
   
 
      |
106 | 99, 101, 104, 105 | syl3anc 1238 |
. . . . . . . 8
                                
 
      |
107 | 27 | ad2antrr 488 |
. . . . . . . . 9
                             |
108 | | f1ofn 5462 |
. . . . . . . . . 10
    
  |
109 | 108 | ad2antll 491 |
. . . . . . . . 9
                         |
110 | 46 | adantrr 479 |
. . . . . . . . . 10
                                  |
111 | | f1ofn 5462 |
. . . . . . . . . 10
                 |
112 | 110, 111 | syl 14 |
. . . . . . . . 9
                              |
113 | | cocan2 5788 |
. . . . . . . . 9
     
     
         
        |
114 | 107, 109,
112, 113 | syl3anc 1238 |
. . . . . . . 8
                                         |
115 | 97, 106, 114 | 3bitr3d 218 |
. . . . . . 7
                         
           |
116 | 115 | ex 115 |
. . . . . 6
                           
         |
117 | 74, 116 | biimtrid 152 |
. . . . 5
                            
            |
118 | 21, 40, 56, 73, 117 | en3d 6768 |
. . . 4
                         |
119 | 118 | exlimivv 1896 |
. . 3
                             |
120 | 3, 119 | sylbir 135 |
. 2
                           |
121 | 1, 2, 120 | syl2anb 291 |
1
                 |