Step | Hyp | Ref
| Expression |
1 | | brdomi 6651 |
. 2
![( (](lp.gif)
![E. E.](exists.gif) ![f
f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
2 | | f1f 5336 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![f
f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
3 | | ffvelrn 5561 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![) )](rp.gif) |
4 | 3 | ex 114 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![(
(](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 2, 4 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![(
(](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 5 | anim2d 335 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![(
(](lp.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![A A](_ca.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 6 | adantld 276 |
. . . . 5
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![(
(](lp.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | elxp4 5034 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x
x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | opelxp 4577 |
. . . . 5
![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 7, 8, 9 | 3imtr4g 204 |
. . . 4
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 10 | adantl 275 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | | elxp2 4565 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![E. E.](exists.gif)
![E. E.](exists.gif)
![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
13 | | elxp2 4565 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![E. E.](exists.gif)
![E. E.](exists.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
14 | | vex 2692 |
. . . . . . . . . . . . . . . . . 18
![_V
_V](rmcv.gif) |
15 | | vex 2692 |
. . . . . . . . . . . . . . . . . . 19
![_V
_V](rmcv.gif) |
16 | | vex 2692 |
. . . . . . . . . . . . . . . . . . 19
![_V
_V](rmcv.gif) |
17 | 15, 16 | fvex 5449 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![_V
_V](rmcv.gif) |
18 | 14, 17 | opth 4167 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![<. <.](langle.gif) ![z
z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | | f1fveq 5681 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif)
![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif)
![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | 19 | ancoms 266 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 20 | anbi2d 460 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif)
![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 18, 21 | syl5bb 191 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 22 | ex 114 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif)
![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | 23 | ad2ant2l 500 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif)
![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif)
![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | imp 123 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 25 | adantlr 469 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![) )](rp.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | | sneq 3543 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
28 | 27 | dmeqd 4749 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![{ {](lbrace.gif) ![x x](_x.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
29 | 28 | unieqd 3755 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
30 | 14, 16 | op1sta 5028 |
. . . . . . . . . . . . . . . 16
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![z z](_z.gif) |
31 | 29, 30 | eqtrdi 2189 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![z z](_z.gif) ![) )](rp.gif) |
32 | 27 | rneqd 4776 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![{ {](lbrace.gif) ![x x](_x.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
33 | 32 | unieqd 3755 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
34 | 14, 16 | op2nda 5031 |
. . . . . . . . . . . . . . . . 17
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![w w](_w.gif) |
35 | 33, 34 | eqtrdi 2189 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif)
![w w](_w.gif) ![) )](rp.gif) |
36 | 35 | fveq2d 5433 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 31, 36 | opeq12d 3721 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
38 | | sneq 3543 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
39 | 38 | dmeqd 4749 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif)
![{ {](lbrace.gif) ![y y](_y.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
40 | 39 | unieqd 3755 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
41 | | vex 2692 |
. . . . . . . . . . . . . . . . 17
![_V
_V](rmcv.gif) |
42 | | vex 2692 |
. . . . . . . . . . . . . . . . 17
![_V
_V](rmcv.gif) |
43 | 41, 42 | op1sta 5028 |
. . . . . . . . . . . . . . . 16
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![v v](_v.gif) |
44 | 40, 43 | eqtrdi 2189 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![v v](_v.gif) ![) )](rp.gif) |
45 | 38 | rneqd 4776 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif)
![{ {](lbrace.gif) ![y y](_y.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
46 | 45 | unieqd 3755 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
47 | 41, 42 | op2nda 5031 |
. . . . . . . . . . . . . . . . 17
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![u u](_u.gif) |
48 | 46, 47 | eqtrdi 2189 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![u u](_u.gif) ![) )](rp.gif) |
49 | 48 | fveq2d 5433 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 44, 49 | opeq12d 3721 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y
y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) |
51 | 37, 50 | eqeqan12d 2156 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![z
z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | 51 | ad2antlr 481 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![) )](rp.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![w w](_w.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![u u](_u.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | | eqeq12 2153 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
![( (](lp.gif)
![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 14, 16 | opth 4167 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![<. <.](langle.gif) ![z
z](_z.gif) ![w w](_w.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) |
55 | 53, 54 | syl6bb 195 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | 55 | ad2antlr 481 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![) )](rp.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![(
(](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | 26, 52, 56 | 3bitr4d 219 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![) )](rp.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 57 | exp53 375 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 58 | com23 78 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 59 | rexlimivv 2558 |
. . . . . . . 8
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif)
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 60 | rexlimdvv 2559 |
. . . . . . 7
![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y
y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 61 | imp 123 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif)
![E. E.](exists.gif)
![E. E.](exists.gif)
![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
63 | 12, 13, 62 | syl2anb 289 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y
y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | 63 | com12 30 |
. . . 4
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif)
![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | 64 | adantl 275 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif)
![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | | xpdom.2 |
. . . . 5
![_V
_V](rmcv.gif) |
67 | | reldom 6647 |
. . . . . 6
![~<_ ~<_](preccurlyeq.gif) |
68 | 67 | brrelex1i 4590 |
. . . . 5
![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
69 | | xpexg 4661 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
70 | 66, 68, 69 | sylancr 411 |
. . . 4
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
71 | 70 | adantr 274 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
72 | 67 | brrelex2i 4591 |
. . . . 5
![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
73 | | xpexg 4661 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![( (](lp.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
74 | 66, 72, 73 | sylancr 411 |
. . . 4
![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
75 | 74 | adantr 274 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
76 | 11, 65, 71, 75 | dom3d 6676 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | 1, 76 | exlimddv 1871 |
1
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |