Step | Hyp | Ref
| Expression |
1 | | brex 4690 |
. 2
     |
2 | | brex 4690 |
. . 3
 1 1  1 1    |
3 | | pw1exb 4327 |
. . . 4
 1   |
4 | | pw1exb 4327 |
. . . 4
 1   |
5 | 3, 4 | anbi12i 678 |
. . 3
  1 1
 
   |
6 | 2, 5 | sylib 188 |
. 2
 1 1     |
7 | | breq1 4643 |
. . . 4
     |
8 | | pw1eq 4144 |
. . . . 5
 1 1   |
9 | 8 | breq1d 4650 |
. . . 4
  1 1 1 1    |
10 | 7, 9 | bibi12d 312 |
. . 3
  
1 1  
1 1     |
11 | | breq2 4644 |
. . . 4
     |
12 | | pw1eq 4144 |
. . . . 5
 1 1   |
13 | 12 | breq2d 4652 |
. . . 4
  1 1
1 1    |
14 | 11, 13 | bibi12d 312 |
. . 3
  
1 1   1 1     |
15 | | bren 6031 |
. . . . 5

       |
16 | | f1ofun 5290 |
. . . . . . . . . 10
       |
17 | | funsi 5521 |
. . . . . . . . . 10

SI   |
18 | 16, 17 | syl 15 |
. . . . . . . . 9
     SI   |
19 | | f1odm 5291 |
. . . . . . . . . 10
    
  |
20 | | dmsi 5520 |
. . . . . . . . . . 11
SI 1  |
21 | | pw1eq 4144 |
. . . . . . . . . . 11
 1
1   |
22 | 20, 21 | syl5eq 2397 |
. . . . . . . . . 10
 SI 1   |
23 | 19, 22 | syl 15 |
. . . . . . . . 9
     SI 1   |
24 | | df-fn 4791 |
. . . . . . . . 9
SI
1  SI
SI 1    |
25 | 18, 23, 24 | sylanbrc 645 |
. . . . . . . 8
     SI 1   |
26 | | f1of1 5287 |
. . . . . . . . . . 11
           |
27 | | df-f1 4793 |
. . . . . . . . . . . 12
              |
28 | 27 | simprbi 450 |
. . . . . . . . . . 11
        |
29 | | funsi 5521 |
. . . . . . . . . . 11
 
SI    |
30 | 26, 28, 29 | 3syl 18 |
. . . . . . . . . 10
     SI    |
31 | | cnvsi 5519 |
. . . . . . . . . . 11
SI SI
  |
32 | 31 | funeqi 5129 |
. . . . . . . . . 10
 SI SI    |
33 | 30, 32 | sylibr 203 |
. . . . . . . . 9
     SI   |
34 | | f1ofo 5294 |
. . . . . . . . . 10
           |
35 | | forn 5273 |
. . . . . . . . . 10
    
  |
36 | | rnsi 5522 |
. . . . . . . . . . . 12
SI 1  |
37 | | dfrn4 4905 |
. . . . . . . . . . . 12
SI SI  |
38 | 36, 37 | eqtr3i 2375 |
. . . . . . . . . . 11
1 SI  |
39 | | pw1eq 4144 |
. . . . . . . . . . 11
 1
1   |
40 | 38, 39 | syl5eqr 2399 |
. . . . . . . . . 10
 SI
1   |
41 | 34, 35, 40 | 3syl 18 |
. . . . . . . . 9
     SI
1   |
42 | | df-fn 4791 |
. . . . . . . . 9
 SI 1  SI SI
1    |
43 | 33, 41, 42 | sylanbrc 645 |
. . . . . . . 8
     SI 1   |
44 | | dff1o4 5295 |
. . . . . . . 8
SI
  1   1 SI 1 SI 1    |
45 | 25, 43, 44 | sylanbrc 645 |
. . . . . . 7
     SI   1   1   |
46 | | vex 2863 |
. . . . . . . . 9
 |
47 | 46 | siex 4754 |
. . . . . . . 8
SI  |
48 | 47 | f1oen 6034 |
. . . . . . 7
SI
  1   1 1 1   |
49 | 45, 48 | syl 15 |
. . . . . 6
     1 1   |
50 | 49 | exlimiv 1634 |
. . . . 5
      1
1   |
51 | 15, 50 | sylbi 187 |
. . . 4

1 1   |
52 | | bren 6031 |
. . . . 5
 1 1
   1   1   |
53 | | f1ofun 5290 |
. . . . . . . . . . . . . 14
   1   1
  |
54 | | fununiq 5518 |
. . . . . . . . . . . . . . . 16
 
                   |
55 | | vex 2863 |
. . . . . . . . . . . . . . . . 17
 |
56 | 55 | sneqb 3877 |
. . . . . . . . . . . . . . . 16
       |
