Step | Hyp | Ref
| Expression |
1 | | pm5.19 349 |
. . . . 5

  |
2 | 1 | a1i 10 |
. . . 4
 
   |
3 | 2 | nrex 2716 |
. . 3


  |
4 | 3 | nex 1555 |
. 2
   
  |
5 | | bren 6030 |
. . 3
 1     1      |
6 | | f1odm 5290 |
. . . . . . . . 9
   1    1   |
7 | | vex 2862 |
. . . . . . . . . 10
 |
8 | 7 | dmex 5106 |
. . . . . . . . 9
 |
9 | 6, 8 | syl6eqelr 2442 |
. . . . . . . 8
   1    1   |
10 | | pw1exb 4326 |
. . . . . . . 8
 1   |
11 | 9, 10 | sylib 188 |
. . . . . . 7
   1      |
12 | | nenpw1pwlem2.1 |
. . . . . . . 8

        |
13 | 12 | nenpw1pwlem1 6084 |
. . . . . . 7
   |
14 | 11, 13 | syl 15 |
. . . . . 6
   1      |
15 | | ssrab2 3351 |
. . . . . . . 8
         |
16 | 12, 15 | eqsstri 3301 |
. . . . . . 7
 |
17 | | elpwg 3729 |
. . . . . . 7
 
    |
18 | 16, 17 | mpbiri 224 |
. . . . . 6
    |
19 | 14, 18 | syl 15 |
. . . . 5
   1       |
20 | | f1ofo 5293 |
. . . . . . . 8
   1      1      |
21 | | forn 5272 |
. . . . . . . 8
   1       |
22 | 20, 21 | syl 15 |
. . . . . . 7
   1       |
23 | 22 | eleq2d 2420 |
. . . . . 6
   1    
    |
24 | | elrn 4896 |
. . . . . . 7
      |
25 | | breldm 4911 |
. . . . . . . . . . . 12
     |
26 | 25 | adantl 452 |
. . . . . . . . . . 11
    1         |
27 | 6 | adantr 451 |
. . . . . . . . . . 11
    1       1   |
28 | 26, 27 | eleqtrd 2429 |
. . . . . . . . . 10
    1       1   |
29 | | elpw1 4144 |
. . . . . . . . . . 11
 1      |
30 | | breq1 4642 |
. . . . . . . . . . . . . . . 16
             |
31 | 30 | 3anbi2d 1257 |
. . . . . . . . . . . . . . 15
       1          1       
    |
32 | | id 19 |
. . . . . . . . . . . . . . . . . . 19
   |
33 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . 20
       |
34 | 33 | fveq2d 5332 |
. . . . . . . . . . . . . . . . . . 19
      
        |
35 | 32, 34 | eleq12d 2421 |
. . . . . . . . . . . . . . . . . 18
 
     
         |
36 | 35 | notbid 285 |
. . . . . . . . . . . . . . . . 17
 
               |
37 | 36, 12 | elrab2 2996 |
. . . . . . . . . . . . . . . 16
 
         |
38 | | simp3 957 |
. . . . . . . . . . . . . . . . . 18
    1           |
39 | 38 | biantrurd 494 |
. . . . . . . . . . . . . . . . 17
    1                
          |
40 | | simp2 956 |
. . . . . . . . . . . . . . . . . . . 20
    1               |
41 | | f1ofn 5288 |
. . . . . . . . . . . . . . . . . . . . . 22
   1    1   |
42 | 41 | 3ad2ant1 976 |
. . . . . . . . . . . . . . . . . . . . 21
    1         1   |
43 | | snelpw1 4146 |
. . . . . . . . . . . . . . . . . . . . . . 23
   1   |
44 | 43 | biimpri 197 |
. . . . . . . . . . . . . . . . . . . . . 22
   1   |
45 | 44 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . . 21
    1           1   |
46 | | fnbrfvb 5358 |
. . . . . . . . . . . . . . . . . . . . 21
  1   1        
       |
47 | 42, 45, 46 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . 20
    1               
       |
48 | 40, 47 | mpbird 223 |
. . . . . . . . . . . . . . . . . . 19
    1                 |
49 | 48 | eleq2d 2420 |
. . . . . . . . . . . . . . . . . 18
    1                   |
50 | 49 | notbid 285 |
. . . . . . . . . . . . . . . . 17
    1                   |
51 | 39, 50 | bitr3d 246 |
. . . . . . . . . . . . . . . 16
    1          
          |
52 | 37, 51 | syl5bb 248 |
. . . . . . . . . . . . . . 15
    1             |
53 | 31, 52 | syl6bi 219 |
. . . . . . . . . . . . . 14
       1       
    |
54 | 53 | com12 27 |
. . . . . . . . . . . . 13
    1     
         |
55 | 54 | 3expa 1151 |
. . . . . . . . . . . 12
     1        
       |
56 | 55 | reximdva 2726 |
. . . . . . . . . . 11
    1                 |
57 | 29, 56 | syl5bi 208 |
. . . . . . . . . 10
    1        1  
    |
58 | 28, 57 | mpd 14 |
. . . . . . . . 9
    1        
   |
59 | 58 | ex 423 |
. . . . . . . 8
   1             |
60 | 59 | exlimdv 1636 |
. . . . . . 7
   1              |
61 | 24, 60 | syl5bi 208 |
. . . . . 6
   1    
      |
62 | 23, 61 | sylbird 226 |
. . . . 5
   1    
       |
63 | 19, 62 | mpd 14 |
. . . 4
   1         |
64 | 63 | eximi 1576 |
. . 3
    1           |
65 | 5, 64 | sylbi 187 |
. 2
 1     
   |
66 | 4, 65 | mto 167 |
1
1   |