 Home New Foundations ExplorerTheorem List (p. 58 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 - 5701-5800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfvmpts 5701* Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
F = (x C B)       ((A C [A / x]B V) → (FA) = [A / x]B)

Theoremfvmptd 5702* Deduction version of fvmpt 5700. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
(φF = (x D B))    &   ((φ x = A) → B = C)    &   (φA D)    &   (φC V)       (φ → (FA) = C)

Theoremfvmpt2i 5703* Value of a function given by the "maps to" notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
F = (x A B)       (x A → (Fx) = ( I ‘B))

Theoremfvmpt2 5704* Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
F = (x A B)       ((x A B C) → (Fx) = B)

Theoremfvmptss 5705* If all the values of the mapping are subsets of a class C, then so is any evaluation of the mapping, even if D is not in the base set A. (Contributed by Mario Carneiro, 13-Feb-2015.)
F = (x A B)       (x A B C → (FD) C)

Theoremdffn5v 5706* Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
(F Fn AF = (x A (Fx)))

Theoremfnov2 5707* Representation of a function in terms of its values. (Contributed by Mario Carneiro, 23-Dec-2013.)
(F Fn (A × B) ↔ F = (x A, y B (xFy)))

Theoremmpt2mptx 5708* Express a two-argument function as a one-argument function, or vice-versa. In this version B(x) is not assumed to be constant w.r.t x. (Contributed by Mario Carneiro, 29-Dec-2014.)
(z = x, yC = D)       (z x A ({x} × B) C) = (x A, y B D)

Theoremmpt2mpt 5709* Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
(z = x, yC = D)       (z (A × B) C) = (x A, y B D)

Theoremovmpt4g 5710* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5704.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
F = (x A, y B C)       ((x A y B C V) → (xFy) = C)

Theoremov2gf 5711* The value of an operation class abstraction. A version of ovmpt2g 5715 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
xA    &   yA    &   yB    &   xG    &   yS    &   (x = AR = G)    &   (y = BG = S)    &   F = (x C, y D R)       ((A C B D S H) → (AFB) = S)

Theoremovmpt2x 5712* The value of an operation class abstraction. Variant of ovmpt2ga 5713 which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
((x = A y = B) → R = S)    &   (x = AD = L)    &   F = (x C, y D R)       ((A C B L S H) → (AFB) = S)

Theoremovmpt2ga 5713* Value of an operation given by a maps-to rule. Equivalent to ov2ag 5598. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → R = S)    &   F = (x C, y D R)       ((A C B D S H) → (AFB) = S)

Theoremovmpt2a 5714* Value of an operation given by a maps-to rule. Equivalent to ov2ag 5598. (Contributed by set.mm contributors, 19-Dec-2013.)
((x = A y = B) → R = S)    &   F = (x C, y D R)    &   S V       ((A C B D) → (AFB) = S)

Theoremovmpt2g 5715* Value of an operation given by a maps-to rule. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 2-Oct-2007.) (Revised by set.mm contributors, 24-Jul-2012.)
(x = AR = G)    &   (y = BG = S)    &   F = (x C, y D R)       ((A C B D S H) → (AFB) = S)

Theoremovmpt2 5716* Value of an operation given by a maps-to rule. Equivalent to ov2 in set.mm. (Contributed by set.mm contributors, 12-Sep-2011.)
(x = AR = G)    &   (y = BG = S)    &   F = (x C, y D R)    &   S V       ((A C B D) → (AFB) = S)

Theoremrnmpt2 5717* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
F = (x A, y B C)       ran F = {z x A y B z = C}

Theoremmptv 5718* Function with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
(x V B) = {x, y y = B}

Theoremmpt2v 5719* Operation with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
(x V, y V C) = {x, y, z z = C}

Theoremmptresid 5720* The restricted identity expressed with the "maps to" notation. (Contributed by FL, 25-Apr-2012.)
(x A x) = ( I A)

Theoremfvmptex 5721* Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that ( I ‘B) is just shorthand for if(B V, B, ), and it is always a set by fvex 5339.) Note also that these functions are not the same; wherever B(C) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G, and G(C) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
F = (x A B)    &   G = (x A ( I ‘B))       (FC) = (GC)

Theoremfvmptf 5722* Value of a function given by an ordered-pair class abstraction. This version of fvmptg 5698 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA    &   xC    &   (x = AB = C)    &   F = (x D B)       ((A D C V) → (FA) = C)

Theoremfvmptnf 5723* The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 5724 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
xA    &   xC    &   (x = AB = C)    &   F = (x D B)       C V → (FA) = )

Theoremfvmptn 5724* This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class C it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 5698. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
(x = DB = C)    &   F = (x A B)       C V → (FD) = )

Theoremfvmptss2 5725* A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.)
(x = DB = C)    &   F = (x A B)       (FD) C

Theoremf1od 5726* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
F = (x A C)    &   ((φ x A) → C W)    &   ((φ y B) → D X)    &   (φ → ((x A y = C) ↔ (y B x = D)))       (φF:A1-1-ontoB)

