Step | Hyp | Ref
| Expression |
1 | | xpcomf1o.1 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
2 | 1 | xpcomf1o 6727 |
. . . . . . . . 9
![F F](_cf.gif) ![: :](colon.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![-1-1-onto->
-1-1-onto->](onetooneonto.gif) ![( (](lp.gif)
![A A](_ca.gif) ![)
)](rp.gif) |
3 | | f1ofun 5377 |
. . . . . . . . 9
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![A A](_ca.gif)
![F F](_cf.gif) ![) )](rp.gif) |
4 | | funbrfv2b 5474 |
. . . . . . . . 9
![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif)
![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 2, 3, 4 | mp2b 8 |
. . . . . . . 8
![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | | ancom 264 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![w w](_w.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | eqcom 2142 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | f1odm 5379 |
. . . . . . . . . . 11
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . 10
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
10 | 9 | eleq2i 2207 |
. . . . . . . . 9
![( (](lp.gif)
![( (](lp.gif)
![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
11 | 7, 10 | anbi12i 456 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif)
![F F](_cf.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 5, 6, 11 | 3bitri 205 |
. . . . . . 7
![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 12 | anbi1i 454 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | | anass 399 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | 13, 14 | bitri 183 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 15 | exbii 1585 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![w w](_w.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![w w](_w.gif) ![G G](_cg.gif) ![v
v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | | vex 2692 |
. . . . . . 7
![_V
_V](rmcv.gif) |
18 | 1 | mptfvex 5514 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
19 | 17, 18 | mpan2 422 |
. . . . . 6
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
20 | | vex 2692 |
. . . . . . . . 9
![_V
_V](rmcv.gif) |
21 | 20 | snex 4117 |
. . . . . . . 8
![{ {](lbrace.gif) ![x x](_x.gif)
![_V _V](rmcv.gif) |
22 | 21 | cnvex 5085 |
. . . . . . 7
![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![_V _V](rmcv.gif) |
23 | 22 | uniex 4367 |
. . . . . 6
![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![_V _V](rmcv.gif) |
24 | 19, 23 | mpg 1428 |
. . . . 5
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![_V
_V](rmcv.gif) |
25 | | breq1 3940 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![w
w](_w.gif) ![G G](_cg.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 25 | anbi2d 460 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 24, 26 | ceqsexv 2728 |
. . . 4
![( (](lp.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![w w](_w.gif) ![G G](_cg.gif) ![v
v](_v.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | | elxp 4564 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 28 | anbi1i 454 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | | nfcv 2282 |
. . . . . . 7
![F/_ F/_](_finvbar.gif) ![z z](_z.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) |
31 | | xpcomco.1 |
. . . . . . . 8
![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) |
32 | | nfmpo2 5847 |
. . . . . . . 8
![F/_ F/_](_finvbar.gif) ![z z](_z.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) |
33 | 31, 32 | nfcxfr 2279 |
. . . . . . 7
![F/_ F/_](_finvbar.gif) ![z z](_z.gif) ![G G](_cg.gif) |
34 | | nfcv 2282 |
. . . . . . 7
![F/_ F/_](_finvbar.gif) ![z z](_z.gif) ![v
v](_v.gif) |
35 | 30, 33, 34 | nfbr 3982 |
. . . . . 6
![F/ F/](finv.gif) ![z z](_z.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) |
36 | 35 | 19.41 1665 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![)
)](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | | nfcv 2282 |
. . . . . . . . 9
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) |
38 | | nfmpo1 5846 |
. . . . . . . . . 10
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) |
39 | 31, 38 | nfcxfr 2279 |
. . . . . . . . 9
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![G G](_cg.gif) |
40 | | nfcv 2282 |
. . . . . . . . 9
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![v
v](_v.gif) |
41 | 37, 39, 40 | nfbr 3982 |
. . . . . . . 8
![F/ F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) |
42 | 41 | 19.41 1665 |
. . . . . . 7
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![)
)](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | | anass 399 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | | fveq2 5429 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![)
)](rp.gif) |
45 | | opelxpi 4579 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
46 | | sneq 3543 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
47 | 46 | cnveqd 4723 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
48 | 47 | unieqd 3755 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
49 | | vex 2692 |
. . . . . . . . . . . . . . . . . 18
![_V
_V](rmcv.gif) |
50 | | vex 2692 |
. . . . . . . . . . . . . . . . . 18
![_V
_V](rmcv.gif) |
51 | | opswapg 5033 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![)
)](rp.gif) |
52 | 49, 50, 51 | mp2an 423 |
. . . . . . . . . . . . . . . . 17
![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) |
53 | 48, 52 | eqtrdi 2189 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
54 | 50, 49 | opex 4159 |
. . . . . . . . . . . . . . . 16
![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![_V _V](rmcv.gif) |
55 | 53, 1, 54 | fvmpt 5506 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![<. <.](langle.gif) ![z
z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif)
![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
56 | 45, 55 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) |
57 | 44, 56 | sylan9eq 2193 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
58 | 57 | breq1d 3947 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif)
![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | | df-br 3938 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![y
y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![G G](_cg.gif)
![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![v v](_v.gif) ![G G](_cg.gif) ![) )](rp.gif) |
60 | | df-mpo 5787 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![v v](_v.gif)
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![} }](rbrace.gif) |
61 | 31, 60 | eqtri 2161 |
. . . . . . . . . . . . . . . . 17
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>.
>.](rangle.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
62 | 61 | eleq2i 2207 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![v v](_v.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![v v](_v.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>.
>.](rangle.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
63 | | oprabid 5811 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![v v](_v.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>.
>.](rangle.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
64 | 59, 62, 63 | 3bitri 205 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![<. <.](langle.gif) ![y
y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![G G](_cg.gif)
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
65 | 64 | baib 905 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>.
>.](rangle.gif) ![G G](_cg.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 65 | ancoms 266 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>.
>.](rangle.gif) ![G G](_cg.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 66 | adantl 275 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![y y](_y.gif) ![z z](_z.gif) ![>. >.](rangle.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | 58, 67 | bitrd 187 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
69 | 68 | pm5.32da 448 |
. . . . . . . . . 10
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | 69 | pm5.32i 450 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 43, 70 | bitri 183 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
72 | 71 | exbii 1585 |
. . . . . . 7
![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | 42, 72 | bitr3i 185 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | 73 | exbii 1585 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 29, 36, 74 | 3bitr2i 207 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![G G](_cg.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
76 | 16, 27, 75 | 3bitri 205 |
. . 3
![( (](lp.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | 76 | opabbii 4003 |
. 2
![{ {](lbrace.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![v v](_v.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![( (](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
78 | | df-co 4556 |
. 2
![( (](lp.gif) ![F F](_cf.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![w w](_w.gif) ![(
(](lp.gif) ![u u](_u.gif) ![F F](_cf.gif) ![w w](_w.gif) ![G G](_cg.gif) ![v v](_v.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
79 | | df-mpo 5787 |
. . 3
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![v v](_v.gif)
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![} }](rbrace.gif) |
80 | | dfoprab2 5826 |
. . 3
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![z
z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![v v](_v.gif)
![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
81 | 79, 80 | eqtri 2161 |
. 2
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![v v](_v.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
82 | 77, 78, 81 | 3eqtr4i 2171 |
1
![( (](lp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |