Theorem List for Intuitionistic Logic Explorer - 4901-5000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xpssres 4901 |
Restriction of a constant function (or other cross product). (Contributed
by Stefan O'Rear, 24-Jan-2015.)
|
|
|
Theorem | elres 4902* |
Membership in a restriction. (Contributed by Scott Fenton,
17-Mar-2011.)
|
|
|
Theorem | elsnres 4903* |
Memebership in restriction to a singleton. (Contributed by Scott
Fenton, 17-Mar-2011.)
|
|
|
Theorem | relssres 4904 |
Simplification law for restriction. (Contributed by NM,
16-Aug-1994.)
|
|
|
Theorem | resdm 4905 |
A relation restricted to its domain equals itself. (Contributed by NM,
12-Dec-2006.)
|
|
|
Theorem | resexg 4906 |
The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | resex 4907 |
The restriction of a set is a set. (Contributed by Jeff Madsen,
19-Jun-2011.)
|
|
|
Theorem | resindm 4908 |
When restricting a relation, intersecting with the domain of the relation
has no effect. (Contributed by FL, 6-Oct-2008.)
|
|
|
Theorem | resdmdfsn 4909 |
Restricting a relation to its domain without a set is the same as
restricting the relation to the universe without this set. (Contributed
by AV, 2-Dec-2018.)
|
|
|
Theorem | resopab 4910* |
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 5-Nov-2002.)
|
|
|
Theorem | resiexg 4911 |
The existence of a restricted identity function, proved without using
the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.)
|
|
|
Theorem | iss 4912 |
A subclass of the identity function is the identity function restricted
to its domain. (Contributed by NM, 13-Dec-2003.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | resopab2 4913* |
Restriction of a class abstraction of ordered pairs. (Contributed by
NM, 24-Aug-2007.)
|
|
|
Theorem | resmpt 4914* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
15-Jul-2013.)
|
|
|
Theorem | resmpt3 4915* |
Unconditional restriction of the mapping operation. (Contributed by
Stefan O'Rear, 24-Jan-2015.) (Proof shortened by Mario Carneiro,
22-Mar-2015.)
|
|
|
Theorem | resmptf 4916 |
Restriction of the mapping operation. (Contributed by Thierry Arnoux,
28-Mar-2017.)
|
|
|
Theorem | resmptd 4917* |
Restriction of the mapping operation, deduction form. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | dfres2 4918* |
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5-Nov-2013.)
|
|
|
Theorem | opabresid 4919* |
The restricted identity expressed with the class builder. (Contributed
by FL, 25-Apr-2012.)
|
|
|
Theorem | mptresid 4920* |
The restricted identity expressed with the maps-to notation.
(Contributed by FL, 25-Apr-2012.)
|
|
|
Theorem | dmresi 4921 |
The domain of a restricted identity function. (Contributed by NM,
27-Aug-2004.)
|
|
|
Theorem | resid 4922 |
Any relation restricted to the universe is itself. (Contributed by NM,
16-Mar-2004.)
|
|
|
Theorem | imaeq1 4923 |
Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | imaeq2 4924 |
Equality theorem for image. (Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | imaeq1i 4925 |
Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|
|
|
Theorem | imaeq2i 4926 |
Equality theorem for image. (Contributed by NM, 21-Dec-2008.)
|
|
|
Theorem | imaeq1d 4927 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
|
|
Theorem | imaeq2d 4928 |
Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
|
|
|
Theorem | imaeq12d 4929 |
Equality theorem for image. (Contributed by Mario Carneiro,
4-Dec-2016.)
|
|
|
Theorem | dfima2 4930* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | dfima3 4931* |
Alternate definition of image. Compare definition (d) of [Enderton]
p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | elimag 4932* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 20-Jan-2007.)
|
|
|
Theorem | elima 4933* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 19-Apr-2004.)
|
|
|
Theorem | elima2 4934* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 11-Aug-2004.)
|
|
|
Theorem | elima3 4935* |
Membership in an image. Theorem 34 of [Suppes]
p. 65. (Contributed by
NM, 14-Aug-1994.)
|
|
|
Theorem | nfima 4936 |
Bound-variable hypothesis builder for image. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | nfimad 4937 |
Deduction version of bound-variable hypothesis builder nfima 4936.
(Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
|
|
Theorem | imadmrn 4938 |
The image of the domain of a class is the range of the class.
(Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | imassrn 4939 |
The image of a class is a subset of its range. Theorem 3.16(xi) of
[Monk1] p. 39. (Contributed by NM,
31-Mar-1995.)
|
|
|
Theorem | imaexg 4940 |
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed
by NM, 24-Jul-1995.)
|
|
|
Theorem | imaex 4941 |
The image of a set is a set. Theorem 3.17 of [Monk1] p. 39.
(Contributed by JJ, 24-Sep-2021.)
|
|
|
Theorem | imai 4942 |
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by NM, 30-Apr-1998.)
|
|
|
Theorem | rnresi 4943 |
The range of the restricted identity function. (Contributed by NM,
27-Aug-2004.)
|
|
|
Theorem | resiima 4944 |
The image of a restriction of the identity function. (Contributed by FL,
31-Dec-2006.)
|
|
|
Theorem | ima0 4945 |
Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed
by NM, 20-May-1998.)
|
|
|
Theorem | 0ima 4946 |
Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|
|
|
Theorem | csbima12g 4947 |
Move class substitution in and out of the image of a function.
(Contributed by FL, 15-Dec-2006.) (Proof shortened by Mario Carneiro,
4-Dec-2016.)
|
|
|
Theorem | imadisj 4948 |
A class whose image under another is empty is disjoint with the other's
domain. (Contributed by FL, 24-Jan-2007.)
|
|
|
Theorem | cnvimass 4949 |
A preimage under any class is included in the domain of the class.
(Contributed by FL, 29-Jan-2007.)
|
|
|
Theorem | cnvimarndm 4950 |
The preimage of the range of a class is the domain of the class.
(Contributed by Jeff Hankins, 15-Jul-2009.)
|
|
|
Theorem | imasng 4951* |
The image of a singleton. (Contributed by NM, 8-May-2005.)
|
|
|
Theorem | elreimasng 4952 |
Elementhood in the image of a singleton. (Contributed by Jim Kingdon,
10-Dec-2018.)
|
|
|
Theorem | elimasn 4953 |
Membership in an image of a singleton. (Contributed by NM,
15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | elimasng 4954 |
Membership in an image of a singleton. (Contributed by Raph Levien,
21-Oct-2006.)
|
|
|
Theorem | args 4955* |
Two ways to express the class of unique-valued arguments of ,
which is the same as the domain of whenever is a function.
The left-hand side of the equality is from Definition 10.2 of [Quine]
p. 65. Quine uses the notation "arg " for this class (for which
we have no separate notation). (Contributed by NM, 8-May-2005.)
|
|
|
Theorem | eliniseg 4956 |
Membership in an initial segment. The idiom ,
meaning , is used to specify an initial segment in
(for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by
NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | epini 4957 |
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9-Mar-2013.)
|
|
|
Theorem | iniseg 4958* |
An idiom that signifies an initial segment of an ordering, used, for
example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by
NM, 28-Apr-2004.)
|
|
|
Theorem | dfse2 4959* |
Alternate definition of set-like relation. (Contributed by Mario
Carneiro, 23-Jun-2015.)
|
Se
|
|
Theorem | exse2 4960 |
Any set relation is set-like. (Contributed by Mario Carneiro,
22-Jun-2015.)
|
Se |
|
Theorem | imass1 4961 |
Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
|
|
|
Theorem | imass2 4962 |
Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
(Contributed by NM, 22-Mar-1998.)
|
|
|
Theorem | ndmima 4963 |
The image of a singleton outside the domain is empty. (Contributed by NM,
22-May-1998.)
|
|
|
Theorem | relcnv 4964 |
A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed
by NM, 29-Oct-1996.)
|
|
|
Theorem | relbrcnvg 4965 |
When is a relation,
the sethood assumptions on brcnv 4769 can be
omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|
|
|
Theorem | relbrcnv 4966 |
When is a relation,
the sethood assumptions on brcnv 4769 can be
omitted. (Contributed by Mario Carneiro, 28-Apr-2015.)
|
|
|
Theorem | cotr 4967* |
Two ways of saying a relation is transitive. Definition of transitivity
in [Schechter] p. 51. (Contributed by
NM, 27-Dec-1996.) (Proof
shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | issref 4968* |
Two ways to state a relation is reflexive. Adapted from Tarski.
(Contributed by FL, 15-Jan-2012.) (Revised by NM, 30-Mar-2016.)
|
|
|
Theorem | cnvsym 4969* |
Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51.
(Contributed by NM, 28-Dec-1996.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | intasym 4970* |
Two ways of saying a relation is antisymmetric. Definition of
antisymmetry in [Schechter] p. 51.
(Contributed by NM, 9-Sep-2004.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | asymref 4971* |
Two ways of saying a relation is antisymmetric and reflexive.
is the field of a relation by relfld 5114. (Contributed by
NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | intirr 4972* |
Two ways of saying a relation is irreflexive. Definition of
irreflexivity in [Schechter] p. 51.
(Contributed by NM, 9-Sep-2004.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | brcodir 4973* |
Two ways of saying that two elements have an upper bound. (Contributed
by Mario Carneiro, 3-Nov-2015.)
|
|
|
Theorem | codir 4974* |
Two ways of saying a relation is directed. (Contributed by Mario
Carneiro, 22-Nov-2013.)
|
|
|
Theorem | qfto 4975* |
A quantifier-free way of expressing the total order predicate.
(Contributed by Mario Carneiro, 22-Nov-2013.)
|
|
|
Theorem | xpidtr 4976 |
A square cross product is a transitive relation.
(Contributed by FL, 31-Jul-2009.)
|
|
|
Theorem | trin2 4977 |
The intersection of two transitive classes is transitive. (Contributed
by FL, 31-Jul-2009.)
|
|
|
Theorem | poirr2 4978 |
A partial order relation is irreflexive. (Contributed by Mario
Carneiro, 2-Nov-2015.)
|
|
|
Theorem | trinxp 4979 |
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.)
|
|
|
Theorem | soirri 4980 |
A strict order relation is irreflexive. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | sotri 4981 |
A strict order relation is a transitive relation. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | son2lpi 4982 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | sotri2 4983 |
A transitivity relation. (Read B < A and B < C implies A < C .)
(Contributed by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | sotri3 4984 |
A transitivity relation. (Read A < B and C < B implies A < C .)
(Contributed by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | poleloe 4985 |
Express "less than or equals" for general strict orders.
(Contributed by
Stefan O'Rear, 17-Jan-2015.)
|
|
|
Theorem | poltletr 4986 |
Transitive law for general strict orders. (Contributed by Stefan O'Rear,
17-Jan-2015.)
|
|
|
Theorem | cnvopab 4987* |
The converse of a class abstraction of ordered pairs. (Contributed by
NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | mptcnv 4988* |
The converse of a mapping function. (Contributed by Thierry Arnoux,
16-Jan-2017.)
|
|
|
Theorem | cnv0 4989 |
The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|
|
|
Theorem | cnvi 4990 |
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.)
|
|
|
Theorem | cnvun 4991 |
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.)
|
|
|
Theorem | cnvdif 4992 |
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26-Jun-2014.)
|
|
|
Theorem | cnvin 4993 |
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.)
|
|
|
Theorem | rnun 4994 |
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by NM, 24-Mar-1998.)
|
|
|
Theorem | rnin 4995 |
The range of an intersection belongs the intersection of ranges. Theorem
9 of [Suppes] p. 60. (Contributed by NM,
15-Sep-2004.)
|
|
|
Theorem | rniun 4996 |
The range of an indexed union. (Contributed by Mario Carneiro,
29-May-2015.)
|
|
|
Theorem | rnuni 4997* |
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.)
|
|
|
Theorem | imaundi 4998 |
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30-Sep-2002.)
|
|
|
Theorem | imaundir 4999 |
The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|
|
|
Theorem | dminss 5000 |
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.)
|
|