P. 51 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpidtr 5001	A square cross product ( A X. A ) is a transitive relation. (Contributed by FL, 31-Jul-2009.)
|- ( ( A X. A ) o. ( A X. A ) ) C_ ( A X. A )
Theorem	trin2 5002	The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.)
|- ( ( ( R o. R ) C_ R /\ ( S o. S ) C_ S ) -> ( ( R i^i S ) o. ( R i^i S ) ) C_ ( R i^i S ) )
Theorem	poirr2 5003	A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.)
|- ( R Po A -> ( R i^i ( _I |` A ) ) = (/) )
Theorem	trinxp 5004	The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a square cross product is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.)
|- ( ( R o. R ) C_ R -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ ( R i^i ( A X. A ) ) )
Theorem	soirri 5005	A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- -. A R A
Theorem	sotri 5006	A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- ( ( A R B /\ B R C ) -> A R C )
Theorem	son2lpi 5007	A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- -. ( A R B /\ B R A )
Theorem	sotri2 5008	A transitivity relation. (Read -. B < A and B < C implies A < C .) (Contributed by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- ( ( A e. S /\ -. B R A /\ B R C ) -> A R C )
Theorem	sotri3 5009	A transitivity relation. (Read A < B and -. C < B implies A < C .) (Contributed by Mario Carneiro, 10-May-2013.)
|- R Or S   &    |- R C_ ( S X. S )   =>    |- ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )
Theorem	poleloe 5010	Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( B e. V -> ( A ( R u. _I ) B <-> ( A R B \/ A = B ) ) )
Theorem	poltletr 5011	Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.)
|- ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B ( R u. _I ) C ) -> A R C ) )
Theorem	cnvopab 5012*	The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' { <. x , y >. | ph } = { <. y , x >. | ph }
Theorem	mptcnv 5013*	The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
|- ( ph -> ( ( x e. A /\ y = B ) <-> ( y e. C /\ x = D ) ) )   =>    |- ( ph -> `' ( x e. A |-> B ) = ( y e. C |-> D ) )
Theorem	cnv0 5014	The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|- `' (/) = (/)
Theorem	cnvi 5015	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' _I = _I
Theorem	cnvun 5016	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' ( A u. B ) = ( `' A u. `' B )
Theorem	cnvdif 5017	Distributive law for converse over set difference. (Contributed by Mario Carneiro, 26-Jun-2014.)
|- `' ( A \ B ) = ( `' A \ `' B )
Theorem	cnvin 5018	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro, 26-Jun-2014.)
|- `' ( A i^i B ) = ( `' A i^i `' B )
Theorem	rnun 5019	Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)
|- ran ( A u. B ) = ( ran A u. ran B )
Theorem	rnin 5020	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)
|- ran ( A i^i B ) C_ ( ran A i^i ran B )
Theorem	rniun 5021	The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.)
|- ran U_ x e. A B = U_ x e. A ran B
Theorem	rnuni 5022*	The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro, 29-May-2015.)
|- ran U. A = U_ x e. A ran x
Theorem	imaundi 5023	Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
|- ( A " ( B u. C ) ) = ( ( A " B ) u. ( A " C ) )
Theorem	imaundir 5024	The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )
Theorem	dminss 5025	An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising". (Contributed by NM, 11-Aug-2004.)
|- ( dom R i^i A ) C_ ( `' R " ( R " A ) )
Theorem	imainss 5026	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.)
|- ( ( R " A ) i^i B ) C_ ( R " ( A i^i ( `' R " B ) ) )
Theorem	inimass 5027	The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i B ) " C ) C_ ( ( A " C ) i^i ( B " C ) )
Theorem	inimasn 5028	The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( C e. V -> ( ( A i^i B ) " { C } ) = ( ( A " { C } ) i^i ( B " { C } ) ) )
Theorem	cnvxp 5029	The converse of a cross product. Exercise 11 of [Suppes] p. 67. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- `' ( A X. B ) = ( B X. A )
Theorem	xp0 5030	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.)
|- ( A X. (/) ) = (/)
Theorem	xpmlem 5031*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 11-Dec-2018.)
|- ( ( E. x x e. A /\ E. y y e. B ) <-> E. z z e. ( A X. B ) )
Theorem	xpm 5032*	The cross product of inhabited classes is inhabited. (Contributed by Jim Kingdon, 13-Dec-2018.)
|- ( ( E. x x e. A /\ E. y y e. B ) <-> E. z z e. ( A X. B ) )
Theorem	xpeq0r 5033	A cross product is empty if at least one member is empty. (Contributed by Jim Kingdon, 12-Dec-2018.)
|- ( ( A = (/) \/ B = (/) ) -> ( A X. B ) = (/) )
Theorem	sqxpeq0 5034	A Cartesian square is empty iff its member is empty. (Contributed by Jim Kingdon, 21-Apr-2023.)
|- ( ( A X. A ) = (/) <-> A = (/) )
Theorem	xpdisj1 5035	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
|- ( ( A i^i B ) = (/) -> ( ( A X. C ) i^i ( B X. D ) ) = (/) )
Theorem	xpdisj2 5036	Cross products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.)
|- ( ( A i^i B ) = (/) -> ( ( C X. A ) i^i ( D X. B ) ) = (/) )
Theorem	xpsndisj 5037	Cross products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.)
|- ( B =/= D -> ( ( A X. { B } ) i^i ( C X. { D } ) ) = (/) )
Theorem	djudisj 5038*	Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|- ( ( A i^i B ) = (/) -> ( U_ x e. A ( { x } X. C ) i^i U_ y e. B ( { y } X. D ) ) = (/) )
Theorem	resdisj 5039	A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ( A i^i B ) = (/) -> ( ( C |` A ) |` B ) = (/) )
Theorem	rnxpm 5040*	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37, with nonempty changed to inhabited. (Contributed by Jim Kingdon, 12-Dec-2018.)
|- ( E. x x e. A -> ran ( A X. B ) = B )
Theorem	dmxpss 5041	The domain of a cross product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.)
|- dom ( A X. B ) C_ A
Theorem	rnxpss 5042	The range of a cross product is a subclass of the second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ran ( A X. B ) C_ B
Theorem	dmxpss2 5043	Upper bound for the domain of a binary relation. (Contributed by BJ, 10-Jul-2022.)
|- ( R C_ ( A X. B ) -> dom R C_ A )
Theorem	rnxpss2 5044	Upper bound for the range of a binary relation. (Contributed by BJ, 10-Jul-2022.)
|- ( R C_ ( A X. B ) -> ran R C_ B )
Theorem	rnxpid 5045	The range of a square cross product. (Contributed by FL, 17-May-2010.)
|- ran ( A X. A ) = A
Theorem	ssxpbm 5046*	A cross-product subclass relationship is equivalent to the relationship for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
|- ( E. x x e. ( A X. B ) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) )
Theorem	ssxp1 5047*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
|- ( E. x x e. C -> ( ( A X. C ) C_ ( B X. C ) <-> A C_ B ) )
Theorem	ssxp2 5048*	Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
|- ( E. x x e. C -> ( ( C X. A ) C_ ( C X. B ) <-> A C_ B ) )
Theorem	xp11m 5049*	The cross product of inhabited classes is one-to-one. (Contributed by Jim Kingdon, 13-Dec-2018.)
|- ( ( E. x x e. A /\ E. y y e. B ) -> ( ( A X. B ) = ( C X. D ) <-> ( A = C /\ B = D ) ) )
Theorem	xpcanm 5050*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
|- ( E. x x e. C -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
Theorem	xpcan2m 5051*	Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
|- ( E. x x e. C -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
Theorem	xpexr2m 5052*	If a nonempty cross product is a set, so are both of its components. (Contributed by Jim Kingdon, 14-Dec-2018.)
|- ( ( ( A X. B ) e. C /\ E. x x e. ( A X. B ) ) -> ( A e. _V /\ B e. _V ) )
Theorem	ssrnres 5053	Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)
|- ( B C_ ran ( C |` A ) <-> ran ( C i^i ( A X. B ) ) = B )
Theorem	rninxp 5054*	Range of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( ran ( C i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x C y )
Theorem	dminxp 5055*	Domain of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.)
|- ( dom ( C i^i ( A X. B ) ) = A <-> A. x e. A E. y e. B x C y )
Theorem	imainrect 5056	Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
|- ( ( G i^i ( A X. B ) ) " Y ) = ( ( G " ( Y i^i A ) ) i^i B )
Theorem	xpima1 5057	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) )
Theorem	xpima2m 5058*	The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( E. x x e. ( A i^i C ) -> ( ( A X. B ) " C ) = B )
Theorem	xpimasn 5059	The image of a singleton by a cross product. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- ( X e. A -> ( ( A X. B ) " { X } ) = B )
Theorem	cnvcnv3 5060*	The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- `' `' R = { <. x , y >. | x R y }
Theorem	dfrel2 5061	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
|- ( Rel R <-> `' `' R = R )
Theorem	dfrel4v 5062*	A relation can be expressed as the set of ordered pairs in it. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- ( Rel R <-> R = { <. x , y >. | x R y } )
Theorem	cnvcnv 5063	The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.)
|- `' `' A = ( A i^i ( _V X. _V ) )
Theorem	cnvcnv2 5064	The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
|- `' `' A = ( A |` _V )
Theorem	cnvcnvss 5065	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
|- `' `' A C_ A
Theorem	cnveqb 5066	Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )
Theorem	cnveq0 5067	A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
|- ( Rel A -> ( A = (/) <-> `' A = (/) ) )
Theorem	dfrel3 5068	Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|- ( Rel R <-> ( R |` _V ) = R )
Theorem	dmresv 5069	The domain of a universal restriction. (Contributed by NM, 14-May-2008.)
|- dom ( A |` _V ) = dom A
Theorem	rnresv 5070	The range of a universal restriction. (Contributed by NM, 14-May-2008.)
|- ran ( A |` _V ) = ran A
Theorem	dfrn4 5071	Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|- ran A = ( A " _V )
Theorem	csbrng 5072	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )
Theorem	rescnvcnv 5073	The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( `' `' A |` B ) = ( A |` B )
Theorem	cnvcnvres 5074	The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
|- `' `' ( A |` B ) = ( `' `' A |` B )
Theorem	imacnvcnv 5075	The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
|- ( `' `' A " B ) = ( A " B )
Theorem	dmsnm 5076*	The domain of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
|- ( A e. ( _V X. _V ) <-> E. x x e. dom { A } )
Theorem	rnsnm 5077*	The range of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
|- ( A e. ( _V X. _V ) <-> E. x x e. ran { A } )
Theorem	dmsn0 5078	The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)
|- dom { (/) } = (/)
Theorem	cnvsn0 5079	The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- `' { (/) } = (/)
Theorem	dmsn0el 5080	The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.)
|- ( (/) e. A -> dom { A } = (/) )
Theorem	relsn2m 5081*	A singleton is a relation iff it has an inhabited domain. (Contributed by Jim Kingdon, 16-Dec-2018.)
|- A e. _V   =>    |- ( Rel { A } <-> E. x x e. dom { A } )
Theorem	dmsnopg 5082	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	dmpropg 5083	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 5084	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 5085	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 5086	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	cnvcnvsn 5087	Double converse of a singleton of an ordered pair. (Unlike cnvsn 5093, this does not need any sethood assumptions on A and B.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- `' `' { <. A , B >. } = `' { <. B , A >. }
Theorem	dmsnsnsng 5088	The domain of the singleton of the singleton of a singleton. (Contributed by Jim Kingdon, 16-Dec-2018.)
|- ( A e. _V -> dom { { { A } } } = { A } )
Theorem	rnsnopg 5089	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( A e. V -> ran { <. A , B >. } = { B } )
Theorem	rnpropg 5090	The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
|- ( ( A e. V /\ B e. W ) -> ran { <. A , C >. , <. B , D >. } = { C , D } )
Theorem	rnsnop 5091	The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   =>    |- ran { <. A , B >. } = { B }
Theorem	op1sta 5092	Extract the first member of an ordered pair. (See op2nda 5095 to extract the second member and op1stb 4463 for an alternate version.) (Contributed by Raph Levien, 4-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- U. dom { <. A , B >. } = A
Theorem	cnvsn 5093	Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- `' { <. A , B >. } = { <. B , A >. }
Theorem	op2ndb 5094	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4463 to extract the first member and op2nda 5095 for an alternate version.) (Contributed by NM, 25-Nov-2003.)
|- A e. _V   &    |- B e. _V   =>    |- |^| |^| |^| `' { <. A , B >. } = B
Theorem	op2nda 5095	Extract the second member of an ordered pair. (See op1sta 5092 to extract the first member and op2ndb 5094 for an alternate version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- A e. _V   &    |- B e. _V   =>    |- U. ran { <. A , B >. } = B
Theorem	cnvsng 5096	Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.)
|- ( ( A e. V /\ B e. W ) -> `' { <. A , B >. } = { <. B , A >. } )
Theorem	opswapg 5097	Swap the members of an ordered pair. (Contributed by Jim Kingdon, 16-Dec-2018.)
|- ( ( A e. V /\ B e. W ) -> U. `' { <. A , B >. } = <. B , A >. )
Theorem	elxp4 5098	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 5099. (Contributed by NM, 17-Feb-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. U. dom { A } , U. ran { A } >. /\ ( U. dom { A } e. B /\ U. ran { A } e. C ) ) )
Theorem	elxp5 5099	Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 5098 when the double intersection does not create class existence problems (caused by int0 3845). (Contributed by NM, 1-Aug-2004.)
|- ( A e. ( B X. C ) <-> ( A = <. |^| |^| A , U. ran { A } >. /\ ( |^| |^| A e. B /\ U. ran { A } e. C ) ) )
Theorem	cnvresima 5100	An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
|- ( `' ( F |` A ) " B ) = ( ( `' F " B ) i^i A )