Step | Hyp | Ref
| Expression |
1 | | 0ex 3972 |
. . . . 5
 |
2 | 1 | eldm 4646 |
. . . 4

      |
3 | | vex 2623 |
. . . . . . 7
 |
4 | | brtpos0 6031 |
. . . . . . 7
  tpos 
     |
5 | 3, 4 | ax-mp 7 |
. . . . . 6
 tpos      |
6 | | 0nelxp 4479 |
. . . . . . . 8
   |
7 | | df-rel 4459 |
. . . . . . . . 9
 tpos tpos
    |
8 | | ssel 3020 |
. . . . . . . . 9
 tpos  
 tpos
     |
9 | 7, 8 | sylbi 120 |
. . . . . . . 8
 tpos
 tpos      |
10 | 6, 9 | mtoi 626 |
. . . . . . 7
 tpos
tpos   |
11 | 1, 3 | breldm 4653 |
. . . . . . 7
 tpos 
tpos   |
12 | 10, 11 | nsyl3 592 |
. . . . . 6
 tpos 
tpos   |
13 | 5, 12 | sylbir 134 |
. . . . 5
   tpos   |
14 | 13 | exlimiv 1535 |
. . . 4
    
tpos   |
15 | 2, 14 | sylbi 120 |
. . 3
 tpos   |
16 | 15 | con2i 593 |
. 2
 tpos
  |
17 | | vex 2623 |
. . . . . 6
 |
18 | 17 | eldm 4646 |
. . . . 5
 tpos
 tpos    |
19 | | relcnv 4823 |
. . . . . . . . . . 11
  |
20 | | df-rel 4459 |
. . . . . . . . . . 11
 
     |
21 | 19, 20 | mpbi 144 |
. . . . . . . . . 10
    |
22 | 21 | sseli 3022 |
. . . . . . . . 9
      |
23 | 22 | a1i 9 |
. . . . . . . 8
  tpos          |
24 | | elsni 3468 |
. . . . . . . . . . . 12
     |
25 | 24 | breq1d 3861 |
. . . . . . . . . . 11
    tpos 
tpos     |
26 | 1, 3 | breldm 4653 |
. . . . . . . . . . . . 13
     |
27 | 26 | pm2.24d 588 |
. . . . . . . . . . . 12
         |
28 | 5, 27 | sylbi 120 |
. . . . . . . . . . 11
 tpos 

     |
29 | 25, 28 | syl6bi 162 |
. . . . . . . . . 10
    tpos         |
30 | 29 | com3l 81 |
. . . . . . . . 9
 tpos     

     |
31 | 30 | impcom 124 |
. . . . . . . 8
  tpos           |
32 | | brtpos2 6030 |
. . . . . . . . . . . 12
  tpos 
                |
33 | 3, 32 | ax-mp 7 |
. . . . . . . . . . 11
 tpos 
               |
34 | 33 | simplbi 269 |
. . . . . . . . . 10
 tpos         |
35 | | elun 3142 |
. . . . . . . . . 10
             |
36 | 34, 35 | sylib 121 |
. . . . . . . . 9
 tpos         |
37 | 36 | adantl 272 |
. . . . . . . 8
  tpos          |
38 | 23, 31, 37 | mpjaod 674 |
. . . . . . 7
  tpos       |
39 | 38 | ex 114 |
. . . . . 6
  tpos       |
40 | 39 | exlimdv 1748 |
. . . . 5
   tpos       |
41 | 18, 40 | syl5bi 151 |
. . . 4
  tpos      |
42 | 41 | ssrdv 3032 |
. . 3
 tpos
    |
43 | 42, 7 | sylibr 133 |
. 2
 tpos   |
44 | 16, 43 | impbii 125 |
1
 tpos
  |