P. 58 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5701-5800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fvmpt 5701*	Value of a function given in maps-to notation. (Contributed by set.mm contributors, 17-Aug-2011.)
|- (x = A -> B = C)   &   |- F = (x e. D |-> B)   &   |- C e. _V   =>   |- (A e. D -> (F` A) = C)
Theorem	fvmpts 5702*	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 e. C |-> B)   =>   |- ((A e. C /\ [_A / x]_B e. V) -> (F` A) = [_A / x]_B)
Theorem	fvmptd 5703*	Deduction version of fvmpt 5701. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- (ph -> F = (x e. D |-> B))   &   |- ((ph /\ x = A) -> B = C)   &   |- (ph -> A e. D)   &   |- (ph -> C e. V)   =>   |- (ph -> (F` A) = C)
Theorem	fvmpt2i 5704*	Value of a function given by the "maps to" notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- F = (x e. A |-> B)   =>   |- (x e. A -> (F` x) = ( _I ` B))
Theorem	fvmpt2 5705*	Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
|- F = (x e. A |-> B)   =>   |- ((x e. A /\ B e. C) -> (F` x) = B)
Theorem	fvmptss 5706*	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 e. A |-> B)   =>   |- (A.x e. A B C_ C -> (F` D) C_ C)
Theorem	dffn5v 5707*	Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- (F Fn A <-> F = (x e. A |-> (F` x)))
Theorem	fnov2 5708*	Representation of a function in terms of its values. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- (F Fn (A X. B) <-> F = (x e. A, y e. B |-> (xFy)))
Theorem	mpt2mptx 5709*	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, y>. -> C = D)   =>   |- (z e. U_x e. A ({x} X. B) |-> C) = (x e. A, y e. B |-> D)
Theorem	mpt2mpt 5710*	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, y>. -> C = D)   =>   |- (z e. (A X. B) |-> C) = (x e. A, y e. B |-> D)
Theorem	ovmpt4g 5711*	Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5705.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = (x e. A, y e. B |-> C)   =>   |- ((x e. A /\ y e. B /\ C e. V) -> (xFy) = C)
Theorem	ov2gf 5712*	The value of an operation class abstraction. A version of ovmpt2g 5716 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- F/_xA   &   |- F/_yA   &   |- F/_yB   &   |- F/_xG   &   |- F/_yS   &   |- (x = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = (x e. C, y e. D |-> R)   =>   |- ((A e. C /\ B e. D /\ S e. H) -> (AFB) = S)
Theorem	ovmpt2x 5713*	The value of an operation class abstraction. Variant of ovmpt2ga 5714 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 = A -> D = L)   &   |- F = (x e. C, y e. D |-> R)   =>   |- ((A e. C /\ B e. L /\ S e. H) -> (AFB) = S)
Theorem	ovmpt2ga 5714*	Value of an operation given by a maps-to rule. Equivalent to ov2ag 5599. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ((x = A /\ y = B) -> R = S)   &   |- F = (x e. C, y e. D |-> R)   =>   |- ((A e. C /\ B e. D /\ S e. H) -> (AFB) = S)
Theorem	ovmpt2a 5715*	Value of an operation given by a maps-to rule. Equivalent to ov2ag 5599. (Contributed by set.mm contributors, 19-Dec-2013.)
|- ((x = A /\ y = B) -> R = S)   &   |- F = (x e. C, y e. D |-> R)   &   |- S e. _V   =>   |- ((A e. C /\ B e. D) -> (AFB) = S)
Theorem	ovmpt2g 5716*	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 = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = (x e. C, y e. D |-> R)   =>   |- ((A e. C /\ B e. D /\ S e. H) -> (AFB) = S)
Theorem	ovmpt2 5717*	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 = A -> R = G)   &   |- (y = B -> G = S)   &   |- F = (x e. C, y e. D |-> R)   &   |- S e. _V   =>   |- ((A e. C /\ B e. D) -> (AFB) = S)
Theorem	rnmpt2 5718*	The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
|- F = (x e. A, y e. B |-> C)   =>   |- ran F = {z | E.x e. A E.y e. B z = C}
Theorem	mptv 5719*	Function with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
|- (x e. _V |-> B) = {<.x, y>. | y = B}
Theorem	mpt2v 5720*	Operation with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
|- (x e. _V, y e. _V |-> C) = {<.<.x, y>., z>. | z = C}
Theorem	mptresid 5721*	The restricted identity expressed with the "maps to" notation. (Contributed by FL, 25-Apr-2012.)
|- (x e. A |-> x) = ( _I |` A)
Theorem	fvmptex 5722*	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 e. _V, B, (/)), and it is always a set by fvex 5340.) 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 e. A |-> B)   &   |- G = (x e. A |-> ( _I ` B))   =>   |- (F` C) = (G` C)
Theorem	fvmptf 5723*	Value of a function given by an ordered-pair class abstraction. This version of fvmptg 5699 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_xA   &   |- F/_xC   &   |- (x = A -> B = C)   &   |- F = (x e. D |-> B)   =>   |- ((A e. D /\ C e. V) -> (F` A) = C)
Theorem	fvmptnf 5724*	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 5725 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- F/_xA   &   |- F/_xC   &   |- (x = A -> B = C)   &   |- F = (x e. D |-> B)   =>   |- (-. C e. _V -> (F` A) = (/))
Theorem	fvmptn 5725*	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 5699. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
|- (x = D -> B = C)   &   |- F = (x e. A |-> B)   =>   |- (-. C e. _V -> (F` D) = (/))
Theorem	fvmptss2 5726*	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 = D -> B = C)   &   |- F = (x e. A |-> B)   =>   |- (F` D) C_ C
Theorem	f1od 5727*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
|- F = (x e. A |-> C)   &   |- ((ph /\ x e. A) -> C e. W)   &   |- ((ph /\ y e. B) -> D e. X)   &   |- (ph -> ((x e. A /\ y = C) <-> (y e. B /\ x = D)))   =>   |- (ph -> F:A-1-1-onto->B)
Theorem	f1o2d 5728*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
|- F = (x e. A |-> C)   &   |- ((ph /\ x e. A) -> C e. B)   &   |- ((ph /\ y e. B) -> D e. A)   &   |- ((ph /\ (x e. A /\ y e. B)) -> (x = D <-> y = C))   =>   |- (ph -> F:A-1-1-onto->B)
Theorem	dfswap3 5729*	Alternate definition of Swap as an operator abstraction. (Contributed by SF, 23-Feb-2015.)
|- Swap = {<.<.x, y>., z>. | z = <.y, x>.}
Theorem	dfswap4 5730*	Alternate definition of Swap as an operator mapping. (Contributed by SF, 23-Feb-2015.)
|- Swap = (x e. _V, y e. _V |-> <.y, x>.)
Theorem	fmpt2x 5731*	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 e. A, y e. B |-> C)   =>   |- (A.x e. A A.y e. B C e. D <-> F:U_x e. A ({x} X. B)-->D)
Theorem	fmpt2 5732*	Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = (x e. A, y e. B |-> C)   =>   |- (A.x e. A A.y e. B C e. D <-> F:(A X. B)-->D)
Theorem	fnmpt2 5733*	Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = (x e. A, y e. B |-> C)   =>   |- (A.x e. A A.y e. B C e. V -> F Fn (A X. B))
Theorem	fnmpt2i 5734*	Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = (x e. A, y e. B |-> C)   &   |- C e. _V   =>   |- F Fn (A X. B)
Theorem	dmmpt2 5735*	Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
|- F = (x e. A, y e. B |-> C)   &   |- C e. _V   =>   |- dom F = (A X. B)
2.3.10  Set construction lemmas
Syntax	ctxp 5736	Extend the definition of a class to include the tail cross product.
class (A (x) B)
Definition	df-txp 5737	Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5784 for membership. (Contributed by SF, 9-Feb-2015.)
|- (A (x) B) = ((`'1st o. A) i^i (`'2nd o. B))
Syntax	cpprod 5738	Extend the definition of a class to include the parallel product operation.
class PProd (A, B)
Definition	df-pprod 5739	Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)
|- PProd (A, B) = ((A o. 1st) (x) (B o. 2nd))
Syntax	cfix 5740	Extend the definition of a class to include the fixed points of a relationship.
class FixA
Definition	df-fix 5741	Define the fixed points of a relationship. (Contributed by SF, 9-Feb-2015.)
|- FixA = ran (A i^i _I )
Syntax	ccup 5742	Extend the definition of a class to include the cup function.
class Cup
Definition	df-cup 5743*	Define the cup function. (Contributed by SF, 9-Feb-2015.)
|- Cup = (x e. _V, y e. _V |-> (x u. y))
Syntax	cdisj 5744	Extend the definition of a class to include the disjoint relationship.
class Disj
Definition	df-disj 5745*	Define the relationship of all disjoint sets. (Contributed by SF, 9-Feb-2015.)
|- Disj = {<.x, y>. | (x i^i y) = (/)}
Syntax	caddcfn 5746	Extend the definition of a class to include the cardinal sum function.
class AddC
Definition	df-addcfn 5747*	Define the function representing cardinal sum. (Contributed by SF, 9-Feb-2015.)
|- AddC = (x e. _V, y e. _V |-> (x +o y))
Syntax	ccompose 5748	Extend the definition of a class to include the compostion function.
class Compose
Definition	df-compose 5749*	Define the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
|- Compose = (x e. _V, y e. _V |-> (x o. y))
Syntax	cins2 5750	Extend the definition of a class to include the second insertion operation.
class Ins2 A
Definition	df-ins2 5751	Define the second insertion operation. (Contributed by SF, 9-Feb-2015.)
|- Ins2 A = (_V (x) A)
Syntax	cins3 5752	Extend the definition of a class to include the third insertion operation.
class Ins3 A
Definition	df-ins3 5753	Define the third insertion operation. (Contributed by SF, 9-Feb-2015.)
|- Ins3 A = (A (x) _V)
Syntax	cimage 5754	Extend the definition of a class to include the image function.
class ImageA
Definition	df-image 5755	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 o. `' SI A))"1c)
Syntax	cins4 5756	Extend the definition of a class to include the fourth insertion operation.
class Ins4 A
Definition	df-ins4 5757	Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)
|- Ins4 A = (`'(1st (x) ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd)))"A)
Syntax	csi3 5758	Extend the definition of a class to include the triple singleton image.
class SI3 A
Definition	df-si3 5759	Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)
|- SI3 A = (( SI 1st (x) ( SI (1st o. 2nd) (x) SI (2nd o. 2nd)))"~P1 A)
Syntax	cfuns 5760	Extend the definition of a class to include the set of all functions.
class Funs
Definition	df-funs 5761	Define the class of all functions. (Contributed by SF, 9-Feb-2015.)
|- Funs = {f | Fun f}
Syntax	cfns 5762	Extend the definition of a class to include the function with domain relationship.
class Fns
Definition	df-fns 5763*	Define the function with domain relationship. (Contributed by SF, 9-Feb-2015.)
|- Fns = {<.f, a>. | f Fn a}
Syntax	ccross 5764	Extend the definition of a class to include the cross product function.
class Cross
Definition	df-cross 5765*	Define the cross product function. (Contributed by SF, 9-Feb-2015.)
|- Cross = (x e. _V, y e. _V |-> (x X. y))
Syntax	cpw1fn 5766	Extend the definition of a class to include the unit power class function.
class Pw1Fn
Definition	df-pw1fn 5767	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 e. 1c |-> ~P1 U.x)
Syntax	cfullfun 5768	Extend the definition of a class to include the full function operation.
class FullFun F
Definition	df-fullfun 5769	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 o. F) \ ( ∼ _I o. F)) u. ( ∼ dom (( _I o. F) \ ( ∼ _I o. F)) X. {(/)}))
Syntax	cdomfn 5770	Extend the definition of a class to include the domain function.
class Dom
Definition	df-domfn 5771	Define the domain function. This is a function wrapper for the domain operator. (Contributed by Scott Fenton, 9-Aug-2019.)
|- Dom = (x e. _V |-> dom x)
Syntax	cranfn 5772	Extend the definition of a class to include the range function.
class Ran
Definition	df-ranfn 5773	Define the range function. This is a function wrapper for the range operator. (Contributed by Scott Fenton, 9-Aug-2019.)
|- Ran = (x e. _V |-> ran x)
Theorem	brsnsi 5774	Binary relationship of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- ({A} SI R{B} <-> ARB)
Theorem	opsnelsi 5775	Ordered pair membership of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.{A}, {B}>. e. SI R <-> <.A, B>. e. R)
Theorem	brsnsi1 5776*	Binary relationship of a singleton to an arbitrary set in a singleton image. (Contributed by SF, 9-Mar-2015.)
|- A e. _V   =>   |- ({A} SI RB <-> E.x(B = {x} /\ ARx))
Theorem	brsnsi2 5777*	Binary relationship of an arbitrary set to a singleton in a singleton image. (Contributed by SF, 9-Mar-2015.)
|- A e. _V   =>   |- (B SI R{A} <-> E.x(B = {x} /\ xRA))
Theorem	brco1st 5778	Binary relationship of composition with 1st. (Contributed by SF, 9-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>.(R o. 1st)C <-> ARC)
Theorem	brco2nd 5779	Binary relationship of composition with 2nd. (Contributed by SF, 9-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>.(R o. 2nd)C <-> BRC)
Theorem	txpeq1 5780	Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (A = B -> (A (x) C) = (B (x) C))
Theorem	txpeq2 5781	Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (A = B -> (C (x) A) = (C (x) B))
Theorem	trtxp 5782	Trinary relationship over a tail cross product. (Contributed by SF, 13-Feb-2015.)
|- (A(R (x) S)<.B, C>. <-> (ARB /\ ASC))
Theorem	oteltxp 5783	Ordered triple membership in a tail cross product. (Contributed by SF, 13-Feb-2015.)
|- (<.A, <.B, C>.>. e. (R (x) S) <-> (<.A, B>. e. R /\ <.A, C>. e. S))
Theorem	brtxp 5784*	Binary relationship over a tail cross product. (Contributed by SF, 11-Feb-2015.)
|- (A(R (x) S)B <-> E.xE.y(B = <.x, y>. /\ ARx /\ ASy))
Theorem	txpexg 5785	The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
|- ((A e. V /\ B e. W) -> (A (x) B) e. _V)
Theorem	txpex 5786	The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A (x) B) e. _V
Theorem	restxp 5787	Restriction distributes over tail cross product. (Contributed by SF, 24-Feb-2015.)
|- ((A (x) B) |` C) = ((A |` C) (x) (B |` C))
Theorem	elfix 5788	Membership in the fixed points of a relationship. (Contributed by SF, 11-Feb-2015.)
|- (A e. FixR <-> ARA)
Theorem	fixexg 5789	The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
|- (R e. V -> FixR e. _V)
Theorem	fixex 5790	The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
|- R e. _V   =>   |- FixR e. _V
Theorem	op1st2nd 5791	Express equality to an ordered pair via 1st and 2nd. (Contributed by SF, 12-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- ((C1stA /\ C2ndB) <-> C = <.A, B>.)
Theorem	otelins2 5792	Ordered triple membership in Ins2. (Contributed by SF, 13-Feb-2015.)
|- B e. _V   =>   |- (<.A, <.B, C>.>. e. Ins2 R <-> <.A, C>. e. R)
Theorem	otelins3 5793	Ordered triple membership in Ins3. (Contributed by SF, 13-Feb-2015.)
|- C e. _V   =>   |- (<.A, <.B, C>.>. e. Ins3 R <-> <.A, B>. e. R)
Theorem	brimage 5794	Binary relationship over the image function. (Contributed by SF, 11-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (AImageRB <-> B = (R"A))
Theorem	oqelins4 5795	Ordered quadruple membership in Ins4. (Contributed by SF, 13-Feb-2015.)
|- D e. _V   =>   |- (<.A, <.B, <.C, D>.>.>. e. Ins4 R <-> <.A, <.B, C>.>. e. R)
Theorem	ins2exg 5796	Ins2 preserves sethood. (Contributed by SF, 9-Mar-2015.)
|- (A e. V -> Ins2 A e. _V)
Theorem	ins3exg 5797	Ins3 preserves sethood. (Contributed by SF, 22-Feb-2015.)
|- (A e. V -> Ins3 A e. _V)
Theorem	ins2ex 5798	Ins2 preserves sethood. (Contributed by SF, 12-Feb-2015.)
|- A e. _V   =>   |- Ins2 A e. _V
Theorem	ins3ex 5799	Ins3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
|- A e. _V   =>   |- Ins3 A e. _V
Theorem	ins4ex 5800	Ins4 preserves sethood. (Contributed by SF, 12-Feb-2015.)
|- A e. _V   =>   |- Ins4 A e. _V