Theorem List for Intuitionistic Logic Explorer - 5901-6000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ovmpt4g 5901* |
Value of a function given by the maps-to notation. (This is the
operation analog of fvmpt2 5512.) (Contributed by NM, 21-Feb-2004.)
(Revised by Mario Carneiro, 1-Sep-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![V V](_cv.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ovmpos 5902* |
Value of a function given by the maps-to notation, expressed using
explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![y y](_y.gif) ![]_ ]_](_urbrack.gif) ![V V](_cv.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![[_
[_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_
[_](_ulbrack.gif) ![y y](_y.gif) ![]_ ]_](_urbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | ov2gf 5903* |
The value of an operation class abstraction. A version of ovmpog 5913
using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![( (](lp.gif)
![G G](_cg.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpodxf 5904* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![L L](_cl.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![L L](_cl.gif) ![( (](lp.gif) ![X X](_cx.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpodx 5905* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![L L](_cl.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![L L](_cl.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpod 5906* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 7-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpox 5907* |
The value of an operation class abstraction. Variant of ovmpoga 5908 which
does not require and to be
distinct. (Contributed by Jeff
Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![( (](lp.gif)
![L L](_cl.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpoga 5908* |
Value of an operation given by a maps-to rule. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpoa 5909* |
Value of an operation given by a maps-to rule. (Contributed by NM,
19-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![( (](lp.gif) ![C C](_cc.gif)
![R R](_cr.gif)
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpodf 5910* |
Alternate deduction version of ovmpo 5914, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![F/
F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovmpodv 5911* |
Alternate deduction version of ovmpo 5914, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovmpodv2 5912* |
Alternate deduction version of ovmpo 5914, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovmpog 5913* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy,
19-Jun-2012.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif)
![S S](_cs.gif)
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovmpo 5914* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 16-May-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif)
![S S](_cs.gif)
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovi3 5915* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![( (](lp.gif)
![H H](_ch.gif) ![) )](rp.gif)
![( (](lp.gif)
![H H](_ch.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![S S](_cs.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif)
![( (](lp.gif) ![H H](_ch.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![w w](_w.gif) ![E. E.](exists.gif) ![v v](_v.gif) ![E. E.](exists.gif) ![u u](_u.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif)
![<. <.](langle.gif) ![u u](_u.gif) ![f f](_f.gif) ![>. >.](rangle.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![H H](_ch.gif) ![( (](lp.gif) ![H H](_ch.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![F F](_cf.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ov6g 5916* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 13-Nov-2006.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif)
![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![<. <.](langle.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![C C](_cc.gif) ![J J](_cj.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ovg 5917* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![E! E!](_e1.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![th th](_theta.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovres 5918 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovresd 5919 |
Lemma for converting metric theorems to metric space theorems.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![D D](_cd.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | oprssov 5920 |
The value of a member of the domain of a subclass of an operation.
(Contributed by NM, 23-Aug-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![D D](_cd.gif) ![F F](_cf.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fovrn 5921 |
An operation's value belongs to its codomain. (Contributed by NM,
27-Aug-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(
(](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![-->
-->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fovrnda 5922 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fovrnd 5923 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | fnrnov 5924* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by NM, 29-Oct-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | foov 5925* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-onto->
-onto->](onto.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-->
-->](longrightarrow.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fnovrn 5926 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![D D](_cd.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | ovelrn 5927* |
A member of an operation's range is a value of the operation.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
30-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![E. E.](exists.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funimassov 5928* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovelimab 5929* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ovconst2 5930 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![S S](_cs.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | caovclg 5931* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![E E](_ce.gif) ![) )](rp.gif) |
|
Theorem | caovcld 5932* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![E E](_ce.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![E E](_ce.gif) ![) )](rp.gif) |
|
Theorem | caovcl 5933* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | caovcomg 5934* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovcomd 5935* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovcom 5936* |
Convert an operation commutative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | caovassg 5937* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro,
26-May-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovassd 5938* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovass 5939* |
Convert an operation associative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
![( (](lp.gif) ![(
(](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovcang 5940* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![z z](_z.gif)
![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovcand 5941* |
Convert an operation cancellation law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![z z](_z.gif)
![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovcanrd 5942* |
Commute the arguments of an operation cancellation law. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![z z](_z.gif)
![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![A A](_ca.gif)
![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovcan 5943* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.)
|
![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![z z](_z.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovordig 5944* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif)
![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovordid 5945* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovordg 5946* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif)
![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovordd 5947* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovord2d 5948* |
Operation ordering law with commuted arguments. (Contributed by Mario
Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovord3d 5949* |
Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovord 5950* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.)
|
![( (](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovord2 5951* |
Operation ordering law with commuted arguments. (Contributed by NM,
27-Feb-1996.)
|
![( (](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovord3 5952* |
Ordering law. (Contributed by NM, 29-Feb-1996.)
|
![( (](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![z z](_z.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdig 5953* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![B B](_cb.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdid 5954* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![B B](_cb.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdir2d 5955* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdirg 5956* |
Convert an operation reverse distributive law to class notation.
(Contributed by Mario Carneiro, 19-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![K K](_ck.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![G G](_cg.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![K K](_ck.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdird 5957* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![K K](_ck.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![G G](_cg.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![H H](_ch.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdi 5958* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov32d 5959* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov12d 5960* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov31d 5961* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov13d 5962* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov4d 5963* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov411d 5964* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov42d 5965* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![D D](_cd.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov32 5966* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | caov12 5967* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caov31 5968* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![) )](rp.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | caov13 5969* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovdilemd 5970* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![G G](_cg.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![) )](rp.gif) ![G G](_cg.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![( (](lp.gif) ![C C](_cc.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![) )](rp.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![( (](lp.gif) ![D D](_cd.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovlem2d 5971* |
Rearrangement of expression involving multiplication ( ) and
addition ( ).
(Contributed by Jim Kingdon, 3-Jan-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![G G](_cg.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![) )](rp.gif) ![G G](_cg.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![( (](lp.gif) ![y y](_y.gif) ![G G](_cg.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![G G](_cg.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![D D](_cd.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![G G](_cg.gif) ![R R](_cr.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![D D](_cd.gif) ![G G](_cg.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![G G](_cg.gif) ![R R](_cr.gif) ![) )](rp.gif) ![F F](_cf.gif) ![( (](lp.gif) ![D D](_cd.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caovimo 5972* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is . (Contributed by Jim Kingdon,
18-Sep-2019.)
|
![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![y y](_y.gif) ![) )](rp.gif) ![F F](_cf.gif) ![z z](_z.gif) ![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![( (](lp.gif) ![y y](_y.gif) ![F F](_cf.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![F F](_cf.gif) ![B B](_cb.gif) ![x x](_x.gif) ![( (](lp.gif) ![E* E*](_em1.gif) ![w w](_w.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![F F](_cf.gif) ![w w](_w.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | grprinvlem 5973* |
Lemma for grprinvd 5974. (Contributed by NM, 9-Aug-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![y y](_y.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E. E.](exists.gif) ![( (](lp.gif)
![x x](_x.gif) ![O O](_co.gif) ![( (](lp.gif) ![(
(](lp.gif)
![ps ps](_psi.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![X X](_cx.gif)
![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![O O](_co.gif) ![) )](rp.gif) |
|
Theorem | grprinvd 5974* |
Deduce right inverse from left inverse and left identity in an
associative structure (such as a group). (Contributed by NM,
10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![y y](_y.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E. E.](exists.gif) ![( (](lp.gif)
![x x](_x.gif) ![O O](_co.gif) ![( (](lp.gif) ![(
(](lp.gif)
![ps ps](_psi.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![X X](_cx.gif)
![O O](_co.gif) ![( (](lp.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![N N](_cn.gif)
![O O](_co.gif) ![) )](rp.gif) |
|
Theorem | grpridd 5975* |
Deduce right identity from left inverse and left identity in an
associative structure (such as a group). (Contributed by NM,
10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![y y](_y.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E. E.](exists.gif) ![( (](lp.gif)
![x x](_x.gif) ![O O](_co.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![O O](_co.gif)
![x x](_x.gif) ![) )](rp.gif) |
|
2.6.11 Maps-to notation
|
|
Theorem | elmpocl 5976* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![F F](_cf.gif) ![T T](_ct.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elmpocl1 5977* |
If a two-parameter class is inhabited, the first argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![F F](_cf.gif) ![T T](_ct.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | elmpocl2 5978* |
If a two-parameter class is inhabited, the second argument is in its
nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan
O'Rear, 7-Mar-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![F F](_cf.gif) ![T T](_ct.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | elovmpo 5979* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Y Y](_cy.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![D D](_cd.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | f1ocnvd 5980* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![X X](_cx.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | f1od 5981* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![X X](_cx.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1ocnv2d 5982* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | f1o2d 5983* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1opw2 5984* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 5985 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![a a](_a.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![b
b](_b.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![~P ~P](scrp.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![~P ~P](scrp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | f1opw 5985* |
A one-to-one mapping induces a one-to-one mapping on power sets.
(Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario
Carneiro, 26-Jun-2015.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![" "](backquote.gif) ![b
b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![~P ~P](scrp.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![~P ~P](scrp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | suppssfv 5986* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![" "](backquote.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![Y Y](_cy.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![L L](_cl.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![Y Y](_cy.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![V V](_cv.gif) ![( (](lp.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![" "](backquote.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![Z Z](_cz.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![L L](_cl.gif) ![) )](rp.gif) |
|
Theorem | suppssov1 5987* |
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![" "](backquote.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![Y Y](_cy.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![L L](_cl.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![Y Y](_cy.gif) ![O O](_co.gif) ![v v](_v.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![O O](_co.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![" "](backquote.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![Z Z](_cz.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![L L](_cl.gif) ![) )](rp.gif) |
|
2.6.12 Function operation
|
|
Syntax | cof 5988 |
Extend class notation to include mapping of an operation to a function
operation.
|
![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) |
|
Syntax | cofr 5989 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) |
|
Definition | df-of 5990* |
Define the function operation map. The definition is designed so that
if is a binary
operation, then ![o o](circ.gif) ![F F](subf.gif) is the analogous operation
on functions which corresponds to applying pointwise to the values
of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
|
![o o](circ.gif) ![F F](subf.gif) ![( (](lp.gif)
![_V _V](rmcv.gif)
![( (](lp.gif)
![( (](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-ofr 5991* |
Define the function relation map. The definition is designed so that if
is a binary
relation, then ![o o](circ.gif) ![F F](subf.gif) is the analogous relation on
functions which is true when each element of the left function relates
to the corresponding element of the right function. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
![o o](circ.gif) ![R R](subr.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![f f](_f.gif) ![g g](_g.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | ofeq 5992 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![o o](circ.gif) ![F F](subf.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ofreq 5993 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
![( (](lp.gif) ![o o](circ.gif) ![R R](subr.gif) ![o o](circ.gif) ![R R](subr.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ofexg 5994 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![A A](_ca.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | nfof 5995 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) |
|
Theorem | nfofr 5996 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
![F/_ F/_](_finvbar.gif) ![x x](_x.gif) ![F/_ F/_](_finvbar.gif) ![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) |
|
Theorem | offval 5997* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ofrfval 5998* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) ![A. A.](forall.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ofvalg 5999 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![X X](_cx.gif)
![D D](_cd.gif) ![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif)
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![U U](_cu.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![) )](rp.gif) ![` `](backtick.gif) ![X X](_cx.gif)
![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ofrval 6000 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![X X](_cx.gif)
![D D](_cd.gif) ![( (](lp.gif) ![(
(](lp.gif)
![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) ![S S](_cs.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![D D](_cd.gif) ![) )](rp.gif) |