HomeHome New Foundations Explorer
Theorem List (p. 55 of 64)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 5401-5500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfunfvbrb 5401 Two ways to say that A is in the domain of F. (Contributed by Mario Carneiro, 1-May-2014.)
(Fun F → (A dom FAF(FA)))
 
Theoremfvimacnvi 5402 A member of a preimage is a function value argument. (Contributed by set.mm contributors, 4-May-2007.)
((Fun F A (FB)) → (FA) B)
 
Theoremfvimacnv 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."
((Fun F A dom F) → ((FA) BA (FB)))
 
Theoremfunimass3 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 A being a singleton, but it works this way round too."
((Fun F A dom F) → ((FA) BA (FB)))
 
Theoremfunimass5 5405* A subclass of a preimage in terms of function values. (Contributed by set.mm contributors, 15-May-2007.)
((Fun F A dom F) → (A (FB) ↔ x A (Fx) B))
 
Theoremfunconstss 5406* Two ways of specifying that a function is constant on a subdomain. (Contributed by set.mm contributors, 8-Mar-2007.)
((Fun F A dom F) → (x A (Fx) = BA (F “ {B})))
 
Theoremelpreima 5407 Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
(F Fn A → (B (FC) ↔ (B A (FB) C)))
 
Theoremunpreima 5408 Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun F → (F “ (AB)) = ((FA) ∪ (FB)))
 
Theoreminpreima 5409 Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun F → (F “ (AB)) = ((FA) ∩ (FB)))
 
Theoremrespreima 5410 The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Fun F → ((F B) “ A) = ((FA) ∩ B))
 
Theoremfimacnv 5411 The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
(F:A–→B → (FB) = A)
 
Theoremfnopfv 5412 Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by set.mm contributors, 30-Sep-2004.)
((F Fn A B A) → B, (FB) F)
 
Theoremfvelrn 5413 A function's value belongs to its range. (Contributed by set.mm contributors, 14-Oct-1996.)
((Fun F A dom F) → (FA) ran F)
 
Theoremfnfvelrn 5414 A function's value belongs to its range. (Contributed by set.mm contributors, 15-Oct-1996.)
((F Fn A B A) → (FB) ran F)
 
Theoremffvelrn 5415 A function's value belongs to its codomain. (Contributed by set.mm contributors, 12-Aug-1999.)
((F:A–→B C A) → (FC) B)
 
Theoremffvelrni 5416 A function's value belongs to its codomain. (Contributed by set.mm contributors, 6-Apr-2005.)
F:A–→B       (C A → (FC) B)
 
Theoremfnasrn 5417* A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.)
(F Fn AF = ran {x, y (x A y = x, (Fx))})
 
Theoremf0cli 5418 Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.)
F:A–→B    &    B       (FC) B
 
Theoremdff2 5419 Alternate definition of a mapping. (Contributed by set.mm contributors, 14-Nov-2007.)
(F:A–→B ↔ (F Fn A F (A × B)))
 
Theoremdff3 5420* Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:A–→B ↔ (F (A × B) x A ∃!y xFy))
 
Theoremdff4 5421* Alternate definition of a mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:A–→B ↔ (F (A × B) x A ∃!y B xFy))
 
Theoremdffo3 5422* An onto mapping expressed in terms of function values. (Contributed by set.mm contributors, 29-Oct-2006.)
(F:AontoB ↔ (F:A–→B y B x A y = (Fx)))
 
Theoremdffo4 5423* Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:AontoB ↔ (F:A–→B y B x A xFy))
 
Theoremdffo5 5424* Alternate definition of an onto mapping. (Contributed by set.mm contributors, 20-Mar-2007.)
(F:AontoB ↔ (F:A–→B y B x xFy))
 
Theoremfoelrn 5425* Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.)
((F:AontoB C B) → x A C = (Fx))
 
Theoremfoco2 5426 If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
((F:B–→C G:A–→B (F G):AontoC) → F:BontoC)
 
Theoremffnfv 5427* A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.)
(F:A–→B ↔ (F Fn A x A (Fx) B))
 
Theoremffnfvf 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.)
xA    &   xB    &   xF       (F:A–→B ↔ (F Fn A x A (Fx) B))
 
