Theorem List for Intuitionistic Logic Explorer - 6501-6600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ecidg 6501 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8-Jan-2020.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | qsid 6502 |
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by NM,
13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif)
![A A](_ca.gif) |
|
Theorem | ectocld 6503* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![B B](_cb.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![(
(](lp.gif) ![S S](_cs.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | ectocl 6504* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![B B](_cb.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | elqsn0m 6505* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif)
![E. E.](exists.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | elqsn0 6506 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif)
![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | ecelqsdm 6507 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif)
![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif)
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | xpider 6508 |
A square Cartesian product is an equivalence relation (in general it's not
a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![A A](_ca.gif) |
|
Theorem | iinerm 6509* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![B B](_cb.gif) ![|^|_ |^|_](_capbar.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | riinerm 6510* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![|^|_ |^|_](_capbar.gif) ![R R](_cr.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | erinxp 6511 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ecinxp 6512 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) !["
"](backquote.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qsinxp 6513 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![" "](backquote.gif) ![A A](_ca.gif)
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qsel 6514 |
If an element of a quotient set contains a given element, it is equal to
the equivalence class of the element. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![B B](_cb.gif) ![[ [](lbrack.gif) ![C C](_cc.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | qliftlem 6515* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif)
![( (](lp.gif) ![X X](_cx.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qliftrel 6516* |
, a function lift, is
a subset of . (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![Y Y](_cy.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qliftel 6517* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![C C](_cc.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![F F](_cf.gif) ![E.
E.](exists.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif)
![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | qliftel1 6518* |
Elementhood in the relation . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![F F](_cf.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | qliftfun 6519* |
The function is the
unique function defined by
![F F](_cf.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![x
x](_x.gif) , provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | qliftfund 6520* |
The function is the
unique function defined by
![F F](_cf.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![x
x](_x.gif) , provided that the well-definedness condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif)
![B B](_cb.gif) ![( (](lp.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | qliftfuns 6521* |
The function is the
unique function defined by
![F F](_cf.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![x
x](_x.gif) , provided that the well-definedness condition
holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![(
(](lp.gif) ![y y](_y.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qliftf 6522* |
The domain and range of the function . (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![X X](_cx.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![Y Y](_cy.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qliftval 6523* |
The value of the function . (Contributed by Mario Carneiro,
23-Dec-2016.)
|
![( (](lp.gif)
![<. <.](langle.gif) ![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![C C](_cc.gif) ![] ]](rbrack.gif) ![R R](_cr.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ecoptocl 6524* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
|
Theorem | 2ecoptocl 6525* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![ch ch](_chi.gif) ![) )](rp.gif) |
|
Theorem | 3ecoptocl 6526* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![th th](_theta.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![ph ph](_varphi.gif) ![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif) ![th th](_theta.gif) ![) )](rp.gif) |
|
Theorem | brecop 6527* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif)
![H H](_ch.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif)
![G G](_cg.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![G G](_cg.gif) ![( (](lp.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif)
![G G](_cg.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eroveu 6528* |
Lemma for eroprf 6530. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![/. /.](diagup.gif) ![S S](_cs.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![:
:](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![r r](_r.gif) ![R R](_cr.gif) ![t t](_t.gif) ![S S](_cs.gif) ![u u](_u.gif) ![( (](lp.gif)
![t t](_t.gif) ![) )](rp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![K K](_ck.gif) ![) )](rp.gif)
![E! E!](_e1.gif) ![z z](_z.gif) ![E. E.](exists.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![p p](_p.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![q q](_q.gif) ![] ]](rbrack.gif) ![S S](_cs.gif) ![[ [](lbrack.gif) ![( (](lp.gif) ![q q](_q.gif) ![) )](rp.gif) ![] ]](rbrack.gif) ![T T](_ct.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | erovlem 6529* |
Lemma for eroprf 6530. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![/. /.](diagup.gif) ![S S](_cs.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![:
:](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![r r](_r.gif) ![R R](_cr.gif) ![t t](_t.gif) ![S S](_cs.gif) ![u u](_u.gif) ![( (](lp.gif)
![t t](_t.gif) ![) )](rp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![E.
E.](exists.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![p p](_p.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![q
q](_q.gif) ![] ]](rbrack.gif) ![S S](_cs.gif) ![[ [](lbrack.gif) ![(
(](lp.gif) ![q q](_q.gif) ![)
)](rp.gif) ![] ]](rbrack.gif) ![T T](_ct.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![J J](_cj.gif)
![( (](lp.gif) ![iota iota](riota.gif) ![z
z](_z.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![p p](_p.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![q
q](_q.gif) ![] ]](rbrack.gif) ![S S](_cs.gif) ![[ [](lbrack.gif) ![(
(](lp.gif) ![q q](_q.gif) ![)
)](rp.gif) ![] ]](rbrack.gif) ![T T](_ct.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eroprf 6530* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![/.
/.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![B B](_cb.gif) ![/. /.](diagup.gif) ![S S](_cs.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![:
:](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![r r](_r.gif) ![R R](_cr.gif) ![t t](_t.gif) ![S S](_cs.gif) ![u u](_u.gif) ![( (](lp.gif)
![t t](_t.gif) ![) )](rp.gif) ![T T](_ct.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![E.
E.](exists.gif) ![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![p p](_p.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![q
q](_q.gif) ![] ]](rbrack.gif) ![S S](_cs.gif) ![[ [](lbrack.gif) ![(
(](lp.gif) ![q q](_q.gif) ![)
)](rp.gif) ![] ]](rbrack.gif) ![T T](_ct.gif) ![) )](rp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![Y Y](_cy.gif) ![( (](lp.gif) ![C C](_cc.gif) ![/.
/.](diagup.gif) ![T T](_ct.gif) ![( (](lp.gif) ![: :](colon.gif) ![( (](lp.gif) ![K K](_ck.gif) ![) )](rp.gif) ![-->
-->](longrightarrow.gif) ![L L](_cl.gif) ![) )](rp.gif) |
|
Theorem | eroprf2 6531* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
![( (](lp.gif) ![A A](_ca.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![E. E.](exists.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![p p](_p.gif) ![[ [](lbrack.gif) ![q
q](_q.gif)
![[ [](lbrack.gif) ![(
(](lp.gif) ![q q](_q.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![U U](_cu.gif) ![( (](lp.gif) ![: :](colon.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![-->
-->](longrightarrow.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![u u](_u.gif) ![( (](lp.gif) ![t t](_t.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![: :](colon.gif) ![( (](lp.gif) ![J J](_cj.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![J J](_cj.gif) ![) )](rp.gif) |
|
Theorem | ecopoveq 6532* |
This is the first of several theorems about equivalence relations of
the kind used in construction of fractions and signed reals, involving
operations on equivalent classes of ordered pairs. This theorem
expresses the relation (specified by the hypothesis) in terms
of its operation . (Contributed by NM, 16-Aug-1995.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecopovsym 6533* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![y y](_y.gif)
![( (](lp.gif)
![x x](_x.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ecopovtrn 6534* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![y y](_y.gif)
![( (](lp.gif)
![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif)
![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif)
![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![z z](_z.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ecopover 6535* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![y y](_y.gif)
![( (](lp.gif)
![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif)
![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![y y](_y.gif)
![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![z z](_z.gif)
![z z](_z.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | ecopovsymg 6536* |
Assuming the operation is commutative, show that the relation
,
specified by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ecopovtrng 6537* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is transitive.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.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) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![z z](_z.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ecopoverg 6538* |
Assuming that operation is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
,
specified by the first hypothesis, is an equivalence
relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![u u](_u.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![y y](_y.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.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) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![y y](_y.gif) ![( (](lp.gif) ![z z](_z.gif)
![z z](_z.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | th3qlem1 6539* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The
third hypothesis is the compatibility assumption. (Contributed by NM,
3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![z z](_z.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif)
![) )](rp.gif) ![E* E*](_em1.gif) ![x x](_x.gif) ![E. E.](exists.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![y y](_y.gif) ![[ [](lbrack.gif) ![z
z](_z.gif)
![[ [](lbrack.gif) ![(
(](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | th3qlem2 6540* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60,
extended to operations on ordered pairs. The fourth hypothesis is the
compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif)
![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif)
![<. <.](langle.gif) ![s s](_s.gif) ![f f](_f.gif)
![<. <.](langle.gif) ![g g](_g.gif) ![h h](_h.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![<.
<.](langle.gif) ![s s](_s.gif) ![f f](_f.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif)
![<. <.](langle.gif) ![g g](_g.gif) ![h h](_h.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) ![E* E*](_em1.gif) ![z z](_z.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) ![t t](_t.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![(
(](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | th3qcor 6541* |
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif)
![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif)
![<. <.](langle.gif) ![s s](_s.gif) ![f f](_f.gif)
![<. <.](langle.gif) ![g g](_g.gif) ![h h](_h.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![<.
<.](langle.gif) ![s s](_s.gif) ![f f](_f.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif)
![<. <.](langle.gif) ![g g](_g.gif) ![h h](_h.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.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) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![S S](_cs.gif) ![) )](rp.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) ![t t](_t.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![<.
<.](langle.gif) ![u u](_u.gif) ![t t](_t.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![G G](_cg.gif) |
|
Theorem | th3q 6542* |
Theorem 3Q of [Enderton] p. 60, extended to
operations on ordered
pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif)
![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif)
![<. <.](langle.gif) ![s s](_s.gif) ![f f](_f.gif)
![<. <.](langle.gif) ![g g](_g.gif) ![h h](_h.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![<.
<.](langle.gif) ![s s](_s.gif) ![f f](_f.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif)
![<. <.](langle.gif) ![g g](_g.gif) ![h h](_h.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.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) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![S S](_cs.gif) ![) )](rp.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) ![t t](_t.gif) ![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![u u](_u.gif) ![t t](_t.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![v v](_v.gif) ![<.
<.](langle.gif) ![u u](_u.gif) ![t t](_t.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![G G](_cg.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![<.
<.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | oviec 6543* |
Express an operation on equivalence classes of ordered pairs in terms of
equivalence class of operations on ordered pairs. See iset.mm for
additional comments describing the hypotheses. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 4-Jun-2013.)
(Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro,
4-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![z z](_z.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) ![( (](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) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![b b](_b.gif) ![( (](lp.gif)
![d d](_d.gif) ![) )](rp.gif)
![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![h h](_h.gif) ![( (](lp.gif) ![s s](_s.gif) ![) )](rp.gif) ![( (](lp.gif) ![ch ch](_chi.gif) ![) )](rp.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) ![S S](_cs.gif)
![( (](lp.gif) ![S S](_cs.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) ![J J](_cj.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![b b](_b.gif) ![( (](lp.gif)
![h h](_h.gif) ![) )](rp.gif)
![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![d d](_d.gif) ![( (](lp.gif) ![s s](_s.gif) ![) )](rp.gif) ![L L](_cl.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif)
![H H](_ch.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)
![Q Q](_cq.gif) ![E. E.](exists.gif) ![a a](_a.gif) ![E. E.](exists.gif) ![b b](_b.gif) ![E. E.](exists.gif) ![c c](_c.gif) ![E. E.](exists.gif) ![d d](_d.gif) ![(
(](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![b b](_b.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![c c](_c.gif) ![d d](_d.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![a a](_a.gif) ![b b](_b.gif) ![<.
<.](langle.gif) ![c c](_c.gif) ![d d](_d.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ch ch](_chi.gif)
![L L](_cl.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![H H](_ch.gif) ![) )](rp.gif) |
|
Theorem | ecovcom 6544* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6545 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![D D](_cd.gif) ![G G](_cg.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![H H](_ch.gif) ![J J](_cj.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecovicom 6545* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![D D](_cd.gif) ![G G](_cg.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![H H](_ch.gif) ![J J](_cj.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![H H](_ch.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![J J](_cj.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecovass 6546* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6547 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![N N](_cn.gif) ![Q Q](_cq.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![J J](_cj.gif) ![K K](_ck.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![N N](_cn.gif) ![Q Q](_cq.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![L L](_cl.gif) ![M M](_cm.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecoviass 6547* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![N N](_cn.gif) ![Q Q](_cq.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![G G](_cg.gif) ![H H](_ch.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![J J](_cj.gif) ![K K](_ck.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![N N](_cn.gif) ![Q Q](_cq.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![L L](_cl.gif) ![M M](_cm.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![L L](_cl.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![M M](_cm.gif) ![( (](lp.gif) ![(
(](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecovdi 6548* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6549 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![M M](_cm.gif) ![N N](_cn.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![M M](_cm.gif) ![N N](_cn.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![H H](_ch.gif) ![J J](_cj.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![W W](_cw.gif) ![X X](_cx.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![Y Y](_cy.gif) ![Z Z](_cz.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![W W](_cw.gif) ![X X](_cx.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![Y Y](_cy.gif) ![Z Z](_cz.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![K K](_ck.gif) ![L L](_cl.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecovidi 6549* |
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17-Sep-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![M M](_cm.gif) ![N N](_cn.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![M M](_cm.gif) ![N N](_cn.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![H H](_ch.gif) ![J J](_cj.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![W W](_cw.gif) ![X X](_cx.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![Y Y](_cy.gif) ![Z Z](_cz.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![W W](_cw.gif) ![X X](_cx.gif) ![>. >.](rangle.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![Y Y](_cy.gif) ![Z Z](_cz.gif) ![>. >.](rangle.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![K K](_ck.gif) ![L L](_cl.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![K K](_ck.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif)
![S S](_cs.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif)
![L L](_cl.gif) ![( (](lp.gif) ![(
(](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
2.6.25 The mapping operation
|
|
Syntax | cmap 6550 |
Extend the definition of a class to include the mapping operation. (Read
for , "the set of all functions that map
from to
.)
|
![^m ^m](_hatm.gif) |
|
Syntax | cpm 6551 |
Extend the definition of a class to include the partial mapping operation.
(Read for , "the set of all partial functions
that map from
to .)
|
![^pm ^pm](_hatpm.gif) |
|
Definition | df-map 6552* |
Define the mapping operation or set exponentiation. The set of all
functions that map from to is
written ![( (](lp.gif) ![B B](_cb.gif) (see
mapval 6562). Many authors write followed by as a superscript
for this operation and rely on context to avoid confusion other
exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring]
p. 95). Other authors show as a prefixed superscript, which is
read " pre
" (e.g.,
definition of [Enderton] p. 52).
Definition 8.21 of [Eisenberg] p. 125
uses the notation Map( ,
) for our ![( (](lp.gif) ![B B](_cb.gif) . The up-arrow is used by
Donald Knuth
for iterated exponentiation (Science 194, 1235-1242, 1976). We
adopt
the first case of his notation (simple exponentiation) and subscript it
with m to distinguish it from other kinds of exponentiation.
(Contributed by NM, 8-Dec-2003.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![y y](_y.gif) ![--> -->](longrightarrow.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Definition | df-pm 6553* |
Define the partial mapping operation. A partial function from to
is a function
from a subset of to
. The set of all
partial functions from to is
written ![( (](lp.gif) ![B B](_cb.gif) (see
pmvalg 6561). A notation for this operation apparently
does not appear in
the literature. We use to distinguish it from the less general
set exponentiation operation (df-map 6552) . See mapsspm 6584 for
its relationship to set exponentiation. (Contributed by NM,
15-Nov-2007.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![{ {](lbrace.gif) ![~P ~P](scrp.gif) ![( (](lp.gif)
![x x](_x.gif)
![f f](_f.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | mapprc 6554* |
When is a proper
class, the class of all functions mapping
to is empty.
Exercise 4.41 of [Mendelson] p. 255.
(Contributed
by NM, 8-Dec-2003.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | pmex 6555* |
The class of all partial functions from one set to another is a set.
(Contributed by NM, 15-Nov-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | mapex 6556* |
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by Raph Levien,
4-Dec-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | fnmap 6557 |
Set exponentiation has a universal domain. (Contributed by NM,
8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
![( (](lp.gif) ![_V
_V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | fnpm 6558 |
Partial function exponentiation has a universal domain. (Contributed by
Mario Carneiro, 14-Nov-2013.)
|
![( (](lp.gif) ![_V
_V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | reldmmap 6559 |
Set exponentiation is a well-behaved binary operator. (Contributed by
Stefan O'Rear, 27-Feb-2015.)
|
![^m ^m](_hatm.gif) |
|
Theorem | mapvalg 6560* |
The value of set exponentiation. ![( (](lp.gif) ![B B](_cb.gif) is the set of all
functions that map from to .
Definition 10.24 of [Kunen]
p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![B B](_cb.gif)
![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | pmvalg 6561* |
The value of the partial mapping operation. ![( (](lp.gif)
![B B](_cb.gif) is the set
of all partial functions that map from to . (Contributed by
NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![B B](_cb.gif) ![{ {](lbrace.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![f f](_f.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | mapval 6562* |
The value of set exponentiation (inference version). ![( (](lp.gif) ![B B](_cb.gif) is
the set of all functions that map from to . Definition
10.24 of [Kunen] p. 24. (Contributed by
NM, 8-Dec-2003.)
|
![( (](lp.gif) ![B B](_cb.gif)
![{ {](lbrace.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![} }](rbrace.gif) |
|
Theorem | elmapg 6563 |
Membership relation for set exponentiation. (Contributed by NM,
17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![C C](_cc.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elmapd 6564 |
Deduction form of elmapg 6563. (Contributed by BJ, 11-Apr-2020.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapdm0 6565 |
The empty set is the only map with empty domain. (Contributed by Glauco
Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux,
3-Dec-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | elpmg 6566 |
The predicate "is a partial function." (Contributed by Mario
Carneiro,
14-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![(
(](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elpm2g 6567 |
The predicate "is a partial function." (Contributed by NM,
31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![F F](_cf.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elpm2r 6568 |
Sufficient condition for being a partial function. (Contributed by NM,
31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elpmi 6569 |
A partial function is a function. (Contributed by Mario Carneiro,
15-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![F F](_cf.gif) ![--> -->](longrightarrow.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pmfun 6570 |
A partial function is a function. (Contributed by Mario Carneiro,
30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | elmapex 6571 |
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | elmapi 6572 |
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | elmapfn 6573 |
A mapping is a function with the appropriate domain. (Contributed by AV,
6-Apr-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | elmapfun 6574 |
A mapping is always a function. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | elmapssres 6575 |
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fpmg 6576 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pmss12g 6577 |
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif)
![W W](_cw.gif) ![) )](rp.gif)
![( (](lp.gif) ![B
B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pmresg 6578 |
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elmap 6579 |
Membership relation for set exponentiation. (Contributed by NM,
8-Dec-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mapval2 6580* |
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3-Nov-2007.)
|
![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
|
Theorem | elpm 6581 |
The predicate "is a partial function." (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elpm2 6582 |
The predicate "is a partial function." (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![F F](_cf.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fpm 6583 |
A total function is a partial function. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsspm 6584 |
Set exponentiation is a subset of partial maps. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | pmsspw 6585 |
Partial maps are a subset of the power set of the Cartesian product of
its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
![( (](lp.gif) ![B B](_cb.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mapsspw 6586 |
Set exponentiation is a subset of the power set of the Cartesian product
of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![B B](_cb.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fvmptmap 6587* |
Special case of fvmpt 5506 for operator theorems. (Contributed by NM,
27-Nov-2007.)
|
![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![: :](colon.gif) ![D D](_cd.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | map0e 6588 |
Set exponentiation with an empty exponent (ordinal number 0) is ordinal
number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM,
10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
|
Theorem | map0b 6589 |
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
|
Theorem | map0g 6590 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by Mario
Carneiro, 30-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | map0 6591 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by NM,
10-Dec-2003.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsn 6592* |
The value of set exponentiation with a singleton exponent. Theorem 98
of [Suppes] p. 89. (Contributed by NM,
10-Dec-2003.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![} }](rbrace.gif) |
|
Theorem | mapss 6593 |
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fdiagfn 6594* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
![I I](_ci.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fvdiagfn 6595* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsnconst 6596 |
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | mapsncnv 6597* |
Expression for the inverse of the canonical map between a set and its
set of singleton functions. (Contributed by Stefan O'Rear,
21-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![x x](_x.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![`' `'](_cnv.gif)
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mapsnf1o2 6598* |
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![x x](_x.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) |
|
Theorem | mapsnf1o3 6599* |
Explicit bijection in the reverse of mapsnf1o2 6598. (Contributed by
Stefan O'Rear, 24-Mar-2015.)
|
![{ {](lbrace.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
2.6.26 Infinite Cartesian products
|
|
Syntax | cixp 6600 |
Extend class notation to include infinite Cartesian products.
|
![X_ X_](_bigtimes.gif) ![B B](_cb.gif) |