57 | 54, 56 | sylib 188 |
. . . . . . . . . . . . . . 15
 
            
  |
58 | 57 | 3expib 1154 |
. . . . . . . . . . . . . 14
               
   |
59 | 53, 58 | syl 15 |
. . . . . . . . . . . . 13
   1   1
              
   |
60 | 59 | alrimivv 1632 |
. . . . . . . . . . . 12
   1   1
                      |
61 | | sneq 3745 |
. . . . . . . . . . . . . 14
       |
62 | 61 | breq2d 4652 |
. . . . . . . . . . . . 13
                 |
63 | 62 | mo4 2237 |
. . . . . . . . . . . 12
                               |
64 | 60, 63 | sylibr 203 |
. . . . . . . . . . 11
   1   1
          |
65 | 64 | alrimiv 1631 |
. . . . . . . . . 10
   1   1
            |
66 | | funopab 5140 |
. . . . . . . . . 10
                        |
67 | 65, 66 | sylibr 203 |
. . . . . . . . 9
   1   1
             |
68 | | dmopab 4916 |
. . . . . . . . . 10
           
          |
69 | | eldm 4899 |
. . . . . . . . . . . . . . 15
           |
70 | | brelrn 4961 |
. . . . . . . . . . . . . . . . 17
    
  |
71 | | f1ofo 5294 |
. . . . . . . . . . . . . . . . . . . . 21
   1   1
  1   1   |
72 | | forn 5273 |
. . . . . . . . . . . . . . . . . . . . 21
   1   1
1   |
73 | 71, 72 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
   1   1
1   |
74 | 73 | eleq2d 2420 |
. . . . . . . . . . . . . . . . . . 19
   1   1

1    |
75 | | elpw1 4145 |
. . . . . . . . . . . . . . . . . . . 20
 1

    |
76 | | breq2 4644 |
. . . . . . . . . . . . . . . . . . . . . 22
       
         |
77 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
78 | | sneq 3745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
79 | 78 | breq2d 4652 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
80 | 77, 79 | spcev 2947 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
81 | 76, 80 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . . . 21
       
           |
82 | 81 | rexlimivw 2735 |
. . . . . . . . . . . . . . . . . . . 20
 
                  |
83 | 75, 82 | sylbi 187 |
. . . . . . . . . . . . . . . . . . 19
 1
                |
84 | 74, 83 | syl6bi 219 |
. . . . . . . . . . . . . . . . . 18
   1   1

    
            |
85 | 84 | com23 72 |
. . . . . . . . . . . . . . . . 17
   1   1
                  |
86 | 70, 85 | mpdi 38 |
. . . . . . . . . . . . . . . 16
   1   1
                |
87 | 86 | exlimdv 1636 |
. . . . . . . . . . . . . . 15
   1   1
      
           |
88 | 69, 87 | syl5bi 208 |
. . . . . . . . . . . . . 14
   1   1
              |
89 | | breldm 4912 |
. . . . . . . . . . . . . . 15
           |
90 | 89 | exlimiv 1634 |
. . . . . . . . . . . . . 14
             |
91 | 88, 90 | impbid1 194 |
. . . . . . . . . . . . 13
   1   1
              |
92 | | f1odm 5291 |
. . . . . . . . . . . . . 14
   1   1
1   |
93 | 92 | eleq2d 2420 |
. . . . . . . . . . . . 13
   1   1
     1    |
94 | 91, 93 | bitr3d 246 |
. . . . . . . . . . . 12
   1   1
          
1    |
95 | | snelpw1 4147 |
. . . . . . . . . . . 12
   1   |
96 | 94, 95 | syl6bb 252 |
. . . . . . . . . . 11
   1   1
            |
97 | 96 | eqabcdv 2470 |
. . . . . . . . . 10
   1   1
         
  |
98 | 68, 97 | syl5eq 2397 |
. . . . . . . . 9
   1   1
             |
99 | | df-fn 4791 |
. . . . . . . . 9
                                      |
100 | 67, 98, 99 | sylanbrc 645 |
. . . . . . . 8
   1   1
  
          |
101 | | f1ocnv 5300 |
. . . . . . . . . . . . . . 15
   1   1
   1   1   |
102 | | f1ofun 5290 |
. . . . . . . . . . . . . . 15
    1   1    |
103 | | fununiq 5518 |
. . . . . . . . . . . . . . . . 17
                 
 
    |
104 | 103 | 3expib 1154 |
. . . . . . . . . . . . . . . 16
 
                        |
105 | | brcnv 4893 |
. . . . . . . . . . . . . . . . 17
                |
106 | | brcnv 4893 |
. . . . . . . . . . . . . . . . 17
                |
107 | 105, 106 | anbi12i 678 |
. . . . . . . . . . . . . . . 16
                                 |
