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))

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-6337
 Copyright terms: Public domain < Previous  Next >