Type | Label | Description |
Statement |
|
Theorem | nfof 6101 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
ā¢ ā²š„š
ā ā¢ ā²š„ āš
š
|
|
Theorem | nfofr 6102 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
ā¢ ā²š„š
ā ā¢ ā²š„ āš
š
|
|
Theorem | offval 6103* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn šµ)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š
& ⢠((š ā§ š„ ā š“) ā (š¹āš„) = š¶)
& ⢠((š ā§ š„ ā šµ) ā (šŗāš„) = š·) ā ⢠(š ā (š¹ āš š
šŗ) = (š„ ā š ⦠(š¶š
š·))) |
|
Theorem | ofrfval 6104* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn šµ)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š
& ⢠((š ā§ š„ ā š“) ā (š¹āš„) = š¶)
& ⢠((š ā§ š„ ā šµ) ā (šŗāš„) = š·) ā ⢠(š ā (š¹ āš š
šŗ ā āš„ ā š š¶š
š·)) |
|
Theorem | ofvalg 6105 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn šµ)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š
& ⢠((š ā§ š ā š“) ā (š¹āš) = š¶)
& ⢠((š ā§ š ā šµ) ā (šŗāš) = š·)
& ⢠((š ā§ š ā š) ā (š¶š
š·) ā š) ā ⢠((š ā§ š ā š) ā ((š¹ āš š
šŗ)āš) = (š¶š
š·)) |
|
Theorem | ofrval 6106 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn šµ)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š
& ⢠((š ā§ š ā š“) ā (š¹āš) = š¶)
& ⢠((š ā§ š ā šµ) ā (šŗāš) = š·) ā ⢠((š ā§ š¹ āš š
šŗ ā§ š ā š) ā š¶š
š·) |
|
Theorem | ofmresval 6107 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
⢠(š ā š¹ ā š“)
& ⢠(š ā šŗ ā šµ) ā ⢠(š ā (š¹( āš š
ā¾ (š“ Ć šµ))šŗ) = (š¹ āš š
šŗ)) |
|
Theorem | off 6108* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⢠((š ā§ (š„ ā š ā§ š¦ ā š)) ā (š„š
š¦) ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠(š ā šŗ:šµā¶š)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š¶ ā ⢠(š ā (š¹ āš š
šŗ):š¶ā¶š) |
|
Theorem | offeq 6109* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
⢠((š ā§ (š„ ā š ā§ š¦ ā š)) ā (š„š
š¦) ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠(š ā šŗ:šµā¶š)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š¶
& ⢠(š ā š»:š¶ā¶š)
& ⢠((š ā§ š„ ā š“) ā (š¹āš„) = š·)
& ⢠((š ā§ š„ ā šµ) ā (šŗāš„) = šø)
& ⢠((š ā§ š„ ā š¶) ā (š·š
šø) = (š»āš„)) ā ⢠(š ā (š¹ āš š
šŗ) = š») |
|
Theorem | ofres 6110 |
Restrict the operands of a function operation to the same domain as that
of the operation itself. (Contributed by Mario Carneiro,
15-Sep-2014.)
|
⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn šµ)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š“ ā© šµ) = š¶ ā ⢠(š ā (š¹ āš š
šŗ) = ((š¹ ā¾ š¶) āš š
(šŗ ā¾ š¶))) |
|
Theorem | offval2 6111* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠((š ā§ š„ ā š“) ā šµ ā š)
& ⢠((š ā§ š„ ā š“) ā š¶ ā š)
& ⢠(š ā š¹ = (š„ ā š“ ⦠šµ)) & ⢠(š ā šŗ = (š„ ā š“ ⦠š¶)) ā ⢠(š ā (š¹ āš š
šŗ) = (š„ ā š“ ⦠(šµš
š¶))) |
|
Theorem | ofrfval2 6112* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠((š ā§ š„ ā š“) ā šµ ā š)
& ⢠((š ā§ š„ ā š“) ā š¶ ā š)
& ⢠(š ā š¹ = (š„ ā š“ ⦠šµ)) & ⢠(š ā šŗ = (š„ ā š“ ⦠š¶)) ā ⢠(š ā (š¹ āš š
šŗ ā āš„ ā š“ šµš
š¶)) |
|
Theorem | suppssof1 6113* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⢠(š ā (ā”š“ ā (V ā {š})) ā šæ)
& ⢠((š ā§ š£ ā š
) ā (ššš£) = š)
& ⢠(š ā š“:š·ā¶š)
& ⢠(š ā šµ:š·ā¶š
)
& ⢠(š ā š· ā š) ā ⢠(š ā (ā”(š“ āš ššµ) ā (V ā {š})) ā šæ) |
|
Theorem | ofco 6114 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn šµ)
& ⢠(š ā š»:š·ā¶š¶)
& ⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š ā š· ā š)
& ⢠(š“ ā© šµ) = š¶ ā ⢠(š ā ((š¹ āš š
šŗ) ā š») = ((š¹ ā š») āš š
(šŗ ā š»))) |
|
Theorem | offveqb 6115* |
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro,
5-Dec-2016.)
|
⢠(š ā š“ ā š)
& ⢠(š ā š¹ Fn š“)
& ⢠(š ā šŗ Fn š“)
& ⢠(š ā š» Fn š“)
& ⢠((š ā§ š„ ā š“) ā (š¹āš„) = šµ)
& ⢠((š ā§ š„ ā š“) ā (šŗāš„) = š¶) ā ⢠(š ā (š» = (š¹ āš š
šŗ) ā āš„ ā š“ (š»āš„) = (šµš
š¶))) |
|
Theorem | ofc12 6116 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š)
& ⢠(š ā š¶ ā š) ā ⢠(š ā ((š“ Ć {šµ}) āš š
(š“ Ć {š¶})) = (š“ Ć {(šµš
š¶)})) |
|
Theorem | caofref 6117* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠((š ā§ š„ ā š) ā š„š
š„) ā ⢠(š ā š¹ āš š
š¹) |
|
Theorem | caofinvl 6118* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠(š ā šµ ā š)
& ⢠(š ā š:šā¶š)
& ⢠(š ā šŗ = (š£ ā š“ ⦠(šā(š¹āš£)))) & ⢠((š ā§ š„ ā š) ā ((šāš„)š
š„) = šµ) ā ⢠(š ā (šŗ āš š
š¹) = (š“ Ć {šµ})) |
|
Theorem | caofcom 6119* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠(š ā šŗ:š“ā¶š)
& ⢠((š ā§ (š„ ā š ā§ š¦ ā š)) ā (š„š
š¦) = (š¦š
š„)) ā ⢠(š ā (š¹ āš š
šŗ) = (šŗ āš š
š¹)) |
|
Theorem | caofrss 6120* |
Transfer a relation subset law to the function relation. (Contributed
by Mario Carneiro, 28-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠(š ā šŗ:š“ā¶š)
& ⢠((š ā§ (š„ ā š ā§ š¦ ā š)) ā (š„š
š¦ ā š„šš¦)) ā ⢠(š ā (š¹ āš š
šŗ ā š¹ āš ššŗ)) |
|
Theorem | caoftrn 6121* |
Transfer a transitivity law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā š¹:š“ā¶š)
& ⢠(š ā šŗ:š“ā¶š)
& ⢠(š ā š»:š“ā¶š)
& ⢠((š ā§ (š„ ā š ā§ š¦ ā š ā§ š§ ā š)) ā ((š„š
š¦ ā§ š¦šš§) ā š„šš§)) ā ⢠(š ā ((š¹ āš š
šŗ ā§ šŗ āš šš») ā š¹ āš šš»)) |
|
2.6.14 Functions (continued)
|
|
Theorem | resfunexgALT 6122 |
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 5750 but requires ax-pow 4186 and ax-un 4445. (Contributed by NM,
7-Apr-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⢠((Fun š“ ā§ šµ ā š¶) ā (š“ ā¾ šµ) ā V) |
|
Theorem | cofunexg 6123 |
Existence of a composition when the first member is a function.
(Contributed by NM, 8-Oct-2007.)
|
⢠((Fun š“ ā§ šµ ā š¶) ā (š“ ā šµ) ā V) |
|
Theorem | cofunex2g 6124 |
Existence of a composition when the second member is one-to-one.
(Contributed by NM, 8-Oct-2007.)
|
⢠((š“ ā š ā§ Fun ā”šµ) ā (š“ ā šµ) ā V) |
|
Theorem | fnexALT 6125 |
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 5312. This version of fnex 5751
uses
ax-pow 4186 and ax-un 4445, whereas fnex 5751
does not. (Contributed by NM,
14-Aug-1994.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⢠((š¹ Fn š“ ā§ š“ ā šµ) ā š¹ ā V) |
|
Theorem | funexw 6126 |
Weak version of funex 5752 that holds without ax-coll 4130. If the domain and
codomain of a function exist, so does the function. (Contributed by Rohan
Ridenour, 13-Aug-2023.)
|
⢠((Fun š¹ ā§ dom š¹ ā šµ ā§ ran š¹ ā š¶) ā š¹ ā V) |
|
Theorem | mptexw 6127* |
Weak version of mptex 5755 that holds without ax-coll 4130. If the domain
and codomain of a function given by maps-to notation are sets, the
function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|
⢠š“ ā V & ⢠š¶ ā V & ā¢ āš„ ā š“ šµ ā š¶ ā ⢠(š„ ā š“ ⦠šµ) ā V |
|
Theorem | funrnex 6128 |
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 5752. (Contributed by NM, 11-Nov-1995.)
|
⢠(dom š¹ ā šµ ā (Fun š¹ ā ran š¹ ā V)) |
|
Theorem | focdmex 6129 |
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23-Jul-2004.)
|
⢠(š“ ā š¶ ā (š¹:š“āontoāšµ ā šµ ā V)) |
|
Theorem | f1dmex 6130 |
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.)
|
⢠((š¹:š“ā1-1āšµ ā§ šµ ā š¶) ā š“ ā V) |
|
Theorem | abrexex 6131* |
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 šµ(š„). 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 5754, funex 5752, fnex 5751, resfunexg 5750, and
funimaexg 5312. See also abrexex2 6138. (Contributed by NM, 16-Oct-2003.)
(Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
⢠š“ ā V ā ⢠{š¦ ā£ āš„ ā š“ š¦ = šµ} ā V |
|
Theorem | abrexexg 6132* |
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.)
|
⢠(š“ ā š ā {š¦ ā£ āš„ ā š“ š¦ = šµ} ā V) |
|
Theorem | iunexg 6133* |
The existence of an indexed union. š„ is normally a free-variable
parameter in šµ. (Contributed by NM, 23-Mar-2006.)
|
⢠((š“ ā š ā§ āš„ ā š“ šµ ā š) ā āŖ š„ ā š“ šµ ā V) |
|
Theorem | abrexex2g 6134* |
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⢠((š“ ā š ā§ āš„ ā š“ {š¦ ⣠š} ā š) ā {š¦ ā£ āš„ ā š“ š} ā V) |
|
Theorem | opabex3d 6135* |
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19-Oct-2017.)
|
⢠(š ā š“ ā V) & ⢠((š ā§ š„ ā š“) ā {š¦ ⣠š} ā V) ā ⢠(š ā {āØš„, š¦ā© ⣠(š„ ā š“ ā§ š)} ā V) |
|
Theorem | opabex3 6136* |
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⢠š“ ā V & ⢠(š„ ā š“ ā {š¦ ⣠š} ā V) ā ⢠{āØš„, š¦ā© ⣠(š„ ā š“ ā§ š)} ā V |
|
Theorem | iunex 6137* |
The existence of an indexed union. š„ is normally a free-variable
parameter in the class expression substituted for šµ, which can be
read informally as šµ(š„). (Contributed by NM, 13-Oct-2003.)
|
⢠š“ ā V & ⢠šµ ā
V ā ⢠⪠š„ ā š“ šµ ā V |
|
Theorem | abrexex2 6138* |
Existence of an existentially restricted class abstraction. š is
normally has free-variable parameters š„ and š¦. See
also
abrexex 6131. (Contributed by NM, 12-Sep-2004.)
|
⢠š“ ā V & ⢠{š¦ ⣠š} ā V ā ⢠{š¦ ā£ āš„ ā š“ š} ā V |
|
Theorem | abexssex 6139* |
Existence of a class abstraction with an existentially quantified
expression. Both š„ and š¦ can be free in š.
(Contributed
by NM, 29-Jul-2006.)
|
⢠š“ ā V & ⢠{š¦ ⣠š} ā V ā ⢠{š¦ ā£ āš„(š„ ā š“ ā§ š)} ā V |
|
Theorem | abexex 6140* |
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4-Mar-2007.)
|
⢠š“ ā V & ⢠(š ā š„ ā š“)
& ⢠{š¦ ⣠š} ā V ā ⢠{š¦ ā£ āš„š} ā V |
|
Theorem | oprabexd 6141* |
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⢠(š ā š“ ā V) & ⢠(š ā šµ ā V) & ⢠((š ā§ (š„ ā š“ ā§ š¦ ā šµ)) ā ā*š§š)
& ⢠(š ā š¹ = {āØāØš„, š¦ā©, š§ā© ⣠((š„ ā š“ ā§ š¦ ā šµ) ā§ š)}) ā ⢠(š ā š¹ ā V) |
|
Theorem | oprabex 6142* |
Existence of an operation class abstraction. (Contributed by NM,
19-Oct-2004.)
|
⢠š“ ā V & ⢠šµ ā V & ⢠((š„ ā š“ ā§ š¦ ā šµ) ā ā*š§š)
& ⢠š¹ = {āØāØš„, š¦ā©, š§ā© ⣠((š„ ā š“ ā§ š¦ ā šµ) ā§ š)} ā ⢠š¹ ā V |
|
Theorem | oprabex3 6143* |
Existence of an operation class abstraction (special case).
(Contributed by NM, 19-Oct-2004.)
|
⢠š» ā V & ⢠š¹ = {āØāØš„, š¦ā©, š§ā© ⣠((š„ ā (š» Ć š») ā§ š¦ ā (š» Ć š»)) ā§ āš¤āš£āš¢āš((š„ = āØš¤, š£ā© ā§ š¦ = āØš¢, šā©) ā§ š§ = š
))} ā ⢠š¹ ā V |
|
Theorem | oprabrexex2 6144* |
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.)
|
⢠š“ ā V & ā¢
{āØāØš„,
š¦ā©, š§ā© ⣠š} ā V ā ⢠{āØāØš„, š¦ā©, š§ā© ā£ āš¤ ā š“ š} ā V |
|
Theorem | ab2rexex 6145* |
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
š¶(š„, š¦). See comments for abrexex 6131. (Contributed by NM,
20-Sep-2011.)
|
⢠š“ ā V & ⢠šµ ā
V ā ⢠{š§ ā£ āš„ ā š“ āš¦ ā šµ š§ = š¶} ā V |
|
Theorem | ab2rexex2 6146* |
Existence of an existentially restricted class abstraction. š
normally has free-variable parameters š„, š¦, and š§.
Compare abrexex2 6138. (Contributed by NM, 20-Sep-2011.)
|
⢠š“ ā V & ⢠šµ ā V & ⢠{š§ ⣠š} ā V ā ⢠{š§ ā£ āš„ ā š“ āš¦ ā šµ š} ā V |
|
Theorem | xpexgALT 6147 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4752 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.)
|
⢠((š“ ā š ā§ šµ ā š) ā (š“ Ć šµ) ā V) |
|
Theorem | offval3 6148* |
General value of (š¹ āš š
šŗ) with no assumptions on
functionality
of š¹ and šŗ. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⢠((š¹ ā š ā§ šŗ ā š) ā (š¹ āš š
šŗ) = (š„ ā (dom š¹ ā© dom šŗ) ⦠((š¹āš„)š
(šŗāš„)))) |
|
Theorem | offres 6149 |
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⢠((š¹ ā š ā§ šŗ ā š) ā ((š¹ āš š
šŗ) ā¾ š·) = ((š¹ ā¾ š·) āš š
(šŗ ā¾ š·))) |
|
Theorem | ofmres 6150* |
Equivalent expressions for a restriction of the function operation map.
Unlike āš š
which is a proper class, ( āš š
ā¾ (š“ Ć šµ)) can
be a set by ofmresex 6151, allowing it to be used as a function or
structure argument. By ofmresval 6107, the restricted operation map
values are the same as the original values, allowing theorems for
āš š
to be reused. (Contributed by NM,
20-Oct-2014.)
|
⢠( āš š
ā¾ (š“ Ć šµ)) = (š ā š“, š ā šµ ⦠(š āš š
š)) |
|
Theorem | ofmresex 6151 |
Existence of a restriction of the function operation map. (Contributed
by NM, 20-Oct-2014.)
|
⢠(š ā š“ ā š)
& ⢠(š ā šµ ā š) ā ⢠(š ā ( āš š
ā¾ (š“ Ć šµ)) ā V) |
|
2.6.15 First and second members of an ordered
pair
|
|
Syntax | c1st 6152 |
Extend the definition of a class to include the first member an ordered
pair function.
|
class 1st |
|
Syntax | c2nd 6153 |
Extend the definition of a class to include the second member an ordered
pair function.
|
class 2nd |
|
Definition | df-1st 6154 |
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6160 proves that it does this. For example,
(1st ā⨠3 , 4 ā©) = 3 . Equivalent to Definition 5.13 (i) of
[Monk1] p. 52 (compare op1sta 5122 and op1stb 4490). The notation is the same
as Monk's. (Contributed by NM, 9-Oct-2004.)
|
⢠1st = (š„ ā V ⦠⪠dom {š„}) |
|
Definition | df-2nd 6155 |
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6161 proves that it does this. For example,
(2nd ā⨠3 , 4 ā©) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 5125 and op2ndb 5124). The notation is the
same as Monk's. (Contributed by NM, 9-Oct-2004.)
|
⢠2nd = (š„ ā V ⦠⪠ran {š„}) |
|
Theorem | 1stvalg 6156 |
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.)
|
⢠(š“ ā V ā (1st
āš“) = āŖ dom {š“}) |
|
Theorem | 2ndvalg 6157 |
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.)
|
⢠(š“ ā V ā (2nd
āš“) = āŖ ran {š“}) |
|
Theorem | 1st0 6158 |
The value of the first-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
⢠(1st āā
) =
ā
|
|
Theorem | 2nd0 6159 |
The value of the second-member function at the empty set. (Contributed by
NM, 23-Apr-2007.)
|
⢠(2nd āā
) =
ā
|
|
Theorem | op1st 6160 |
Extract the first member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
⢠š“ ā V & ⢠šµ ā
V ā ⢠(1st
āāØš“, šµā©) = š“ |
|
Theorem | op2nd 6161 |
Extract the second member of an ordered pair. (Contributed by NM,
5-Oct-2004.)
|
⢠š“ ā V & ⢠šµ ā
V ā ⢠(2nd
āāØš“, šµā©) = šµ |
|
Theorem | op1std 6162 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⢠š“ ā V & ⢠šµ ā
V ā ⢠(š¶ = āØš“, šµā© ā (1st āš¶) = š“) |
|
Theorem | op2ndd 6163 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⢠š“ ā V & ⢠šµ ā
V ā ⢠(š¶ = āØš“, šµā© ā (2nd āš¶) = šµ) |
|
Theorem | op1stg 6164 |
Extract the first member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
⢠((š“ ā š ā§ šµ ā š) ā (1st āāØš“, šµā©) = š“) |
|
Theorem | op2ndg 6165 |
Extract the second member of an ordered pair. (Contributed by NM,
19-Jul-2005.)
|
⢠((š“ ā š ā§ šµ ā š) ā (2nd āāØš“, šµā©) = šµ) |
|
Theorem | ot1stg 6166 |
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 6166,
ot2ndg 6167, ot3rdgg 6168.) (Contributed by NM, 3-Apr-2015.) (Revised
by
Mario Carneiro, 2-May-2015.)
|
⢠((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (1st
ā(1st āāØš“, šµ, š¶ā©)) = š“) |
|
Theorem | ot2ndg 6167 |
Extract the second member of an ordered triple. (See ot1stg 6166 comment.)
(Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro,
2-May-2015.)
|
⢠((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (2nd
ā(1st āāØš“, šµ, š¶ā©)) = šµ) |
|
Theorem | ot3rdgg 6168 |
Extract the third member of an ordered triple. (See ot1stg 6166 comment.)
(Contributed by NM, 3-Apr-2015.)
|
⢠((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (2nd āāØš“, šµ, š¶ā©) = š¶) |
|
Theorem | 1stval2 6169 |
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.)
|
⢠(š“ ā (V Ć V) ā
(1st āš“)
= ā© ā© š“) |
|
Theorem | 2ndval2 6170 |
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.)
|
⢠(š“ ā (V Ć V) ā
(2nd āš“)
= ā© ā© ā© ā”{š“}) |
|
Theorem | fo1st 6171 |
The 1st function maps the universe onto the
universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⢠1st :VāontoāV |
|
Theorem | fo2nd 6172 |
The 2nd function maps the universe onto the
universe. (Contributed
by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⢠2nd :VāontoāV |
|
Theorem | f1stres 6173 |
Mapping of a restriction of the 1st (first
member of an ordered
pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
⢠(1st ā¾ (š“ Ć šµ)):(š“ Ć šµ)ā¶š“ |
|
Theorem | f2ndres 6174 |
Mapping of a restriction of the 2nd (second
member of an ordered
pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario
Carneiro, 8-Sep-2013.)
|
⢠(2nd ā¾ (š“ Ć šµ)):(š“ Ć šµ)ā¶šµ |
|
Theorem | fo1stresm 6175* |
Onto mapping of a restriction of the 1st
(first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
⢠(āš¦ š¦ ā šµ ā (1st ā¾ (š“ Ć šµ)):(š“ Ć šµ)āontoāš“) |
|
Theorem | fo2ndresm 6176* |
Onto mapping of a restriction of the 2nd
(second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|
⢠(āš„ š„ ā š“ ā (2nd ā¾ (š“ Ć šµ)):(š“ Ć šµ)āontoāšµ) |
|
Theorem | 1stcof 6177 |
Composition of the first member function with another function.
(Contributed by NM, 12-Oct-2007.)
|
⢠(š¹:š“ā¶(šµ Ć š¶) ā (1st ā š¹):š“ā¶šµ) |
|
Theorem | 2ndcof 6178 |
Composition of the second member function with another function.
(Contributed by FL, 15-Oct-2012.)
|
⢠(š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹):š“ā¶š¶) |
|
Theorem | xp1st 6179 |
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⢠(š“ ā (šµ Ć š¶) ā (1st āš“) ā šµ) |
|
Theorem | xp2nd 6180 |
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⢠(š“ ā (šµ Ć š¶) ā (2nd āš“) ā š¶) |
|
Theorem | 1stexg 6181 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
⢠(š“ ā š ā (1st āš“) ā V) |
|
Theorem | 2ndexg 6182 |
Existence of the first member of a set. (Contributed by Jim Kingdon,
26-Jan-2019.)
|
⢠(š“ ā š ā (2nd āš“) ā V) |
|
Theorem | elxp6 6183 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5128. (Contributed by NM, 9-Oct-2004.)
|
⢠(š“ ā (šµ Ć š¶) ā (š“ = āØ(1st āš“), (2nd āš“)ā© ā§ ((1st
āš“) ā šµ ā§ (2nd
āš“) ā š¶))) |
|
Theorem | elxp7 6184 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5128. (Contributed by NM, 19-Aug-2006.)
|
⢠(š“ ā (šµ Ć š¶) ā (š“ ā (V Ć V) ā§
((1st āš“)
ā šµ ā§
(2nd āš“)
ā š¶))) |
|
Theorem | oprssdmm 6185* |
Domain of closure of an operation. (Contributed by Jim Kingdon,
23-Oct-2023.)
|
⢠((š ā§ š¢ ā š) ā āš£ š£ ā š¢)
& ⢠((š ā§ (š„ ā š ā§ š¦ ā š)) ā (š„š¹š¦) ā š)
& ⢠(š ā Rel š¹) ā ⢠(š ā (š Ć š) ā dom š¹) |
|
Theorem | eqopi 6186 |
Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.)
(Revised by Mario Carneiro, 23-Feb-2014.)
|
⢠((š“ ā (š Ć š) ā§ ((1st āš“) = šµ ā§ (2nd āš“) = š¶)) ā š“ = āØšµ, š¶ā©) |
|
Theorem | xp2 6187* |
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16-Sep-2006.)
|
⢠(š“ Ć šµ) = {š„ ā (V Ć V) ā£
((1st āš„)
ā š“ ā§
(2nd āš„)
ā šµ)} |
|
Theorem | unielxp 6188 |
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16-Sep-2006.)
|
⢠(š“ ā (šµ Ć š¶) ā āŖ š“ ā āŖ (šµ
Ć š¶)) |
|
Theorem | 1st2nd2 6189 |
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20-Oct-2013.)
|
⢠(š“ ā (šµ Ć š¶) ā š“ = āØ(1st āš“), (2nd āš“)ā©) |
|
Theorem | xpopth 6190 |
An ordered pair theorem for members of cross products. (Contributed by
NM, 20-Jun-2007.)
|
⢠((š“ ā (š¶ Ć š·) ā§ šµ ā (š
Ć š)) ā (((1st āš“) = (1st
āšµ) ā§
(2nd āš“)
= (2nd āšµ)) ā š“ = šµ)) |
|
Theorem | eqop 6191 |
Two ways to express equality with an ordered pair. (Contributed by NM,
3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|
⢠(š“ ā (š Ć š) ā (š“ = āØšµ, š¶ā© ā ((1st āš“) = šµ ā§ (2nd āš“) = š¶))) |
|
Theorem | eqop2 6192 |
Two ways to express equality with an ordered pair. (Contributed by NM,
25-Feb-2014.)
|
⢠šµ ā V & ⢠š¶ ā
V ā ⢠(š“ = āØšµ, š¶ā© ā (š“ ā (V Ć V) ā§
((1st āš“)
= šµ ā§ (2nd
āš“) = š¶))) |
|
Theorem | op1steq 6193* |
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.)
|
⢠(š“ ā (š Ć š) ā ((1st āš“) = šµ ā āš„ š“ = āØšµ, š„ā©)) |
|
Theorem | 2nd1st 6194 |
Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.)
|
⢠(š“ ā (šµ Ć š¶) ā āŖ ā”{š“} = āØ(2nd āš“), (1st āš“)ā©) |
|
Theorem | 1st2nd 6195 |
Reconstruction of a member of a relation in terms of its ordered pair
components. (Contributed by NM, 29-Aug-2006.)
|
⢠((Rel šµ ā§ š“ ā šµ) ā š“ = āØ(1st āš“), (2nd āš“)ā©) |
|
Theorem | 1stdm 6196 |
The first ordered pair component of a member of a relation belongs to the
domain of the relation. (Contributed by NM, 17-Sep-2006.)
|
⢠((Rel š
ā§ š“ ā š
) ā (1st āš“) ā dom š
) |
|
Theorem | 2ndrn 6197 |
The second ordered pair component of a member of a relation belongs to the
range of the relation. (Contributed by NM, 17-Sep-2006.)
|
⢠((Rel š
ā§ š“ ā š
) ā (2nd āš“) ā ran š
) |
|
Theorem | 1st2ndbr 6198 |
Express an element of a relation as a relationship between first and
second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
|
⢠((Rel šµ ā§ š“ ā šµ) ā (1st āš“)šµ(2nd āš“)) |
|
Theorem | releldm2 6199* |
Two ways of expressing membership in the domain of a relation.
(Contributed by NM, 22-Sep-2013.)
|
⢠(Rel š“ ā (šµ ā dom š“ ā āš„ ā š“ (1st āš„) = šµ)) |
|
Theorem | reldm 6200* |
An expression for the domain of a relation. (Contributed by NM,
22-Sep-2013.)
|
⢠(Rel š“ ā dom š“ = ran (š„ ā š“ ⦠(1st āš„))) |