Step | Hyp | Ref
| Expression |
1 | | excom 1643 |
. . . . . 6
![( (](lp.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | nfv 1509 |
. . . . . . . . . . 11
![F/ F/](finv.gif)
![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![>. >.](rangle.gif) |
3 | | cnvoprab.x |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![x x](_x.gif) ![ps ps](_psi.gif) |
4 | 2, 3 | nfan 1545 |
. . . . . . . . . 10
![F/ F/](finv.gif) ![x x](_x.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
5 | 4 | nfex 1617 |
. . . . . . . . 9
![F/ F/](finv.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
6 | | nfv 1509 |
. . . . . . . . . . . 12
![F/ F/](finv.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![>. >.](rangle.gif) |
7 | | cnvoprab.y |
. . . . . . . . . . . 12
![F/ F/](finv.gif) ![y y](_y.gif) ![ps ps](_psi.gif) |
8 | 6, 7 | nfan 1545 |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
9 | 8 | nfex 1617 |
. . . . . . . . . 10
![F/ F/](finv.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
10 | | vex 2692 |
. . . . . . . . . . . 12
![_V
_V](rmcv.gif) |
11 | | vex 2692 |
. . . . . . . . . . . 12
![_V
_V](rmcv.gif) |
12 | 10, 11 | opex 4159 |
. . . . . . . . . . 11
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![_V _V](rmcv.gif) |
13 | | opeq1 3713 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif)
![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) |
14 | 13 | eqeq2d 2152 |
. . . . . . . . . . . 12
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | | cnvoprab.1 |
. . . . . . . . . . . 12
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 14, 15 | anbi12d 465 |
. . . . . . . . . . 11
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 12, 16 | spcev 2784 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 9, 17 | exlimi 1574 |
. . . . . . . . 9
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 5, 18 | exlimi 1574 |
. . . . . . . 8
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | | cnvoprab.2 |
. . . . . . . . . . 11
![( (](lp.gif)
![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 20 | adantl 275 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) |
22 | | vex 2692 |
. . . . . . . . . . . 12
![_V
_V](rmcv.gif) |
23 | | 1stexg 6073 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![_V
_V](rmcv.gif) ![) )](rp.gif) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![_V _V](rmcv.gif) |
25 | | 2ndexg 6074 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![_V
_V](rmcv.gif) ![) )](rp.gif) |
26 | 22, 25 | ax-mp 5 |
. . . . . . . . . . 11
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![_V _V](rmcv.gif) |
27 | | eqcom 2142 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif)
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | | eqcom 2142 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 27, 28 | anbi12i 456 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![y y](_y.gif)
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | | eqopi 6078 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![y y](_y.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
31 | 29, 30 | sylan2br 286 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![)
)](rp.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
32 | 16 | bicomd 140 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 4, 8, 33 | spc2ed 6138 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![a a](_a.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![a a](_a.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 24, 26, 34 | mpanr12 436 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif)
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x
x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 21, 35 | mpcom 36 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x
x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 36 | exlimiv 1578 |
. . . . . . . 8
![( (](lp.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 19, 37 | impbii 125 |
. . . . . . 7
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif)
![E. E.](exists.gif) ![a a](_a.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 38 | exbii 1585 |
. . . . . 6
![( (](lp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif)
![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | | exrot3 1669 |
. . . . . 6
![( (](lp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif)
![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 1, 39, 40 | 3bitr2ri 208 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif)
![E. E.](exists.gif) ![a a](_a.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 41 | abbii 2256 |
. . . 4
![{ {](lbrace.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) ![{ {](lbrace.gif)
![E. E.](exists.gif) ![a a](_a.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
43 | | df-oprab 5786 |
. . . 4
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x
x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif)
![{ {](lbrace.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
44 | | df-opab 3998 |
. . . 4
![{ {](lbrace.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif)
![{ {](lbrace.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
45 | 42, 43, 44 | 3eqtr4ri 2172 |
. . 3
![{ {](lbrace.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![ph ph](_varphi.gif) ![} }](rbrace.gif) |
46 | 45 | cnveqi 4722 |
. 2
![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![} }](rbrace.gif) |
47 | | cnvopab 4948 |
. 2
![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![a a](_a.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) |
48 | 46, 47 | eqtr3i 2163 |
1
![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![z z](_z.gif) ![ph
ph](_varphi.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![a a](_a.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) |