Theoremf1o2d 5727* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
F = (x A C)    &   ((φ x A) → C B)    &   ((φ y B) → D A)    &   ((φ (x A y B)) → (x = Dy = C))       (φF:A1-1-ontoB)

Theoremdfswap3 5728* Alternate definition of Swap as an operator abstraction. (Contributed by SF, 23-Feb-2015.)
Swap = {x, y, z z = y, x}

Theoremdfswap4 5729* Alternate definition of Swap as an operator mapping. (Contributed by SF, 23-Feb-2015.)
Swap = (x V, y V y, x)

Theoremfmpt2x 5730* Functionality, domain and codomain of a class given by the "maps to" notation, where B(x) is not constant but depends on x. (Contributed by NM, 29-Dec-2014.)
F = (x A, y B C)       (x A y B C DF:x A ({x} × B)–→D)

Theoremfmpt2 5731* Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
F = (x A, y B C)       (x A y B C DF:(A × B)–→D)

Theoremfnmpt2 5732* Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
F = (x A, y B C)       (x A y B C VF Fn (A × B))

Theoremfnmpt2i 5733* Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
F = (x A, y B C)    &   C V       F Fn (A × B)

Theoremdmmpt2 5734* Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
F = (x A, y B C)    &   C V       dom F = (A × B)

2.3.10  Set construction lemmas

Syntaxctxp 5735 Extend the definition of a class to include the tail cross product.
class (AB)

Definitiondf-txp 5736 Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5783 for membership. (Contributed by SF, 9-Feb-2015.)
(AB) = ((1st A) ∩ (2nd B))

Syntaxcpprod 5737 Extend the definition of a class to include the parallel product operation.
class PProd (A, B)

Definitiondf-pprod 5738 Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)
PProd (A, B) = ((A 1st ) ⊗ (B 2nd ))

Syntaxcfix 5739 Extend the definition of a class to include the fixed points of a relationship.
class Fix A

Definitiondf-fix 5740 Define the fixed points of a relationship. (Contributed by SF, 9-Feb-2015.)
Fix A = ran (A ∩ I )

Syntaxccup 5741 Extend the definition of a class to include the cup function.
class Cup

Definitiondf-cup 5742* Define the cup function. (Contributed by SF, 9-Feb-2015.)
Cup = (x V, y V (xy))

Syntaxcdisj 5743 Extend the definition of a class to include the disjoint relationship.
class Disj

Definitiondf-disj 5744* Define the relationship of all disjoint sets. (Contributed by SF, 9-Feb-2015.)
Disj = {x, y (xy) = }

Syntaxcaddcfn 5745 Extend the definition of a class to include the cardinal sum function.

Definitiondf-addcfn 5746* Define the function representing cardinal sum. (Contributed by SF, 9-Feb-2015.)
AddC = (x V, y V (x +c y))

Syntaxccompose 5747 Extend the definition of a class to include the compostion function.
class Compose

Definitiondf-compose 5748* Define the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
Compose = (x V, y V (x y))

Syntaxcins2 5749 Extend the definition of a class to include the second insertion operation.
class Ins2 A

Definitiondf-ins2 5750 Define the second insertion operation. (Contributed by SF, 9-Feb-2015.)
Ins2 A = (V ⊗ A)

Syntaxcins3 5751 Extend the definition of a class to include the third insertion operation.
class Ins3 A

Definitiondf-ins3 5752 Define the third insertion operation. (Contributed by SF, 9-Feb-2015.)
Ins3 A = (A ⊗ V)

Syntaxcimage 5753 Extend the definition of a class to include the image function.
class ImageA

Definitiondf-image 5754 Define the image function of a class. (Contributed by SF, 9-Feb-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
ImageA = ∼ (( Ins2 S Ins3 ( S SI A)) “ 1c)

Syntaxcins4 5755 Extend the definition of a class to include the fourth insertion operation.
class Ins4 A

Definitiondf-ins4 5756 Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)
Ins4 A = ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)

Syntaxcsi3 5757 Extend the definition of a class to include the triple singleton image.
class SI3 A

Definitiondf-si3 5758 Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)
SI3 A = (( SI 1st ⊗ ( SI (1st 2nd ) ⊗ SI (2nd 2nd ))) “ 1A)

Syntaxcfuns 5759 Extend the definition of a class to include the set of all functions.
class Funs

Definitiondf-funs 5760 Define the class of all functions. (Contributed by SF, 9-Feb-2015.)
Funs = {f Fun f}

Syntaxcfns 5761 Extend the definition of a class to include the function with domain relationship.
class Fns

Definitiondf-fns 5762* Define the function with domain relationship. (Contributed by SF, 9-Feb-2015.)
Fns = {f, a f Fn a}

Syntaxccross 5763 Extend the definition of a class to include the cross product function.
class Cross

Definitiondf-cross 5764* Define the cross product function. (Contributed by SF, 9-Feb-2015.)
Cross = (x V, y V (x × y))

Syntaxcpw1fn 5765 Extend the definition of a class to include the unit power class function.
class Pw1Fn

