Step | Hyp | Ref
| Expression |
1 | | 0ex 4063 |
. . . . 5
![_V _V](rmcv.gif) |
2 | 1 | eldm 4744 |
. . . 4
![( (](lp.gif)
![E. E.](exists.gif) ![y y](_y.gif) ![(/) (/)](varnothing.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) |
3 | | vex 2692 |
. . . . . . 7
![_V
_V](rmcv.gif) |
4 | | brtpos0 6157 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) tpos ![F F](_cf.gif)
![(/) (/)](varnothing.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
![( (](lp.gif) tpos ![F F](_cf.gif) ![(/) (/)](varnothing.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) |
6 | | 0nelxp 4575 |
. . . . . . . 8
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
7 | | df-rel 4554 |
. . . . . . . . 9
![( (](lp.gif) tpos tpos
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | ssel 3096 |
. . . . . . . . 9
![( (](lp.gif) tpos ![( (](lp.gif) ![_V _V](rmcv.gif)
![( (](lp.gif) tpos
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
9 | 7, 8 | sylbi 120 |
. . . . . . . 8
![( (](lp.gif) tpos
![( (](lp.gif) tpos ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 6, 9 | mtoi 654 |
. . . . . . 7
![( (](lp.gif) tpos
tpos ![F F](_cf.gif) ![) )](rp.gif) |
11 | 1, 3 | breldm 4751 |
. . . . . . 7
![( (](lp.gif) tpos ![F F](_cf.gif)
tpos ![F F](_cf.gif) ![) )](rp.gif) |
12 | 10, 11 | nsyl3 616 |
. . . . . 6
![( (](lp.gif) tpos ![F F](_cf.gif)
tpos ![F F](_cf.gif) ![) )](rp.gif) |
13 | 5, 12 | sylbir 134 |
. . . . 5
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![F F](_cf.gif) tpos ![F F](_cf.gif) ![) )](rp.gif) |
14 | 13 | exlimiv 1578 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(/) (/)](varnothing.gif) ![F F](_cf.gif)
tpos ![F F](_cf.gif) ![) )](rp.gif) |
15 | 2, 14 | sylbi 120 |
. . 3
![( (](lp.gif) tpos ![F F](_cf.gif) ![) )](rp.gif) |
16 | 15 | con2i 617 |
. 2
![( (](lp.gif) tpos
![F F](_cf.gif) ![) )](rp.gif) |
17 | | vex 2692 |
. . . . . 6
![_V
_V](rmcv.gif) |
18 | 17 | eldm 4744 |
. . . . 5
![( (](lp.gif) tpos
![E. E.](exists.gif) tpos ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) |
19 | | relcnv 4925 |
. . . . . . . . . . 11
![`' `'](_cnv.gif) ![F F](_cf.gif) |
20 | | df-rel 4554 |
. . . . . . . . . . 11
![( (](lp.gif) ![`' `'](_cnv.gif)
![`' `'](_cnv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 19, 20 | mpbi 144 |
. . . . . . . . . 10
![`' `'](_cnv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
22 | 21 | sseli 3098 |
. . . . . . . . 9
![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 22 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) tpos ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | | elsni 3550 |
. . . . . . . . . . . 12
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
25 | 24 | breq1d 3947 |
. . . . . . . . . . 11
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) tpos ![F F](_cf.gif)
tpos ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 1, 3 | breldm 4751 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![F F](_cf.gif) ![F F](_cf.gif) ![) )](rp.gif) |
27 | 26 | pm2.24d 612 |
. . . . . . . . . . . 12
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 5, 27 | sylbi 120 |
. . . . . . . . . . 11
![( (](lp.gif) tpos ![F F](_cf.gif)
![( (](lp.gif)
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 25, 28 | syl6bi 162 |
. . . . . . . . . 10
![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) tpos ![F F](_cf.gif) ![(
(](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 29 | com3l 81 |
. . . . . . . . 9
![( (](lp.gif) tpos ![F
F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif)
![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 30 | impcom 124 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) tpos ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | | brtpos2 6156 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) tpos ![F F](_cf.gif)
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![F F](_cf.gif) ![y
y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 3, 32 | ax-mp 5 |
. . . . . . . . . . 11
![( (](lp.gif) tpos ![F
F](_cf.gif)
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![F F](_cf.gif) ![y
y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 33 | simplbi 272 |
. . . . . . . . . 10
![( (](lp.gif) tpos ![F
F](_cf.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | elun 3222 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![`' `'](_cnv.gif) ![{
{](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 34, 35 | sylib 121 |
. . . . . . . . 9
![( (](lp.gif) tpos ![F
F](_cf.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 36 | adantl 275 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) tpos ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 23, 31, 37 | mpjaod 708 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) tpos ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) |
39 | 38 | ex 114 |
. . . . . 6
![( (](lp.gif) ![(
(](lp.gif) tpos ![F F](_cf.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
40 | 39 | exlimdv 1792 |
. . . . 5
![( (](lp.gif) ![(
(](lp.gif) ![E. E.](exists.gif) tpos ![F
F](_cf.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 18, 40 | syl5bi 151 |
. . . 4
![( (](lp.gif) ![(
(](lp.gif) tpos ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
42 | 41 | ssrdv 3108 |
. . 3
![( (](lp.gif) tpos
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 42, 7 | sylibr 133 |
. 2
![( (](lp.gif) tpos ![F F](_cf.gif) ![) )](rp.gif) |
44 | 16, 43 | impbii 125 |
1
![( (](lp.gif) tpos
![F F](_cf.gif) ![) )](rp.gif) |