Step | Hyp | Ref
| Expression |
1 | | 0ex 4131 |
. . . . 5
 |
2 | 1 | eldm 4825 |
. . . 4

      |
3 | | vex 2741 |
. . . . . . 7
 |
4 | | brtpos0 6253 |
. . . . . . 7
  tpos 
     |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
 tpos      |
6 | | 0nelxp 4655 |
. . . . . . . 8
   |
7 | | df-rel 4634 |
. . . . . . . . 9
 tpos tpos
    |
8 | | ssel 3150 |
. . . . . . . . 9
 tpos  
 tpos
     |
9 | 7, 8 | sylbi 121 |
. . . . . . . 8
 tpos
 tpos      |
10 | 6, 9 | mtoi 664 |
. . . . . . 7
 tpos
tpos   |
11 | 1, 3 | breldm 4832 |
. . . . . . 7
 tpos 
tpos   |
12 | 10, 11 | nsyl3 626 |
. . . . . 6
 tpos 
tpos   |
13 | 5, 12 | sylbir 135 |
. . . . 5
   tpos   |
14 | 13 | exlimiv 1598 |
. . . 4
    
tpos   |
15 | 2, 14 | sylbi 121 |
. . 3
 tpos   |
16 | 15 | con2i 627 |
. 2
 tpos
  |
17 | | vex 2741 |
. . . . . 6
 |
18 | 17 | eldm 4825 |
. . . . 5
 tpos
 tpos    |
19 | | relcnv 5007 |
. . . . . . . . . . 11
  |
20 | | df-rel 4634 |
. . . . . . . . . . 11
 
     |
21 | 19, 20 | mpbi 145 |
. . . . . . . . . 10
    |
22 | 21 | sseli 3152 |
. . . . . . . . 9
      |
23 | 22 | a1i 9 |
. . . . . . . 8
  tpos          |
24 | | elsni 3611 |
. . . . . . . . . . . 12
     |
25 | 24 | breq1d 4014 |
. . . . . . . . . . 11
    tpos 
tpos     |
26 | 1, 3 | breldm 4832 |
. . . . . . . . . . . . 13
     |
27 | 26 | pm2.24d 622 |
. . . . . . . . . . . 12
         |
28 | 5, 27 | sylbi 121 |
. . . . . . . . . . 11
 tpos 

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

     |
31 | 30 | impcom 125 |
. . . . . . . 8
  tpos           |
32 | | brtpos2 6252 |
. . . . . . . . . . . 12
  tpos 
                |
33 | 3, 32 | ax-mp 5 |
. . . . . . . . . . 11
 tpos 
               |
34 | 33 | simplbi 274 |
. . . . . . . . . 10
 tpos         |
35 | | elun 3277 |
. . . . . . . . . 10
             |
36 | 34, 35 | sylib 122 |
. . . . . . . . 9
 tpos         |
37 | 36 | adantl 277 |
. . . . . . . 8
  tpos          |
38 | 23, 31, 37 | mpjaod 718 |
. . . . . . 7
  tpos       |
39 | 38 | ex 115 |
. . . . . 6
  tpos       |
40 | 39 | exlimdv 1819 |
. . . . 5
   tpos       |
41 | 18, 40 | biimtrid 152 |
. . . 4
  tpos      |
42 | 41 | ssrdv 3162 |
. . 3
 tpos
    |
43 | 42, 7 | sylibr 134 |
. 2
 tpos   |
44 | 16, 43 | impbii 126 |
1
 tpos
  |