P. 51 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iss 5001	A subclass of the identity function is the identity function restricted to its domain. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 13-Dec-2003.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (A C_ _I <-> A = ( _I |` dom A))
Theorem	resopab2 5002*	Restriction of a class abstraction of ordered pairs. (Contributed by set.mm contributors, 24-Aug-2007.)
|- (A C_ B -> ({<.x, y>. | (x e. B /\ ph)} |` A) = {<.x, y>. | (x e. A /\ ph)})
Theorem	dfres2 5003*	Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- (R |` A) = {<.x, y>. | (x e. A /\ xRy)}
Theorem	opabresid 5004*	The restricted identity expressed with the class builder. (Contributed by FL, 25-Apr-2012.)
|- {<.x, y>. | (x e. A /\ y = x)} = ( _I |` A)
Theorem	dmresi 5005	The domain of a restricted identity function. (Contributed by set.mm contributors, 27-Aug-2004.)
|- dom ( _I |` A) = A
Theorem	resid 5006	Any class restricted to the universe is itself. (Contributed by set.mm contributors, 16-Mar-2004.) (Revised by Scott Fenton, 18-Apr-2021.)
|- (A |` _V) = A
Theorem	resima 5007	A restriction to an image. (Contributed by set.mm contributors, 29-Sep-2004.)
|- ((A |` B)"B) = (A"B)
Theorem	resima2 5008	Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
|- (B C_ C -> ((A |` C)"B) = (A"B))
Theorem	imadmrn 5009	The image of the domain of a class is the range of the class. (Contributed by set.mm contributors, 14-Aug-1994.)
|- (A"dom A) = ran A
Theorem	imassrn 5010	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by set.mm contributors, 31-Mar-1995.)
|- (A"B) C_ ran A
Theorem	imai 5011	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by set.mm contributors, 30-Apr-1998.)
|- ( _I "A) = A
Theorem	rnresi 5012	The range of the restricted identity function. (Contributed by set.mm contributors, 27-Aug-2004.)
|- ran ( _I |` A) = A
Theorem	resiima 5013	The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.)
|- (B C_ A -> (( _I |` A)"B) = B)
Theorem	ima0 5014	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by set.mm contributors, 20-May-1998.)
|- (A"(/)) = (/)
Theorem	0ima 5015	Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|- ((/)"A) = (/)
Theorem	imadisj 5016	A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
|- ((A"B) = (/) <-> (dom A i^i B) = (/))
Theorem	cnvimass 5017	A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)
|- (`'A"B) C_ dom A
Theorem	cnvimarndm 5018	The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- (`'A"ran A) = dom A
Theorem	imasn 5019*	The image of a singleton. (Contributed by set.mm contributors, 9-Jan-2015.)
|- (R"{A}) = {y | ARy}
Theorem	elimasn 5020	Membership in an image of a singleton. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 15-Mar-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (C e. (A"{B}) <-> <.B, C>. e. A)
Theorem	eliniseg 5021	Membership in an initial segment. The idiom (`'A"{B}), meaning {x | xAB}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 28-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (C e. (`'A"{B}) <-> CAB)
Theorem	epini 5022	Any set is equal to its preimage under the converse epsilon relation. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- A e. _V   =>   |- (`' _E "{A}) = A
Theorem	iniseg 5023*	An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by set.mm contributors, 28-Apr-2004.)
|- (`'A"{B}) = {x | xAB}
Theorem	imass1 5024	Subset theorem for image. (Contributed by set.mm contributors, 16-Mar-2004.)
|- (A C_ B -> (A"C) C_ (B"C))
Theorem	imass2 5025	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by set.mm contributors, 22-Mar-1998.)
|- (A C_ B -> (C"A) C_ (C"B))
Theorem	ndmima 5026	The image of a singleton outside the domain is empty. (Contributed by set.mm contributors, 22-May-1998.)
|- (-. A e. dom B -> (B"{A}) = (/))
Theorem	cotr 5027*	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 27-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ((R o. R) C_ R <-> A.xA.yA.z((xRy /\ yRz) -> xRz))
Theorem	cnvsym 5028*	Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 28-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (`'R C_ R <-> A.xA.y(xRy -> yRx))
Theorem	intasym 5029*	Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 9-Sep-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ((R i^i `'R) C_ _I <-> A.xA.y((xRy /\ yRx) -> x = y))
Theorem	intirr 5030*	Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Revised by Andrew Salmon, 27-Aug-2011.)
|- ((R i^i _I ) = (/) <-> A.x -. xRx)
Theorem	cnvopab 5031*	The converse of a class abstraction of ordered pairs. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 11-Dec-2003.) (Revised by set.mm contributors, 27-Aug-2011.)
|- `'{<.x, y>. | ph} = {<.y, x>. | ph}
Theorem	cnv0 5032	The converse of the empty set. (Contributed by set.mm contributors, 6-Apr-1998.)
|- `'(/) = (/)
Theorem	cnvi 5033	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 26-Apr-1998.) (Revised by set.mm contributors, 27-Aug-2011.)
|- `' _I = _I
Theorem	cnvun 5034	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 27-Aug-2011.)
|- `'(A u. B) = (`'A u. `'B)
Theorem	cnvdif 5035	Distributive law for converse over set difference. (Contributed by set.mm contributors, 26-Jun-2014.)
|- `'(A \ B) = (`'A \ `'B)
Theorem	cnvin 5036	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by set.mm contributors, 26-Jun-2014.)
|- `'(A i^i B) = (`'A i^i `'B)
Theorem	rnun 5037	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by set.mm contributors, 24-Mar-1998.)
|- ran (A u. B) = (ran A u. ran B)
Theorem	rnin 5038	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by set.mm contributors, 15-Sep-2004.)
|- ran (A i^i B) C_ (ran A i^i ran B)
Theorem	rnuni 5039*	The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by set.mm contributors, 17-Mar-2004.)
|- ran U.A = U_x e. A ran x
Theorem	imaundi 5040	Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by set.mm contributors, 30-Sep-2002.)
|- (A"(B u. C)) = ((A"B) u. (A"C))
Theorem	imaundir 5041	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ((A u. B)"C) = ((A"C) u. (B"C))
Theorem	dminss 5042	An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising." (Contributed by set.mm contributors, 11-Aug-2004.)
|- (dom R i^i A) C_ (`'R"(R"A))
Theorem	imainss 5043	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by set.mm contributors, 11-Aug-2004.)
|- ((R"A) i^i B) C_ (R"(A i^i (`'R"B)))
Theorem	cnvxp 5044	The converse of a cross product. Exercise 11 of [Suppes] p. 67. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 14-Aug-1999.) (Revised by set.mm contributors, 27-Aug-2011.)
|- `'(A X. B) = (B X. A)
Theorem	xp0 5045	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by set.mm contributors, 12-Apr-2004.)
|- (A X. (/)) = (/)
Theorem	xpnz 5046	The cross product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by set.mm contributors, 30-Jun-2006.) (Revised by set.mm contributors, 19-Apr-2007.)
|- ((A =/= (/) /\ B =/= (/)) <-> (A X. B) =/= (/))
Theorem	xpeq0 5047	At least one member of an empty cross product is empty. (Contributed by set.mm contributors, 27-Aug-2006.)
|- ((A X. B) = (/) <-> (A = (/) \/ B = (/)))
Theorem	xpdisj1 5048	Cross products with disjoint sets are disjoint. (Contributed by set.mm contributors, 13-Sep-2004.)
|- ((A i^i B) = (/) -> ((A X. C) i^i (B X. D)) = (/))
Theorem	xpdisj2 5049	Cross products with disjoint sets are disjoint. (Contributed by set.mm contributors, 13-Sep-2004.)
|- ((A i^i B) = (/) -> ((C X. A) i^i (D X. B)) = (/))
Theorem	xpsndisj 5050	Cross products with two different singletons are disjoint. (Contributed by set.mm contributors, 28-Jul-2004.) (Revised by set.mm contributors, 3-Jun-2007.)
|- (B =/= D -> ((A X. {B}) i^i (C X. {D})) = (/))
Theorem	resdisj 5051	A double restriction to disjoint classes is the empty set. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 7-Oct-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ((A i^i B) = (/) -> ((C |` A) |` B) = (/))
Theorem	rnxp 5052	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by set.mm contributors, 12-Apr-2004.) (Revised by set.mm contributors, 9-Apr-2007.)
|- (A =/= (/) -> ran (A X. B) = B)
Theorem	dmxpss 5053	The domain of a cross product is a subclass of the first factor. (Contributed by set.mm contributors, 19-Mar-2007.)
|- dom (A X. B) C_ A
Theorem	rnxpss 5054	The range of a cross product is a subclass of the second factor. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 16-Jan-2006.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ran (A X. B) C_ B
Theorem	rnxpid 5055	The range of a square cross product. (Contributed by FL, 17-May-2010.)
|- ran (A X. A) = A
Theorem	ssxpb 5056	A cross-product subclass relationship is equivalent to the relationship for it components. (Contributed by set.mm contributors, 17-Dec-2008.)
|- ((A X. B) =/= (/) -> ((A X. B) C_ (C X. D) <-> (A C_ C /\ B C_ D)))
Theorem	xp11 5057	The cross product of nonempty classes is one-to-one. (Contributed by set.mm contributors, 31-May-2008.)
|- ((A =/= (/) /\ B =/= (/)) -> ((A X. B) = (C X. D) <-> (A = C /\ B = D)))
Theorem	xpcan 5058	Cancellation law for cross-product. (Contributed by set.mm contributors, 30-Aug-2011.)
|- (C =/= (/) -> ((C X. A) = (C X. B) <-> A = B))
Theorem	xpcan2 5059	Cancellation law for cross-product. (Contributed by set.mm contributors, 30-Aug-2011.)
|- (C =/= (/) -> ((A X. C) = (B X. C) <-> A = B))
Theorem	ssrnres 5060	Subset of the range of a restriction. (Contributed by set.mm contributors, 16-Jan-2006.)
|- (B C_ ran (C |` A) <-> ran (C i^i (A X. B)) = B)
Theorem	rninxp 5061*	Range of the intersection with a cross product. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 17-Jan-2006.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (ran (C i^i (A X. B)) = B <-> A.y e. B E.x e. A xCy)
Theorem	dminxp 5062*	Domain of the intersection with a cross product. (Contributed by set.mm contributors, 17-Jan-2006.)
|- (dom (C i^i (A X. B)) = A <-> A.x e. A E.y e. B xCy)
Theorem	cnvcnv 5063	The double converse of a class is the original class. (Contributed by Scott Fenton, 17-Apr-2021.)
|- `'`'R = R
Theorem	cnveqb 5064	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) (Revised by Scott Fenton, 17-Apr-2021.)
|- (A = B <-> `'A = `'B)
Theorem	dmsnn0 5065	The domain of a singleton is nonzero iff the singleton argument is a set. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Scott Fenton, 19-Apr-2021.)
|- (A e. _V <-> dom {A} =/= (/))
Theorem	rnsnn0 5066	The range of a singleton is nonzero iff the singleton argument is a set. (Contributed by set.mm contributors, 14-Dec-2008.) (Revised by Scott Fenton, 19-Apr-2021.)
|- (A e. _V <-> ran {A} =/= (/))
Theorem	dmsnopg 5067	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- (B e. V -> dom {<.A, B>.} = {A})
Theorem	dmsnopss 5068	The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B). (Contributed by Mario Carneiro, 30-Apr-2015.)
|- dom {<.A, B>.} C_ {A}
Theorem	dmpropg 5069	The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ((B e. V /\ D e. W) -> dom {<.A, B>., <.C, D>.} = {A, C})
Theorem	dmsnop 5070	The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- B e. _V   =>   |- dom {<.A, B>.} = {A}
Theorem	dmprop 5071	The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
|- B e. _V   &   |- D e. _V   =>   |- dom {<.A, B>., <.C, D>.} = {A, C}
Theorem	dmtpop 5072	The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
|- B e. _V   &   |- D e. _V   &   |- F e. _V   =>   |- dom {<.A, B>., <.C, D>., <.E, F>.} = {A, C, E}
Theorem	op1sta 5073	Extract the first member of an ordered pair. (Contributed by Raph Levien, 4-Dec-2003.)
|- A e. _V   &   |- B e. _V   =>   |- U.dom {<.A, B>.} = A
Theorem	cnvsn 5074	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.)
|- A e. _V   &   |- B e. _V   =>   |- `'{<.A, B>.} = {<.B, A>.}
Theorem	opswap 5075	Swap the members of an ordered pair. (Contributed by set.mm contributors, 14-Dec-2008.)
|- A e. _V   &   |- B e. _V   =>   |- U.`'{<.A, B>.} = <.B, A>.
Theorem	rnsnop 5076	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by set.mm contributors, 24-Jul-2004.)
|- A e. _V   =>   |- ran {<.A, B>.} = {B}
Theorem	op2nda 5077	Extract the second member of an ordered pair. (Contributed by set.mm contributors, 9-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- U.ran {<.A, B>.} = B
Theorem	cnvresima 5078	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
|- (`'(F |` A)"B) = ((`'F"B) i^i A)
Theorem	resdmres 5079	Restriction to the domain of a restriction. (Contributed by set.mm contributors, 8-Apr-2007.)
|- (A |` dom (A |` B)) = (A |` B)
Theorem	imadmres 5080	The image of the domain of a restriction. (Contributed by set.mm contributors, 8-Apr-2007.)
|- (A"dom (A |` B)) = (A"B)
Theorem	dfco2 5081*	Alternate definition of a class composition, using only one bound variable. (Contributed by set.mm contributors, 19-Dec-2008.)
|- (A o. B) = U_x e. _V ((`'B"{x}) X. (A"{x}))
Theorem	dfco2a 5082*	Generalization of dfco2 5081, where C can have any value between dom A i^i ran B and _V. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ((dom A i^i ran B) C_ C -> (A o. B) = U_x e. C ((`'B"{x}) X. (A"{x})))
Theorem	coundi 5083	Class composition distributes over union. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (A o. (B u. C)) = ((A o. B) u. (A o. C))
Theorem	coundir 5084	Class composition distributes over union. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
|- ((A u. B) o. C) = ((A o. C) u. (B o. C))
Theorem	cores 5085	Restricted first member of a class composition. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 12-Oct-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|- (ran B C_ C -> ((A |` C) o. B) = (A o. B))
Theorem	resco 5086	Associative law for the restriction of a composition. (Contributed by set.mm contributors, 12-Dec-2006.)
|- ((A o. B) |` C) = (A o. (B |` C))
Theorem	imaco 5087	Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
|- ((A o. B)"C) = (A"(B"C))
Theorem	rnco 5088	The range of the composition of two classes. (Contributed by set.mm contributors, 12-Dec-2006.)
|- ran (A o. B) = ran (A |` ran B)
Theorem	rnco2 5089	The range of the composition of two classes. (Contributed by set.mm contributors, 27-Mar-2008.)
|- ran (A o. B) = (A"ran B)
Theorem	dmco 5090	The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by set.mm contributors, 4-Feb-2004.)
|- dom (A o. B) = (`'B"dom A)
Theorem	coiun 5091*	Composition with an indexed union. (Contributed by set.mm contributors, 21-Dec-2008.)
|- (A o. U_x e. C B) = U_x e. C (A o. B)
Theorem	cores2 5092	Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by set.mm contributors, 11-Dec-2006.)
|- (dom A C_ C -> (A o. `'(`'B |` C)) = (A o. B))
Theorem	co02 5093	Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by set.mm contributors, 24-Apr-2004.)
|- (A o. (/)) = (/)
Theorem	co01 5094	Composition with the empty set. (Contributed by set.mm contributors, 24-Apr-2004.)
|- ((/) o. A) = (/)
Theorem	coi1 5095	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by set.mm contributors, 22-Apr-2004.) (Revised by Scott Fenton, 14-Apr-2021.)
|- (A o. _I ) = A
Theorem	coi2 5096	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by set.mm contributors, 22-Apr-2004.) (Revised by Scott Fenton, 17-Apr-2021.)
|- ( _I o. A) = A
Theorem	coires1 5097	Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Scott Fenton, 17-Apr-2021.)
|- (A o. ( _I |` B)) = (A |` B)
Theorem	coass 5098	Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by set.mm contributors, 27-Jan-1997.)
|- ((A o. B) o. C) = (A o. (B o. C))
Theorem	cnvtr 5099	A class is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) (Revised by Scott Fenton, 18-Apr-2021.)
|- ((R o. R) C_ R <-> (`'R o. `'R) C_ `'R)
Theorem	ssdmrn 5100	A class is included in the cross product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by set.mm contributors, 3-Aug-1994.) (Revised by Scott Fenton, 15-Apr-2021.)
|- A C_ (dom A X. ran A)