Step | Hyp | Ref
| Expression |
1 | | 0ex 4523 |
. . . . 5
 |
2 | 1 | eldm 5138 |
. . . 4

      |
3 | | vex 3074 |
. . . . . . 7
 |
4 | | brtpos0 6855 |
. . . . . . 7
  tpos 
     |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
 tpos      |
6 | | 0nelxp 4968 |
. . . . . . . 8
   |
7 | | df-rel 4948 |
. . . . . . . . 9
 tpos tpos
    |
8 | | ssel 3451 |
. . . . . . . . 9
 tpos  
 tpos
     |
9 | 7, 8 | sylbi 195 |
. . . . . . . 8
 tpos
 tpos      |
10 | 6, 9 | mtoi 178 |
. . . . . . 7
 tpos
tpos   |
11 | 1, 3 | breldm 5145 |
. . . . . . 7
 tpos 
tpos   |
12 | 10, 11 | nsyl3 119 |
. . . . . 6
 tpos 
tpos   |
13 | 5, 12 | sylbir 213 |
. . . . 5
   tpos   |
14 | 13 | exlimiv 1689 |
. . . 4
    
tpos   |
15 | 2, 14 | sylbi 195 |
. . 3
 tpos   |
16 | 15 | con2i 120 |
. 2
 tpos
  |
17 | | vex 3074 |
. . . . . 6
 |
18 | 17 | eldm 5138 |
. . . . 5
 tpos
 tpos    |
19 | | relcnv 5307 |
. . . . . . . . . . 11
  |
20 | | df-rel 4948 |
. . . . . . . . . . 11
 
     |
21 | 19, 20 | mpbi 208 |
. . . . . . . . . 10
    |
22 | 21 | sseli 3453 |
. . . . . . . . 9
      |
23 | 22 | a1i 11 |
. . . . . . . 8
  tpos          |
24 | | elsni 4003 |
. . . . . . . . . . . 12
     |
25 | 24 | breq1d 4403 |
. . . . . . . . . . 11
    tpos 
tpos     |
26 | 1, 3 | breldm 5145 |
. . . . . . . . . . . . 13
     |
27 | 26 | pm2.24d 143 |
. . . . . . . . . . . 12
         |
28 | 5, 27 | sylbi 195 |
. . . . . . . . . . 11
 tpos 

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

     |
31 | 30 | impcom 430 |
. . . . . . . 8
  tpos           |
32 | | brtpos2 6854 |
. . . . . . . . . . . 12
  tpos 
                |
33 | 3, 32 | ax-mp 5 |
. . . . . . . . . . 11
 tpos 
               |
34 | 33 | simplbi 460 |
. . . . . . . . . 10
 tpos         |
35 | | elun 3598 |
. . . . . . . . . 10
             |
36 | 34, 35 | sylib 196 |
. . . . . . . . 9
 tpos         |
37 | 36 | adantl 466 |
. . . . . . . 8
  tpos          |
38 | 23, 31, 37 | mpjaod 381 |
. . . . . . 7
  tpos       |
39 | 38 | ex 434 |
. . . . . 6
  tpos       |
40 | 39 | exlimdv 1691 |
. . . . 5
   tpos       |
41 | 18, 40 | syl5bi 217 |
. . . 4
  tpos      |
42 | 41 | ssrdv 3463 |
. . 3
 tpos
    |
43 | 42, 7 | sylibr 212 |
. 2
 tpos   |
44 | 16, 43 | impbii 188 |
1
 tpos
  |