Theorem List for Intuitionistic Logic Explorer - 6001-6100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ofmresval 6001 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![o o](circ.gif) ![F F](subf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | off 6002* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![T T](_ct.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![U U](_cu.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-->
-->](longrightarrow.gif) ![T T](_ct.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![) )](rp.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![U U](_cu.gif) ![) )](rp.gif) |
|
Theorem | offeq 6003* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![T T](_ct.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![U U](_cu.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-->
-->](longrightarrow.gif) ![T T](_ct.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![C C](_cc.gif) ![--> -->](longrightarrow.gif) ![U U](_cu.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif)
![E E](_ce.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![R R](_cr.gif) ![E E](_ce.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif)
![H H](_ch.gif) ![) )](rp.gif) |
|
Theorem | ofres 6004 |
Restrict the operands of a function operation to the same domain as that
of the operation itself. (Contributed by Mario Carneiro,
15-Sep-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) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | offval2 6005* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.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) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ofrfval2 6006* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) ![A. A.](forall.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | suppssof1 6007* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![A A](_ca.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) ![A A](_ca.gif) ![: :](colon.gif) ![D D](_cd.gif) ![--> -->](longrightarrow.gif) ![V V](_cv.gif) ![( (](lp.gif)
![B B](_cb.gif) ![: :](colon.gif) ![D D](_cd.gif) ![-->
-->](longrightarrow.gif) ![R R](_cr.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![O O](_co.gif) ![B B](_cb.gif) ![) )](rp.gif) ![" "](backquote.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![Z Z](_cz.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![L L](_cl.gif) ![) )](rp.gif) |
|
Theorem | ofco 6008 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![D D](_cd.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![H H](_ch.gif)
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![( (](lp.gif) ![H H](_ch.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | offveqb 6009* |
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro,
5-Dec-2016.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif)
![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ofc12 6010 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caofref 6011* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![x x](_x.gif) ![R R](_cr.gif) ![x x](_x.gif) ![( (](lp.gif) ![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | caofinvl 6012* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![W W](_cw.gif) ![( (](lp.gif) ![N N](_cn.gif) ![: :](colon.gif) ![S S](_cs.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![( (](lp.gif)
![( (](lp.gif) ![N N](_cn.gif) ![` `](backtick.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![x x](_x.gif) ![B B](_cb.gif) ![( (](lp.gif)
![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![F F](_cf.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caofcom 6013* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![( (](lp.gif) ![y y](_y.gif) ![R R](_cr.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif)
![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caofrss 6014* |
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![x x](_x.gif) ![T T](_ct.gif) ![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) ![o o](circ.gif) ![R R](subr.gif) ![T T](_ct.gif) ![G G](_cg.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | caoftrn 6015* |
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif)
![G G](_cg.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![S S](_cs.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![T T](_ct.gif) ![z z](_z.gif) ![x x](_x.gif) ![U U](_cu.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![R R](subr.gif) ![R R](_cr.gif) ![o o](circ.gif) ![R R](subr.gif) ![T T](_ct.gif) ![H H](_ch.gif) ![o o](circ.gif) ![R R](subr.gif) ![U U](_cu.gif) ![H H](_ch.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
2.6.13 Functions (continued)
|
|
Theorem | resfunexgALT 6016 |
The restriction of a function to a set exists. Compare Proposition 6.17
of [TakeutiZaring] p. 28. This
version has a shorter proof than
resfunexg 5649 but requires ax-pow 4106 and ax-un 4363. (Contributed by NM,
7-Apr-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | cofunexg 6017 |
Existence of a composition when the first member is a function.
(Contributed by NM, 8-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | cofunex2g 6018 |
Existence of a composition when the second member is one-to-one.
(Contributed by NM, 8-Oct-2007.)
|
![( (](lp.gif) ![( (](lp.gif)
![`' `'](_cnv.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | fnexALT 6019 |
If the domain of a function is a set, the function is a set. Theorem
6.16(1) of [TakeutiZaring] p. 28.
This theorem is derived using the Axiom
of Replacement in the form of funimaexg 5215. This version of fnex 5650
uses
ax-pow 4106 and ax-un 4363, whereas fnex 5650
does not. (Contributed by NM,
14-Aug-1994.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | funrnex 6020 |
If the domain of a function exists, so does its range. Part of Theorem
4.15(v) of [Monk1] p. 46. This theorem is
derived using the Axiom of
Replacement in the form of funex 5651. (Contributed by NM, 11-Nov-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fornex 6021 |
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23-Jul-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | f1dmex 6022 |
If the codomain of a one-to-one function exists, so does its domain. This
can be thought of as a form of the Axiom of Replacement. (Contributed by
NM, 4-Sep-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![C C](_cc.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | abrexex 6023* |
Existence of a class abstraction of existentially restricted sets.
is normally a free-variable parameter in the class expression
substituted for , which can be thought of as ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) . This
simple-looking theorem is actually quite powerful and appears to involve
the Axiom of Replacement in an intrinsic way, as can be seen by tracing
back through the path mptexg 5653, funex 5651, fnex 5650, resfunexg 5649, and
funimaexg 5215. See also abrexex2 6030. (Contributed by NM, 16-Oct-2003.)
(Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
![{ {](lbrace.gif) ![E.
E.](exists.gif)
![B B](_cb.gif) ![_V _V](rmcv.gif) |
|
Theorem | abrexexg 6024* |
Existence of a class abstraction of existentially restricted sets.
is normally a free-variable parameter in . The antecedent assures
us that is a
set. (Contributed by NM, 3-Nov-2003.)
|
![( (](lp.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif)
![B B](_cb.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | iunexg 6025* |
The existence of an indexed union. is normally a free-variable
parameter in .
(Contributed by NM, 23-Mar-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![W W](_cw.gif) ![U_ U_](_cupbar.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | abrexex2g 6026* |
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![ph
ph](_varphi.gif)
![W W](_cw.gif) ![{ {](lbrace.gif) ![E.
E.](exists.gif) ![ph ph](_varphi.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | opabex3d 6027* |
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19-Oct-2017.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![{ {](lbrace.gif) ![ps ps](_psi.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | opabex3 6028* |
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif)
![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![_V _V](rmcv.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif)
![_V _V](rmcv.gif) |
|
Theorem | iunex 6029* |
The existence of an indexed union. is normally a free-variable
parameter in the class expression substituted for , which can be
read informally as ![B B](_cb.gif) ![( (](lp.gif) ![x x](_x.gif) . (Contributed by NM, 13-Oct-2003.)
|
![U_ U_](_cupbar.gif)
![_V _V](rmcv.gif) |
|
Theorem | abrexex2 6030* |
Existence of an existentially restricted class abstraction. is
normally has free-variable parameters and . See also
abrexex 6023. (Contributed by NM, 12-Sep-2004.)
|
![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![_V _V](rmcv.gif) |
|
Theorem | abexssex 6031* |
Existence of a class abstraction with an existentially quantified
expression. Both and can be
free in .
(Contributed
by NM, 29-Jul-2006.)
|
![{ {](lbrace.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![( (](lp.gif) ![ph ph](_varphi.gif) ![) )](rp.gif)
![_V _V](rmcv.gif) |
|
Theorem | abexex 6032* |
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4-Mar-2007.)
|
![( (](lp.gif) ![A A](_ca.gif) ![{
{](lbrace.gif) ![ph ph](_varphi.gif) ![{
{](lbrace.gif) ![E. E.](exists.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) ![_V _V](rmcv.gif) |
|
Theorem | oprabexd 6033* |
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![E* E*](_em1.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![( (](lp.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)
![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | oprabex 6034* |
Existence of an operation class abstraction. (Contributed by NM,
19-Oct-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![E* E*](_em1.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)
![B B](_cb.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![_V _V](rmcv.gif) |
|
Theorem | oprabex3 6035* |
Existence of an operation class abstraction (special case).
(Contributed by NM, 19-Oct-2004.)
|
![{ {](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) ![_V _V](rmcv.gif) |
|
Theorem | oprabrexex2 6036* |
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.)
|
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif)
![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif)
![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![_V _V](rmcv.gif) |
|
Theorem | ab2rexex 6037* |
Existence of a class abstraction of existentially restricted sets.
Variables and
are normally
free-variable parameters in the
class expression substituted for , which can be thought of as
![C C](_cc.gif) ![( (](lp.gif) ![x x](_x.gif) ![y y](_y.gif) . See comments for abrexex 6023. (Contributed by NM,
20-Sep-2011.)
|
![{
{](lbrace.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![C C](_cc.gif)
![_V _V](rmcv.gif) |
|
Theorem | ab2rexex2 6038* |
Existence of an existentially restricted class abstraction.
normally has free-variable parameters , , and .
Compare abrexex2 6030. (Contributed by NM, 20-Sep-2011.)
|
![{ {](lbrace.gif) ![ph
ph](_varphi.gif)
![{ {](lbrace.gif) ![E. E.](exists.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![_V _V](rmcv.gif) |
|
Theorem | xpexgALT 6039 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4661 for a version that uses the Power Set axiom
instead.
(Contributed by Mario Carneiro, 20-May-2013.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![B B](_cb.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | offval3 6040* |
General value of ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) with no assumptions on functionality
of and . (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | offres 6041 |
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![G G](_cg.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | ofmres 6042* |
Equivalent expressions for a restriction of the function operation map.
Unlike ![o o](circ.gif) ![F F](subf.gif) which is a proper class, ![o o](circ.gif) ![F F](subf.gif) ![( (](lp.gif)
![B B](_cb.gif) ![)
)](rp.gif) can
be a set by ofmresex 6043, allowing it to be used as a function or
structure argument. By ofmresval 6001, the restricted operation map
values are the same as the original values, allowing theorems for
![o o](circ.gif) ![F F](subf.gif) to be reused. (Contributed by NM, 20-Oct-2014.)
|
![o o](circ.gif) ![F F](subf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![R R](_cr.gif) ![g g](_g.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ofmresex 6043 |
Existence of a restriction of the function operation map. (Contributed
by NM, 20-Oct-2014.)
|
![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![o o](circ.gif) ![F F](subf.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
2.6.14 First and second members of an ordered
pair
|
|
Syntax | c1st 6044 |
Extend the definition of a class to include the first member an ordered
pair function.
|
![1st 1st](_1st.gif) |
|
Syntax | c2nd 6045 |
Extend the definition of a class to include the second member an ordered
pair function.
|
![2nd 2nd](_2nd.gif) |
|
Definition | df-1st 6046 |
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6052 proves that it does this. For example,
(![1st 1st](_1st.gif) ![` `](backtick.gif) 3 , 4 ) = 3 . Equivalent to Definition
5.13 (i) of
[Monk1] p. 52 (compare op1sta 5028 and op1stb 4407). The notation is the same
as Monk's. (Contributed by NM, 9-Oct-2004.)
|
![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Definition | df-2nd 6047 |
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6053 proves that it does this. For example,
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) 3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 5031 and op2ndb 5030). The notation is the
same as Monk's. (Contributed by NM, 9-Oct-2004.)
|
![( (](lp.gif) ![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![x x](_x.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | 1stvalg 6048 |
The value of the function that extracts the first member of an ordered
pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | 2ndvalg 6049 |
The value of the function that extracts the second member of an ordered
pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![U. U.](bigcup.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | 1st0 6050 |
The value of the first-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) |
|
Theorem | 2nd0 6051 |
The value of the second-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![(/) (/)](varnothing.gif) ![(/) (/)](varnothing.gif) |
|
Theorem | op1st 6052 |
Extract the first member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![A A](_ca.gif) |
|
Theorem | op2nd 6053 |
Extract the second member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![B B](_cb.gif) |
|
Theorem | op1std 6054 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | op2ndd 6055 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | op1stg 6056 |
Extract the first member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | op2ndg 6057 |
Extract the second member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ot1stg 6058 |
Extract the first member of an ordered triple. (Due to infrequent
usage, it isn't worthwhile at this point to define special extractors
for triples, so we reuse the ordered pair extractors for ot1stg 6058,
ot2ndg 6059, ot3rdgg 6060.) (Contributed by NM, 3-Apr-2015.) (Revised
by
Mario Carneiro, 2-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ot2ndg 6059 |
Extract the second member of an ordered triple. (See ot1stg 6058 comment.)
(Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro,
2-May-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ot3rdgg 6060 |
Extract the third member of an ordered triple. (See ot1stg 6058 comment.)
(Contributed by NM, 3-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![>. >.](rangle.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 1stval2 6061 |
Alternate value of the function that extracts the first member of an
ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by
NM, 18-Aug-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![|^| |^|](bigcap.gif) ![|^| |^|](bigcap.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | 2ndval2 6062 |
Alternate value of the function that extracts the second member of an
ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by
NM, 18-Aug-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![|^| |^|](bigcap.gif) ![|^| |^|](bigcap.gif) ![|^| |^|](bigcap.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | fo1st 6063 |
The function
maps the universe onto the universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
![1st
1st](_1st.gif) ![: :](colon.gif) ![_V _V](rmcv.gif) ![-onto-> -onto->](onto.gif) ![_V _V](rmcv.gif) |
|
Theorem | fo2nd 6064 |
The function
maps the universe onto the universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
![2nd
2nd](_2nd.gif) ![: :](colon.gif) ![_V _V](rmcv.gif) ![-onto-> -onto->](onto.gif) ![_V _V](rmcv.gif) |
|
Theorem | f1stres 6065 |
Mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A A](_ca.gif) |
|
Theorem | f2ndres 6066 |
Mapping of a restriction of the (second member of an ordered
pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) |
|
Theorem | fo1stresm 6067* |
Onto mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-onto-> -onto->](onto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fo2ndresm 6068* |
Onto mapping of a restriction of the (second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![-onto-> -onto->](onto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | 1stcof 6069 |
Composition of the first member function with another function.
(Contributed by NM, 12-Oct-2007.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | 2ndcof 6070 |
Composition of the second member function with another function.
(Contributed by FL, 15-Oct-2012.)
|
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | xp1st 6071 |
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | xp2nd 6072 |
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | 1stexg 6073 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | 2ndexg 6074 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | elxp6 6075 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5034. (Contributed by NM, 9-Oct-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elxp7 6076 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5034. (Contributed by NM, 19-Aug-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | oprssdmm 6077* |
Domain of closure of an operation. (Contributed by Jim Kingdon,
23-Oct-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif) ![E. E.](exists.gif)
![u u](_u.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)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![S S](_cs.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | eqopi 6078 |
Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.)
(Revised by Mario Carneiro, 23-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | xp2 6079* |
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16-Sep-2006.)
|
![( (](lp.gif) ![B B](_cb.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![_V _V](rmcv.gif)
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | unielxp 6080 |
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16-Sep-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![U. U.](bigcup.gif)
![U. U.](bigcup.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 1st2nd2 6081 |
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20-Oct-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![<. <.](langle.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | xpopth 6082 |
An ordered pair theorem for members of cross products. (Contributed by
NM, 20-Jun-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![S S](_cs.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![`
`](backtick.gif) ![B B](_cb.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqop 6083 |
Two ways to express equality with an ordered pair. (Contributed by NM,
3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif)
![<. <.](langle.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | eqop2 6084 |
Two ways to express equality with an ordered pair. (Contributed by NM,
25-Feb-2014.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![`
`](backtick.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | op1steq 6085* |
Two ways of expressing that an element is the first member of an ordered
pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro,
23-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![E. E.](exists.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![x x](_x.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2nd1st 6086 |
Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![U. U.](bigcup.gif) ![`' `'](_cnv.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | 1st2nd 6087 |
Reconstruction of a member of a relation in terms of its ordered pair
components. (Contributed by NM, 29-Aug-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
|
Theorem | 1stdm 6088 |
The first ordered pair component of a member of a relation belongs to the
domain of the relation. (Contributed by NM, 17-Sep-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | 2ndrn 6089 |
The second ordered pair component of a member of a relation belongs to the
range of the relation. (Contributed by NM, 17-Sep-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | 1st2ndbr 6090 |
Express an element of a relation as a relationship between first and
second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | releldm2 6091* |
Two ways of expressing membership in the domain of a relation.
(Contributed by NM, 22-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | reldm 6092* |
An expression for the domain of a relation. (Contributed by NM,
22-Sep-2013.)
|
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | sbcopeq1a 6093 |
Equality theorem for substitution of a class for an ordered pair (analog
of sbceq1a 2922 that avoids the existential quantifiers of copsexg 4174).
(Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | csbopeq1a 6094 |
Equality theorem for substitution of a class for an ordered pair
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif)
in (analog of csbeq1a 3016). (Contributed by NM,
19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![y y](_y.gif) ![]_ ]_](_urbrack.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | dfopab2 6095* |
A way to define an ordered-pair class abstraction without using
existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
![{
{](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![_V _V](rmcv.gif) ![[.
[.](_dlbrack.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![z z](_z.gif)
![x x](_x.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![z z](_z.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![} }](rbrace.gif) |
|
Theorem | dfoprab3s 6096* |
A way to define an operation class abstraction without using existential
quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario
Carneiro, 31-Aug-2015.)
|
![{
{](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ph ph](_varphi.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![w w](_w.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![w w](_w.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | dfoprab3 6097* |
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 16-Dec-2008.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif)
![ph ph](_varphi.gif) ![) )](rp.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![ps ps](_psi.gif) ![} }](rbrace.gif) |
|
Theorem | dfoprab4 6098* |
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
![( (](lp.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![ph ph](_varphi.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) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | dfoprab4f 6099* |
Operation class abstraction expressed without existential quantifiers.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19-Jun-2012.) (Contributed by NM, 20-Dec-2008.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
![F/
F/](finv.gif) ![x x](_x.gif) ![F/ F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif)
![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![w w](_w.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![ph ph](_varphi.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) ![B B](_cb.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![} }](rbrace.gif) |
|
Theorem | dfxp3 6100* |
Define the cross product of three classes. Compare df-xp 4553.
(Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro,
3-Nov-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![z z](_z.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![} }](rbrace.gif) |