Definitiondf-pw1fn 5766 Define the function that takes a singleton to the unit power class of its member. This function is defined in such a way as to ensure stratification. (Contributed by SF, 9-Feb-2015.)
Pw1Fn = (x 1c 1x)

Syntaxcfullfun 5767 Extend the definition of a class to include the full function operation.
class FullFun F

Definitiondf-fullfun 5768 Define the full function operator. This is a function over V that agrees with the function value of F at every point. (Contributed by SF, 9-Feb-2015.)
FullFun F = ((( I F) ( ∼ I F)) ∪ ( ∼ dom (( I F) ( ∼ I F)) × {}))

Syntaxcdomfn 5769 Extend the definition of a class to include the domain function.
class Dom

Definitiondf-domfn 5770 Define the domain function. This is a function wrapper for the domain operator. (Contributed by Scott Fenton, 9-Aug-2019.)
Dom = (x V dom x)

Syntaxcranfn 5771 Extend the definition of a class to include the range function.
class Ran

Definitiondf-ranfn 5772 Define the range function. This is a function wrapper for the range operator. (Contributed by Scott Fenton, 9-Aug-2019.)
Ran = (x V ran x)

Theorembrsnsi 5773 Binary relationship of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
A V    &   B V       ({A} SI R{B} ↔ ARB)

Theoremopsnelsi 5774 Ordered pair membership of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
A V    &   B V       ({A}, {B} SI RA, B R)

Theorembrsnsi1 5775* Binary relationship of a singleton to an arbitrary set in a singleton image. (Contributed by SF, 9-Mar-2015.)
A V       ({A} SI RBx(B = {x} ARx))

Theorembrsnsi2 5776* Binary relationship of an arbitrary set to a singleton in a singleton image. (Contributed by SF, 9-Mar-2015.)
A V       (B SI R{A} ↔ x(B = {x} xRA))

Theorembrco1st 5777 Binary relationship of composition with 1st. (Contributed by SF, 9-Feb-2015.)
A V    &   B V       (A, B(R 1st )CARC)

Theorembrco2nd 5778 Binary relationship of composition with 2nd. (Contributed by SF, 9-Feb-2015.)
A V    &   B V       (A, B(R 2nd )CBRC)

Theoremtxpeq1 5779 Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
(A = B → (AC) = (BC))

Theoremtxpeq2 5780 Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
(A = B → (CA) = (CB))

Theoremtrtxp 5781 Trinary relationship over a tail cross product. (Contributed by SF, 13-Feb-2015.)
(A(RS)B, C ↔ (ARB ASC))

Theoremoteltxp 5782 Ordered triple membership in a tail cross product. (Contributed by SF, 13-Feb-2015.)
(A, B, C (RS) ↔ (A, B R A, C S))

Theorembrtxp 5783* Binary relationship over a tail cross product. (Contributed by SF, 11-Feb-2015.)
(A(RS)Bxy(B = x, y ARx ASy))

Theoremtxpexg 5784 The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
((A V B W) → (AB) V)

Theoremtxpex 5785 The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
A V    &   B V       (AB) V

Theoremrestxp 5786 Restriction distributes over tail cross product. (Contributed by SF, 24-Feb-2015.)
((AB) C) = ((A C) ⊗ (B C))

Theoremelfix 5787 Membership in the fixed points of a relationship. (Contributed by SF, 11-Feb-2015.)
(A Fix RARA)

Theoremfixexg 5788 The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
(R V Fix R V)

Theoremfixex 5789 The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
R V        Fix R V

Theoremop1st2nd 5790 Express equality to an ordered pair via 1st and 2nd. (Contributed by SF, 12-Feb-2015.)
A V    &   B V       ((C1st A C2nd B) ↔ C = A, B)

Theoremotelins2 5791 Ordered triple membership in Ins2. (Contributed by SF, 13-Feb-2015.)
B V       (A, B, C Ins2 RA, C R)

Theoremotelins3 5792 Ordered triple membership in Ins3. (Contributed by SF, 13-Feb-2015.)
C V       (A, B, C Ins3 RA, B R)

Theorembrimage 5793 Binary relationship over the image function. (Contributed by SF, 11-Feb-2015.)
A V    &   B V       (AImageRBB = (RA))

Theoremoqelins4 5794 Ordered quadruple membership in Ins4. (Contributed by SF, 13-Feb-2015.)
D V       (A, B, C, D Ins4 RA, B, C R)

Theoremins2exg 5795 Ins2 preserves sethood. (Contributed by SF, 9-Mar-2015.)
(A VIns2 A V)

Theoremins3exg 5796 Ins3 preserves sethood. (Contributed by SF, 22-Feb-2015.)
(A VIns3 A V)

Theoremins2ex 5797 Ins2 preserves sethood. (Contributed by SF, 12-Feb-2015.)
A V        Ins2 A V

Theoremins3ex 5798 Ins3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
A V        Ins3 A V

Theoremins4ex 5799 Ins4 preserves sethood. (Contributed by SF, 12-Feb-2015.)
A V        Ins4 A V

Theoremimageexg 5800 The image function of a set is a set. (Contributed by SF, 11-Feb-2015.)
(A V → ImageA V)

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 >