Theoremfnfvrnss 5429* An upper bound for range determined by function values. (Contributed by set.mm contributors, 8-Oct-2004.)
((F Fn A x A (Fx) B) → ran F B)
 
Theoremfopabfv 5430* Representation of a mapping in terms of its values. (Contributed by set.mm contributors, 21-Feb-2004.)
(F:A–→B ↔ (F = {x, y (x A y = (Fx))} x A (Fx) B))
 
Theoremffvresb 5431* A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.)
(Fun F → ((F A):A–→Bx A (x dom F (Fx) B)))
 
Theoremfsn 5432 A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)
A V    &   B V       (F:{A}–→{B} ↔ F = {A, B})
 
Theoremfsng 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.)
((A C B D) → (F:{A}–→{B} ↔ F = {A, B}))
 
Theoremfsn2 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.)
A V       (F:{A}–→B ↔ ((FA) B F = {A, (FA)}))
 
Theoremxpsn 5435 The cross product of two singletons. (Contributed by set.mm contributors, 4-Nov-2006.)
A V    &   B V       ({A} × {B}) = {A, B}
 
Theoremressnop0 5436 If A is not in C, then the restriction of a singleton of A, B to C is null. (Contributed by Scott Fenton, 15-Apr-2011.)
A C → ({A, B} C) = )
 
Theoremfpr 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.)
A V    &   B V    &   C V    &   D V       (AB → {A, C, B, D}:{A, B}–→{C, D})
 
Theoremfnressn 5438 A function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.)
((F Fn A B A) → (F {B}) = {B, (FB)})
 
Theoremfressnfv 5439 The value of a function restricted to a singleton. (Contributed by set.mm contributors, 9-Oct-2004.)
((F Fn A B A) → ((F {B}):{B}–→C ↔ (FB) C))
 
Theoremfvconst 5440 The value of a constant function. (Contributed by set.mm contributors, 30-May-1999.)
((F:A–→{B} C A) → (FC) = B)
 
Theoremfopabsn 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.)
A V    &   B V       {A, B} = {x, y (x {A} y = B)}
 
Theoremfvi 5442 The value of the identity function. (Contributed by set.mm contributors, 1-May-2004.)
(A V → ( I ‘A) = A)
 
Theoremfvresi 5443 The value of a restricted identity function. (Contributed by set.mm contributors, 19-May-2004.)
(B A → (( I A) ‘B) = B)
 
Theoremfvunsn 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.)
(BD → ((A ∪ {B, C}) ‘D) = (AD))
 
Theoremfvsn 5445 The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 12-Aug-1994.)
A V    &   B V       ({A, B} ‘A) = B
 
Theoremfvsng 5446 The value of a singleton of an ordered pair is the second member. (Contributed by set.mm contributors, 26-Oct-2012.)
((A V B W) → ({A, B} ‘A) = B)
 
Theoremfvsnun1 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.)
A V    &   B V    &   G = ({A, B} ∪ (F (C {A})))       (GA) = B
 
Theoremfvsnun2 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.)
A V    &   B V    &   G = ({A, B} ∪ (F (C {A})))       (D (C {A}) → (GD) = (FD))
 
Theoremfvpr1 5449 The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
A V    &   C V       (AB → ({A, C, B, D} ‘A) = C)
 
Theoremfvpr2 5450 The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
B V    &   D V       (AB → ({A, C, B, D} ‘B) = D)
 
Theoremfvconst2g 5451 The value of a constant function. (Contributed by set.mm contributors, 20-Aug-2005.)
((B D C A) → ((A × {B}) ‘C) = B)
 
Theoremfconst2g 5452 A constant function expressed as a cross product. (Contributed by set.mm contributors, 27-Nov-2007.)
(B C → (F:A–→{B} ↔ F = (A × {B})))
 
Theoremfvconst2 5453 The value of a constant function. (Contributed by set.mm contributors, 16-Apr-2005.)
B V       (C A → ((A × {B}) ‘C) = B)
 
Theoremfconst2 5454 A constant function expressed as a cross product. (Contributed by set.mm contributors, 20-Aug-1999.)
B V       (F:A–→{B} ↔ F = (A × {B}))
 
