HomeHome New Foundations Explorer
Theorem 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.
class AddC
 
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)
    < 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-6338
  Copyright terms: Public domain < Previous  Next >