108 | | vex 2863 |
. . . . . . . . . . . . . . . . 17
 |
109 | 108 | sneqb 3877 |
. . . . . . . . . . . . . . . 16
       |
110 | 104, 107,
109 | 3imtr3g 260 |
. . . . . . . . . . . . . . 15
 
              
   |
111 | 101, 102,
110 | 3syl 18 |
. . . . . . . . . . . . . 14
   1   1
              
   |
112 | 111 | alrimivv 1632 |
. . . . . . . . . . . . 13
   1   1
                      |
113 | | sneq 3745 |
. . . . . . . . . . . . . . 15
       |
114 | 113 | breq1d 4650 |
. . . . . . . . . . . . . 14
                 |
115 | 114 | mo4 2237 |
. . . . . . . . . . . . 13
                               |
116 | 112, 115 | sylibr 203 |
. . . . . . . . . . . 12
   1   1
          |
117 | 116 | alrimiv 1631 |
. . . . . . . . . . 11
   1   1
            |
118 | | funopab 5140 |
. . . . . . . . . . 11
                        |
119 | 117, 118 | sylibr 203 |
. . . . . . . . . 10
   1   1
             |
120 | | dmopab 4916 |
. . . . . . . . . . 11
           
          |
121 | | elrn 4897 |
. . . . . . . . . . . . . . . 16
   
      |
122 | | breldm 4912 |
. . . . . . . . . . . . . . . . . 18
       |
123 | 92 | eleq2d 2420 |
. . . . . . . . . . . . . . . . . . . 20
   1   1

1    |
124 | | elpw1 4145 |
. . . . . . . . . . . . . . . . . . . . 21
 1

    |
125 | | breq1 4643 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
126 | | sneq 3745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
127 | 126 | breq1d 4650 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
128 | 77, 127 | spcev 2947 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
129 | 125, 128 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
130 | 129 | rexlimivw 2735 |
. . . . . . . . . . . . . . . . . . . . 21
 
                  |
131 | 124, 130 | sylbi 187 |
. . . . . . . . . . . . . . . . . . . 20
 1
                |
132 | 123, 131 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . 19
   1   1

                 |
133 | 132 | com23 72 |
. . . . . . . . . . . . . . . . . 18
   1   1
                  |
134 | 122, 133 | mpdi 38 |
. . . . . . . . . . . . . . . . 17
   1   1
                |
135 | 134 | exlimdv 1636 |
. . . . . . . . . . . . . . . 16
   1   1
 
               |
136 | 121, 135 | syl5bi 208 |
. . . . . . . . . . . . . . 15
   1   1
              |
137 | | brelrn 4961 |
. . . . . . . . . . . . . . . 16
           |
138 | 137 | exlimiv 1634 |
. . . . . . . . . . . . . . 15
             |
139 | 136, 138 | impbid1 194 |
. . . . . . . . . . . . . 14
   1   1
              |
140 | 73 | eleq2d 2420 |
. . . . . . . . . . . . . 14
   1   1
     1    |
141 | 139, 140 | bitr3d 246 |
. . . . . . . . . . . . 13
   1   1
          
1    |
142 | | snelpw1 4147 |
. . . . . . . . . . . . 13
   1   |
143 | 141, 142 | syl6bb 252 |
. . . . . . . . . . . 12
   1   1
            |
144 | 143 | eqabcdv 2470 |
. . . . . . . . . . 11
   1   1
         
  |
145 | 120, 144 | syl5eq 2397 |
. . . . . . . . . 10
   1   1
             |
146 | | df-fn 4791 |
. . . . . . . . . 10
                                      |
147 | 119, 145,
146 | sylanbrc 645 |
. . . . . . . . 9
   1   1
  
          |
148 | | cnvopab 5031 |
. . . . . . . . . 10
                        |
149 | 148 | fneq1i 5179 |
. . . . . . . . 9
            
             |
150 | 147, 149 | sylibr 203 |
. . . . . . . 8
   1   1
              |
151 | | dff1o4 5295 |
. . . . . . . 8
                   
                       |
152 | 100, 150,
151 | sylanbrc 645 |
. . . . . . 7
   1   1
  
              |
153 | | enpw1lem1 6062 |
. . . . . . . 8
  
         |
154 | 153 | f1oen 6034 |
. . . . . . 7
                  |
155 | 152, 154 | syl 15 |
. . . . . 6
   1   1
  |
156 | 155 | exlimiv 1634 |
. . . . 5
    1   1   |
157 | 52, 156 | sylbi 187 |
. . . 4
 1 1
  |
158 | 51, 157 | impbii 180 |
. . 3

1 1   |
159 | 10, 14, 158 | vtocl2g 2919 |
. 2
 
  1 1    |
160 | 1, 6, 159 | pm5.21nii 342 |
1
 1 1   |