Theoremfconst5 5455 Two ways to express that a function is constant. (Contributed by set.mm contributors, 27-Nov-2007.)
((F Fn A A) → (F = (A × {B}) ↔ ran F = {B}))
 
Theoremfconstfv 5456* A constant function expressed in terms of its functionality, domain, and value. See also fconst2 5454. (Contributed by NM, 27-Aug-2004.)
(F:A–→{B} ↔ (F Fn A x A (Fx) = B))
 
Theoremfconst3 5457 Two ways to express a constant function. (Contributed by set.mm contributors, 15-Mar-2007.)
(F:A–→{B} ↔ (F Fn A A (F “ {B})))
 
Theoremfconst4 5458 Two ways to express a constant function. (Contributed by set.mm contributors, 8-Mar-2007.)
(F:A–→{B} ↔ (F Fn A (F “ {B}) = A))
 
Theoremfunfvima 5459 A function's value in a preimage belongs to the image. (Contributed by set.mm contributors, 23-Sep-2003.)
((Fun F B dom F) → (B A → (FB) (FA)))
 
Theoremfunfvima2 5460 A function's value in an included preimage belongs to the image. (Contributed by set.mm contributors, 3-Feb-1997.)
((Fun F A dom F) → (B A → (FB) (FA)))
 
Theoremfunfvima3 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.)
((Fun F F G) → (A dom F → (FA) (G “ {A})))
 
Theoremfvclss 5462* Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.)
{y x y = (Fx)} (ran F ∪ {})
 
Theoremabrexco 5463* Composition of two image maps C(y) and B(w). (Contributed by set.mm contributors, 27-May-2013.)
B V    &   (y = BC = D)       {x y {z w A z = B}x = C} = {x w A x = D}
 
Theoremimaiun 5464* The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.)
(Ax B C) = x B (AC)
 
Theoremimauni 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.)
(AB) = x B (Ax)
 
Theoremfniunfv 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.)
(F Fn Ax A (Fx) = ran F)
 
Theoremfuniunfv 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 F Fn A, the theorem can be proved without this dependency. (Contributed by set.mm contributors, 26-Mar-2006.)

(Fun Fx A (Fx) = (FA))
 
Theoremfuniunfvf 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.)
xF       (Fun Fx A (Fx) = (FA))
 
Theoremeluniima 5469* Membership in the union of an image of a function. (Contributed by set.mm contributors, 28-Sep-2006.)
(Fun F → (B (FA) ↔ x A B (Fx)))
 
Theoremelunirn 5470* Membership in the union of the range of a function. (Contributed by set.mm contributors, 24-Sep-2006.)
(Fun F → (A ran Fx dom F A (Fx)))
 
Theoremdff13 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.)
(F:A1-1B ↔ (F:A–→B x A y A ((Fx) = (Fy) → x = y)))
 
Theoremdff13f 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.)
xF    &   yF       (F:A1-1B ↔ (F:A–→B x A y A ((Fx) = (Fy) → x = y)))
 
Theoremf1fveq 5473 Equality of function values for a one-to-one function. (Contributed by set.mm contributors, 11-Feb-1997.)
((F:A1-1B (C A D A)) → ((FC) = (FD) ↔ C = D))
 
Theoremf1elima 5474 Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.)
((F:A1-1B X A Y A) → ((FX) (FY) ↔ X Y))
 
Theoremdff1o6 5475* A one-to-one onto function in terms of function values. (Contributed by set.mm contributors, 29-Mar-2008.)
(F:A1-1-ontoB ↔ (F Fn A ran F = B x A y A ((Fx) = (Fy) → x = y)))
 
Theoremf1ocnvfv1 5476 The converse value of the value of a one-to-one onto function. (Contributed by set.mm contributors, 20-May-2004.)
((F:A1-1-ontoB C A) → (F ‘(FC)) = C)
 
Theoremf1ocnvfv2 5477 The value of the converse value of a one-to-one onto function. (Contributed by set.mm contributors, 20-May-2004.)
((F:A1-1-ontoB C B) → (F ‘(FC)) = C)
 
