Home | New
Foundations Explorer Theorem List (p. 55 of 64) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | funfvbrb 5401 | Two ways to say that is in the domain of . (Contributed by Mario Carneiro, 1-May-2014.) |
Theorem | fvimacnvi 5402 | A member of a preimage is a function value argument. (Contributed by set.mm contributors, 4-May-2007.) |
Theorem | fvimacnv 5403 | The argument of a function value belongs to the preimage of any class containing the function value. (Contributed by Raph Levien, 20-Nov-2006.) He remarks: "This proof is unsatisfying, because it seems to me that funimass2 5170 could probably be strengthened to a biconditional." |
Theorem | funimass3 5404 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by Raph Levien, 20-Nov-2006.) He remarks: "Likely this could be proved directly, and fvimacnv 5403 would be the special case of being a singleton, but it works this way round too." |
Theorem | funimass5 5405* | A subclass of a preimage in terms of function values. (Contributed by set.mm contributors, 15-May-2007.) |
Theorem | funconstss 5406* | Two ways of specifying that a function is constant on a subdomain. (Contributed by set.mm contributors, 8-Mar-2007.) |
Theorem | elpreima 5407 | Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | unpreima 5408 | Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | inpreima 5409 | Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | respreima 5410 | The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | fimacnv 5411 | The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.) |
Theorem | fnopfv 5412 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by set.mm contributors, 30-Sep-2004.) |
Theorem | fvelrn 5413 | A function's value belongs to its range. (Contributed by set.mm contributors, 14-Oct-1996.) |
Theorem | fnfvelrn 5414 | A function's value belongs to its range. (Contributed by set.mm contributors, 15-Oct-1996.) |
Theorem | ffvelrn 5415 | A function's value belongs to its codomain. (Contributed by set.mm contributors, 12-Aug-1999.) |
Theorem | ffvelrni 5416 | A function's value belongs to its codomain. (Contributed by set.mm contributors, 6-Apr-2005.) |
Theorem | fnasrn 5417* | A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) |
Theorem | f0cli 5418 | Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.) |
Theorem | dff2 5419 | Alternate definition of a mapping. (Contributed by set.mm contributors, 14-Nov-2007.) |
Theorem | dff3 5420* | Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.) |
Theorem | dff4 5421* | Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.) |
Theorem | dffo3 5422* | An onto mapping expressed in terms of function values. (Contributed by set.mm contributors, 29-Oct-2006.) |
Theorem | dffo4 5423* | Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.) |
Theorem | dffo5 5424* | Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.) |
Theorem | foelrn 5425* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) |
Theorem | foco2 5426 | If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) |
Theorem | ffnfv 5427* | A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
Theorem | ffnfvf 5428 | A function maps to a class to which all values belong. This version of ffnfv 5427 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.) |
Theorem | fnfvrnss 5429* | An upper bound for range determined by function values. (Contributed by set.mm contributors, 8-Oct-2004.) |
Theorem | fopabfv 5430* | Representation of a mapping in terms of its values. (Contributed by set.mm contributors, 21-Feb-2004.) |
Theorem | ffvresb 5431* | A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
Theorem | fsn 5432 | A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.) |
Theorem | fsng 5433 | A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by set.mm contributors, 26-Oct-2012.) |
Theorem | fsn2 5434 | A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by set.mm contributors, 19-May-2004.) |
Theorem | xpsn 5435 | The cross product of two singletons. (Contributed by set.mm contributors, 4-Nov-2006.) |
Theorem | ressnop0 5436 | If is not in , then the restriction of a singleton of to is null. (Contributed by Scott Fenton, 15-Apr-2011.) |
Theorem | fpr 5437 | A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (The proof was shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | fnressn 5438 | A function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.) |
Theorem | fressnfv 5439 | The value of a function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.) |
Theorem | fvconst 5440 | The value of a constant function. (Contributed by set.mm contributors, 30-May-1999.) |
Theorem | fopabsn 5441* | The singleton of an ordered pair expressed as an ordered pair class abstraction. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 6-Jun-2006.) (Revised by set.mm contributors, 22-Oct-2011.) |
Theorem | fvi 5442 | The value of the identity function. (Contributed by set.mm contributors, 1-May-2004.) |
Theorem | fvresi 5443 | The value of a restricted identity function. (Contributed by set.mm contributors, 19-May-2004.) |
Theorem | fvunsn 5444 | Remove an ordered pair not participating in a function value. (Contributed by set.mm contributors, 1-Oct-2013.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | fvsn 5445 | The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 12-Aug-1994.) |
Theorem | fvsng 5446 | The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 26-Oct-2012.) |
Theorem | fvsnun1 5447 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 5448. (Contributed by set.mm contributors, 23-Sep-2007.) |
Theorem | fvsnun2 5448 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5447. (Contributed by set.mm contributors, 23-Sep-2007.) |
Theorem | fvpr1 5449 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
Theorem | fvpr2 5450 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
Theorem | fvconst2g 5451 | The value of a constant function. (Contributed by set.mm contributors, 20-Aug-2005.) |
Theorem | fconst2g 5452 | A constant function expressed as a cross product. (Contributed by set.mm contributors, 27-Nov-2007.) |
Theorem | fvconst2 5453 | The value of a constant function. (Contributed by set.mm contributors, 16-Apr-2005.) |
Theorem | fconst2 5454 | A constant function expressed as a cross product. (Contributed by set.mm contributors, 20-Aug-1999.) |
Theorem | fconst5 5455 | Two ways to express that a function is constant. (Contributed by set.mm contributors, 27-Nov-2007.) |
Theorem | fconstfv 5456* | A constant function expressed in terms of its functionality, domain, and value. See also fconst2 5454. (Contributed by NM, 27-Aug-2004.) |
Theorem | fconst3 5457 | Two ways to express a constant function. (Contributed by set.mm contributors, 15-Mar-2007.) |
Theorem | fconst4 5458 | Two ways to express a constant function. (Contributed by set.mm contributors, 8-Mar-2007.) |
Theorem | funfvima 5459 | A function's value in a preimage belongs to the image. (Contributed by set.mm contributors, 23-Sep-2003.) |
Theorem | funfvima2 5460 | A function's value in an included preimage belongs to the image. (Contributed by set.mm contributors, 3-Feb-1997.) |
Theorem | funfvima3 5461 | A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by set.mm contributors, 23-Mar-2004.) |
Theorem | fvclss 5462* | Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.) |
Theorem | abrexco 5463* | Composition of two image maps and . (Contributed by set.mm contributors, 27-May-2013.) |
Theorem | imaiun 5464* | The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.) |
Theorem | imauni 5465* | The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (The proof was shortened by Mario Carneiro, 18-Jun-2014.) (Contributed by set.mm contributors, 9-Aug-2004.) (Revised by set.mm contributors, 18-Jun-2014.) |
Theorem | fniunfv 5466* | The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by set.mm contributors, 27-Sep-2004.) |
Theorem | funiunfv 5467* |
The indexed union of a function's values is the union of its image under
the index class.
Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to , the theorem can be proved without this dependency. (Contributed by set.mm contributors, 26-Mar-2006.) |
Theorem | funiunfvf 5468* | The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 5467 uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006.) (Revised by David Abernethy, 15-Apr-2013.) |
Theorem | eluniima 5469* | Membership in the union of an image of a function. (Contributed by set.mm contributors, 28-Sep-2006.) |
Theorem | elunirn 5470* | Membership in the union of the range of a function. (Contributed by set.mm contributors, 24-Sep-2006.) |
Theorem | dff13 5471* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by set.mm contributors, 29-Oct-1996.) |
Theorem | dff13f 5472* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 31-Jul-2003.) |
Theorem | f1fveq 5473 | Equality of function values for a one-to-one function. (Contributed by set.mm contributors, 11-Feb-1997.) |
Theorem | f1elima 5474 | Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | dff1o6 5475* | A one-to-one onto function in terms of function values. (Contributed by set.mm contributors, 29-Mar-2008.) |
Theorem | f1ocnvfv1 5476 | The converse value of the value of a one-to-one onto function. (Contributed by set.mm contributors, 20-May-2004.) |
Theorem | f1ocnvfv2 5477 | The value of the converse value of a one-to-one onto function. (Contributed by set.mm contributors, 20-May-2004.) |
Theorem | f1ocnvfv 5478 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.) |
Theorem | f1ocnvfvb 5479 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by set.mm contributors, 20-May-2004.) (Revised by set.mm contributors, 9-Aug-2006.) |
Theorem | f1ofveu 5480* | There is one domain element for each value of a one-to-one onto function. (Contributed by set.mm contributors, 26-May-2006.) |
Theorem | f1ocnvdm 5481 | The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by set.mm contributors, 26-May-2006.) |
Theorem | isoeq1 5482 | Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.) |
Theorem | isoeq2 5483 | Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.) |
Theorem | isoeq3 5484 | Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.) |
Theorem | isoeq4 5485 | Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.) |
Theorem | isoeq5 5486 | Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.) |
Theorem | nfiso 5487 | Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | isof1o 5488 | An isomorphism is a one-to-one onto function. (Contributed by set.mm contributors, 27-Apr-2004.) |
Theorem | isorel 5489 | An isomorphism connects binary relations via its function values. (Contributed by set.mm contributors, 27-Apr-2004.) |
Theorem | isoid 5490 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.) |
Theorem | isocnv 5491 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.) |
Theorem | isocnv2 5492 | Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) |
Theorem | isores2 5493 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | isores1 5494 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | isotr 5495 | Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.) |
Theorem | isomin 5496 | Isomorphisms preserve minimal elements. Note that is Takeuti and Zaring's idiom for the initial segment . Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 19-Apr-2004.) |
Theorem | isoini 5497 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 20-Apr-2004.) |
Theorem | isoini2 5498 | Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.) |
Theorem | f1oiso 5499* | Any one-to-one onto function determines an isomorphism with an induced relation . Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by set.mm contributors, 30-Apr-2004.) |
Theorem | f1oiso2 5500* | Any one-to-one onto function determines an isomorphism with an induced relation . (Contributed by Mario Carneiro, 9-Mar-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |