Theorem List for Intuitionistic Logic Explorer - 4401-4500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | brrelex2 4401 |
A true binary relation on a relation implies the second argument is a set.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brrelexi 4402 |
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
|
|
|
Theorem | brrelex2i 4403 |
The second argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | nprrel 4404 |
No proper class is related to anything via any relation. (Contributed
by Roy F. Longton, 30-Jul-2005.)
|
|
|
Theorem | fconstmpt 4405* |
Representation of a constant function using the mapping operation.
(Note that
cannot appear free in .) (Contributed by NM,
12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
|
|
Theorem | vtoclr 4406* |
Variable to class conversion of transitive relation. (Contributed by
NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opelvvg 4407 |
Ordered pair membership in the universal class of ordered pairs.
(Contributed by Mario Carneiro, 3-May-2015.)
|
|
|
Theorem | opelvv 4408 |
Ordered pair membership in the universal class of ordered pairs.
(Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | opthprc 4409 |
Justification theorem for an ordered pair definition that works for any
classes, including proper classes. This is a possible definition
implied by the footnote in [Jech] p. 78,
which says, "The sophisticated
reader will not object to our use of a pair of classes."
(Contributed
by NM, 28-Sep-2003.)
|
|
|
Theorem | brel 4410 |
Two things in a binary relation belong to the relation's domain.
(Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | brab2a 4411* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 9-Nov-2015.)
|
|
|
Theorem | elxp3 4412* |
Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
|
|
|
Theorem | opeliunxp 4413 |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|
|
|
Theorem | xpundi 4414 |
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12-Aug-2004.)
|
|
|
Theorem | xpundir 4415 |
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30-Sep-2002.)
|
|
|
Theorem | xpiundi 4416* |
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27-Apr-2014.)
|
|
|
Theorem | xpiundir 4417* |
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27-Apr-2014.)
|
|
|
Theorem | iunxpconst 4418* |
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | xpun 4419 |
The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
|
|
|
Theorem | elvv 4420* |
Membership in universal class of ordered pairs. (Contributed by NM,
4-Jul-1994.)
|
|
|
Theorem | elvvv 4421* |
Membership in universal class of ordered triples. (Contributed by NM,
17-Dec-2008.)
|
|
|
Theorem | elvvuni 4422 |
An ordered pair contains its union. (Contributed by NM,
16-Sep-2006.)
|
|
|
Theorem | mosubopt 4423* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-Aug-2007.)
|
|
|
Theorem | mosubop 4424* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-May-1995.)
|
|
|
Theorem | brinxp2 4425 |
Intersection of binary relation with cross product. (Contributed by NM,
3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brinxp 4426 |
Intersection of binary relation with cross product. (Contributed by NM,
9-Mar-1997.)
|
|
|
Theorem | poinxp 4427 |
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
|
|
Theorem | soinxp 4428 |
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
|
|
Theorem | seinxp 4429 |
Intersection of set-like relation with cross product of its field.
(Contributed by Mario Carneiro, 22-Jun-2015.)
|
Se
Se |
|
Theorem | posng 4430 |
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
|
|
Theorem | sosng 4431 |
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
|
|
Theorem | opabssxp 4432* |
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16-Jul-1995.)
|
|
|
Theorem | brab2ga 4433* |
The law of concretion for a binary relation. See brab2a 4411 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|
|
|
Theorem | optocl 4434* |
Implicit substitution of class for ordered pair. (Contributed by NM,
5-Mar-1995.)
|
|
|
Theorem | 2optocl 4435* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
|
|
Theorem | 3optocl 4436* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
|
|
Theorem | opbrop 4437* |
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5-Aug-1995.)
|
|
|
Theorem | 0xp 4438 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
4-Jul-1994.)
|
|
|
Theorem | csbxpg 4439 |
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | releq 4440 |
Equality theorem for the relation predicate. (Contributed by NM,
1-Aug-1994.)
|
|
|
Theorem | releqi 4441 |
Equality inference for the relation predicate. (Contributed by NM,
8-Dec-2006.)
|
|
|
Theorem | releqd 4442 |
Equality deduction for the relation predicate. (Contributed by NM,
8-Mar-2014.)
|
|
|
Theorem | nfrel 4443 |
Bound-variable hypothesis builder for a relation. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | sbcrel 4444 |
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23-Jul-2017.)
|
|
|
Theorem | relss 4445 |
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15-Aug-1994.)
|
|
|
Theorem | ssrel 4446* |
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
(Contributed by NM, 2-Aug-1994.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | eqrel 4447* |
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | ssrel2 4448* |
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4446 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25-Jan-2018.)
|
|
|
Theorem | relssi 4449* |
Inference from subclass principle for relations. (Contributed by NM,
31-Mar-1998.)
|
|
|
Theorem | relssdv 4450* |
Deduction from subclass principle for relations. (Contributed by NM,
11-Sep-2004.)
|
|
|
Theorem | eqrelriv 4451* |
Inference from extensionality principle for relations. (Contributed by
FL, 15-Oct-2012.)
|
|
|
Theorem | eqrelriiv 4452* |
Inference from extensionality principle for relations. (Contributed by
NM, 17-Mar-1995.)
|
|
|
Theorem | eqbrriv 4453* |
Inference from extensionality principle for relations. (Contributed by
NM, 12-Dec-2006.)
|
|
|
Theorem | eqrelrdv 4454* |
Deduce equality of relations from equivalence of membership.
(Contributed by Rodolfo Medina, 10-Oct-2010.)
|
|
|
Theorem | eqbrrdv 4455* |
Deduction from extensionality principle for relations. (Contributed by
Mario Carneiro, 3-Jan-2017.)
|
|
|
Theorem | eqbrrdiv 4456* |
Deduction from extensionality principle for relations. (Contributed by
Rodolfo Medina, 10-Oct-2010.)
|
|
|
Theorem | eqrelrdv2 4457* |
A version of eqrelrdv 4454. (Contributed by Rodolfo Medina,
10-Oct-2010.)
|
|
|
Theorem | ssrelrel 4458* |
A subclass relationship determined by ordered triples. Use relrelss 4864
to express the antecedent in terms of the relation predicate.
(Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
|
|
Theorem | eqrelrel 4459* |
Extensionality principle for ordered triples, analogous to eqrel 4447.
Use relrelss 4864 to express the antecedent in terms of the
relation
predicate. (Contributed by NM, 17-Dec-2008.)
|
|
|
Theorem | elrel 4460* |
A member of a relation is an ordered pair. (Contributed by NM,
17-Sep-2006.)
|
|
|
Theorem | relsn 4461 |
A singleton is a relation iff it is an ordered pair. (Contributed by
NM, 24-Sep-2013.)
|
|
|
Theorem | relsnop 4462 |
A singleton of an ordered pair is a relation. (Contributed by NM,
17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | xpss12 4463 |
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52. (Contributed by NM,
26-Aug-1995.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
|
|
Theorem | xpss 4464 |
A cross product is included in the ordered pair universe. Exercise 3 of
[TakeutiZaring] p. 25. (Contributed
by NM, 2-Aug-1994.)
|
|
|
Theorem | relxp 4465 |
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
(Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | xpss1 4466 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
|
|
Theorem | xpss2 4467 |
Subset relation for cross product. (Contributed by Jeff Hankins,
30-Aug-2009.)
|
|
|
Theorem | xpsspw 4468 |
A cross product is included in the power of the power of the union of
its arguments. (Contributed by NM, 13-Sep-2006.)
|
|
|
Theorem | unixpss 4469 |
The double class union of a cross product is included in the union of its
arguments. (Contributed by NM, 16-Sep-2006.)
|
|
|
Theorem | xpexg 4470 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. (Contributed
by NM, 14-Aug-1994.)
|
|
|
Theorem | xpex 4471 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
(Contributed by NM, 14-Aug-1994.)
|
|
|
Theorem | relun 4472 |
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25. (Contributed
by NM, 12-Aug-1994.)
|
|
|
Theorem | relin1 4473 |
The intersection with a relation is a relation. (Contributed by NM,
16-Aug-1994.)
|
|
|
Theorem | relin2 4474 |
The intersection with a relation is a relation. (Contributed by NM,
17-Jan-2006.)
|
|
|
Theorem | reldif 4475 |
A difference cutting down a relation is a relation. (Contributed by NM,
31-Mar-1998.)
|
|
|
Theorem | reliun 4476 |
An indexed union is a relation iff each member of its indexed family is
a relation. (Contributed by NM, 19-Dec-2008.)
|
|
|
Theorem | reliin 4477 |
An indexed intersection is a relation if at least one of the member of the
indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
|
|
|
Theorem | reluni 4478* |
The union of a class is a relation iff any member is a relation.
Exercise 6 of [TakeutiZaring] p.
25 and its converse. (Contributed by
NM, 13-Aug-2004.)
|
|
|
Theorem | relint 4479* |
The intersection of a class is a relation if at least one member is a
relation. (Contributed by NM, 8-Mar-2014.)
|
|
|
Theorem | rel0 4480 |
The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
|
|
|
Theorem | relopabi 4481 |
A class of ordered pairs is a relation. (Contributed by Mario Carneiro,
21-Dec-2013.)
|
|
|
Theorem | relopab 4482 |
A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.)
(Unnecessary distinct variable restrictions were removed by Alan Sare,
9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | reli 4483 |
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235. (Contributed by
NM, 26-Apr-1998.) (Revised by
Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | rele 4484 |
The membership relation is a relation. (Contributed by NM,
26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | opabid2 4485* |
A relation expressed as an ordered pair abstraction. (Contributed by
NM, 11-Dec-2006.)
|
|
|
Theorem | inopab 4486* |
Intersection of two ordered pair class abstractions. (Contributed by
NM, 30-Sep-2002.)
|
|
|
Theorem | difopab 4487* |
The difference of two ordered-pair abstractions. (Contributed by Stefan
O'Rear, 17-Jan-2015.)
|
|
|
Theorem | inxp 4488 |
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
|
|
Theorem | xpindi 4489 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52. (Contributed by NM,
26-Sep-2004.)
|
|
|
Theorem | xpindir 4490 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
(Contributed by NM, 26-Sep-2004.)
|
|
|
Theorem | xpiindim 4491* |
Distributive law for cross product over indexed intersection.
(Contributed by Jim Kingdon, 7-Dec-2018.)
|
|
|
Theorem | xpriindim 4492* |
Distributive law for cross product over relativized indexed
intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
|
|
|
Theorem | eliunxp 4493* |
Membership in a union of cross products. Analogue of elxp 4380
for
nonconstant . (Contributed by Mario Carneiro,
29-Dec-2014.)
|
|
|
Theorem | opeliunxp2 4494* |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 14-Feb-2015.)
|
|
|
Theorem | raliunxp 4495* |
Write a double restricted quantification as one universal quantifier.
In this version of ralxp 4497, is not assumed to be constant.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | rexiunxp 4496* |
Write a double restricted quantification as one universal quantifier.
In this version of rexxp 4498, is not assumed to be constant.
(Contributed by Mario Carneiro, 14-Feb-2015.)
|
|
|
Theorem | ralxp 4497* |
Universal quantification restricted to a cross product is equivalent to
a double restricted quantification. The hypothesis specifies an
implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | rexxp 4498* |
Existential quantification restricted to a cross product is equivalent
to a double restricted quantification. (Contributed by NM,
11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
|
|
|
Theorem | djussxp 4499* |
Disjoint union is a subset of a cross product. (Contributed by Stefan
O'Rear, 21-Nov-2014.)
|
|
|
Theorem | ralxpf 4500* |
Version of ralxp 4497 with bound-variable hypotheses. (Contributed
by NM,
18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|