Theoremf1ocnvfv 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.)
((F:A1-1-ontoB C A) → ((FC) = D → (FD) = C))
 
Theoremf1ocnvfvb 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.)
((F:A1-1-ontoB C A D B) → ((FC) = D ↔ (FD) = C))
 
Theoremf1ofveu 5480* There is one domain element for each value of a one-to-one onto function. (Contributed by set.mm contributors, 26-May-2006.)
((F:A1-1-ontoB C B) → ∃!x A (Fx) = C)
 
Theoremf1ocnvdm 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.)
((F:A1-1-ontoB C B) → (FC) A)
 
Theoremisoeq1 5482 Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
(H = G → (H Isom R, S (A, B) ↔ G Isom R, S (A, B)))
 
Theoremisoeq2 5483 Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
(R = T → (H Isom R, S (A, B) ↔ H Isom T, S (A, B)))
 
Theoremisoeq3 5484 Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
(S = T → (H Isom R, S (A, B) ↔ H Isom R, T (A, B)))
 
Theoremisoeq4 5485 Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
(A = C → (H Isom R, S (A, B) ↔ H Isom R, S (C, B)))
 
Theoremisoeq5 5486 Equality theorem for isomorphisms. (Contributed by set.mm contributors, 17-May-2004.)
(B = C → (H Isom R, S (A, B) ↔ H Isom R, S (A, C)))
 
Theoremnfiso 5487 Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
xH    &   xR    &   xS    &   xA    &   xB       x H Isom R, S (A, B)
 
Theoremisof1o 5488 An isomorphism is a one-to-one onto function. (Contributed by set.mm contributors, 27-Apr-2004.)
(H Isom R, S (A, B) → H:A1-1-ontoB)
 
Theoremisorel 5489 An isomorphism connects binary relations via its function values. (Contributed by set.mm contributors, 27-Apr-2004.)
((H Isom R, S (A, B) (C A D A)) → (CRD ↔ (HC)S(HD)))
 
Theoremisoid 5490 Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.)
( I A) Isom R, R (A, A)
 
Theoremisocnv 5491 Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.)
(H Isom R, S (A, B) → H Isom S, R (B, A))
 
Theoremisocnv2 5492 Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
(H Isom R, S (A, B) ↔ H Isom R, S(A, B))
 
Theoremisores2 5493 An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
(H Isom R, S (A, B) ↔ H Isom R, (S ∩ (B × B))(A, B))
 
Theoremisores1 5494 An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
(H Isom R, S (A, B) ↔ H Isom (R ∩ (A × A)), S(A, B))
 
Theoremisotr 5495 Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 27-Apr-2004.)
((H Isom R, S (A, B) G Isom S, T (B, C)) → (G H) Isom R, T (A, C))
 
Theoremisomin 5496 Isomorphisms preserve minimal elements. Note that (R “ {D}) is Takeuti and Zaring's idiom for the initial segment {x xRD}. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 19-Apr-2004.)
((H Isom R, S (A, B) (C A D A)) → ((C ∩ (R “ {D})) = ↔ ((HC) ∩ (S “ {(HD)})) = ))
 
Theoremisoini 5497 Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by set.mm contributors, 20-Apr-2004.)
((H Isom R, S (A, B) D A) → (H “ (A ∩ (R “ {D}))) = (B ∩ (S “ {(HD)})))
 
Theoremisoini2 5498 Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
C = (A ∩ (R “ {X}))    &   D = (B ∩ (S “ {(HX)}))       ((H Isom R, S (A, B) X A) → (H C) Isom R, S (C, D))
 
Theoremf1oiso 5499* Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by set.mm contributors, 30-Apr-2004.)
((H:A1-1-ontoB S = {z, w x A y A ((z = (Hx) w = (Hy)) xRy)}) → H Isom R, S (A, B))
 
Theoremf1oiso2 5500* Any one-to-one onto function determines an isomorphism with an induced relation S. (Contributed by Mario Carneiro, 9-Mar-2013.)
S = {x, y ((x B y B) (Hx)R(Hy))}       (H:A1-1-ontoBH Isom R, S (A, B))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6336
  Copyright terms: Public domain < Previous  Next >