Theorem List for Intuitionistic Logic Explorer - 4501-4600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nndceq0 4501 |
A natural number is either zero or nonzero. Decidable equality for
natural numbers is a special case of the law of the excluded middle
which holds in most constructive set theories including ours.
(Contributed by Jim Kingdon, 5-Jan-2019.)
|
DECID |
|
Theorem | 0elnn 4502 |
A natural number is either the empty set or has the empty set as an
element. (Contributed by Jim Kingdon, 23-Aug-2019.)
|
|
|
Theorem | nn0eln0 4503 |
A natural number is nonempty iff it contains the empty set. Although in
constructive mathematics it is generally more natural to work with
inhabited sets and ignore the whole concept of nonempty sets, in the
specific case of natural numbers this theorem may be helpful in converting
proofs which were written assuming excluded middle. (Contributed by Jim
Kingdon, 28-Aug-2019.)
|
|
|
Theorem | nnregexmid 4504* |
If inhabited sets of natural numbers always have minimal elements,
excluded middle follows. The argument is essentially the same as
regexmid 4420 and the larger lesson is that although
natural numbers may
behave "non-constructively" even in a constructive set theory
(for
example see nndceq 6363 or nntri3or 6357), sets of natural numbers are a
different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)
|
|
|
Theorem | omsinds 4505* |
Strong (or "total") induction principle over . (Contributed by
Scott Fenton, 17-Jul-2015.)
|
|
|
Theorem | nnpredcl 4506 |
The predecessor of a natural number is a natural number. This theorem
is most interesting when the natural number is a successor (as seen in
theorems like onsucuni2 4449) but also holds when it is by
uni0 3733. (Contributed by Jim Kingdon, 31-Jul-2022.)
|
|
|
2.6.6 Relations
|
|
Syntax | cxp 4507 |
Extend the definition of a class to include the cross product.
|
|
|
Syntax | ccnv 4508 |
Extend the definition of a class to include the converse of a class.
|
|
|
Syntax | cdm 4509 |
Extend the definition of a class to include the domain of a class.
|
|
|
Syntax | crn 4510 |
Extend the definition of a class to include the range of a class.
|
|
|
Syntax | cres 4511 |
Extend the definition of a class to include the restriction of a class.
(Read: The restriction of to .)
|
|
|
Syntax | cima 4512 |
Extend the definition of a class to include the image of a class. (Read:
The image of
under .)
|
|
|
Syntax | ccom 4513 |
Extend the definition of a class to include the composition of two
classes. (Read: The composition of and .)
|
|
|
Syntax | wrel 4514 |
Extend the definition of a wff to include the relation predicate. (Read:
is a relation.)
|
|
|
Definition | df-xp 4515* |
Define the cross product of two classes. Definition 9.11 of [Quine]
p. 64. For example, ( { 1 , 5 } { 2 , 7 } ) = ( { 1 , 2
,
1 , 7 } { 5 , 2 , 5 ,
7 }
) . Another example is that the set of rational numbers are
defined in using the cross-product ( Z N ) ; the left- and
right-hand sides of the cross-product represent the top (integer) and
bottom (natural) numbers of a fraction. (Contributed by NM,
4-Jul-1994.)
|
|
|
Definition | df-rel 4516 |
Define the relation predicate. Definition 6.4(1) of [TakeutiZaring]
p. 23. For alternate definitions, see dfrel2 4959 and dfrel3 4966.
(Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-cnv 4517* |
Define the converse of a class. Definition 9.12 of [Quine] p. 64. The
converse of a binary relation swaps its arguments, i.e., if
and then , as proven in brcnv 4692
(see df-br 3900 and df-rel 4516 for more on relations). For example,
{ 2
, 6 , 3 , 9 } = { 6 , 2 ,
9 ,
3 } . We
use Quine's breve accent (smile) notation.
Like Quine, we use it as a prefix, which eliminates the need for
parentheses. Many authors use the postfix superscript "to the
minus
one." "Converse" is Quine's terminology; some authors
call it
"inverse," especially when the argument is a function.
(Contributed by
NM, 4-Jul-1994.)
|
|
|
Definition | df-co 4518* |
Define the composition of two classes. Definition 6.6(3) of
[TakeutiZaring] p. 24. Note that
Definition 7 of [Suppes] p. 63
reverses and
, uses a slash instead
of , and calls
the operation "relative product." (Contributed by NM,
4-Jul-1994.)
|
|
|
Definition | df-dm 4519* |
Define the domain of a class. Definition 3 of [Suppes] p. 59. For
example, F = { 2 , 6 , 3 , 9 } dom F
= { 2 , 3 } . Contrast with range (defined in df-rn 4520). For alternate
definitions see dfdm2 5043, dfdm3 4696, and dfdm4 4701. The
notation " " is used by Enderton; other authors sometimes use
script D. (Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-rn 4520 |
Define the range of a class. For example, F = { 2 , 6 ,
3 ,
9 } ->
ran F = { 6 , 9 } . Contrast with domain
(defined in df-dm 4519). For alternate definitions, see dfrn2 4697,
dfrn3 4698, and dfrn4 4969. The notation " " is used by Enderton;
other authors sometimes use script R or script W. (Contributed by NM,
1-Aug-1994.)
|
|
|
Definition | df-res 4521 |
Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring]
p. 24. For example ( F = { 2 , 6 , 3 , 9 }
B = { 1 ,
2 } ) -> ( F B ) = { 2 , 6 } .
(Contributed by NM, 2-Aug-1994.)
|
|
|
Definition | df-ima 4522 |
Define the image of a class (as restricted by another class).
Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = {
2 , 6 , 3 , 9 } /\ B = { 1 , 2 } ) -> ( F B )
= { 6 } . Contrast with restriction (df-res 4521) and range (df-rn 4520).
For an alternate definition, see dfima2 4853. (Contributed by NM,
2-Aug-1994.)
|
|
|
Theorem | xpeq1 4523 |
Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
|
|
|
Theorem | xpeq2 4524 |
Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
|
|
|
Theorem | elxpi 4525* |
Membership in a cross product. Uses fewer axioms than elxp 4526.
(Contributed by NM, 4-Jul-1994.)
|
|
|
Theorem | elxp 4526* |
Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
|
|
|
Theorem | elxp2 4527* |
Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
|
|
|
Theorem | xpeq12 4528 |
Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
|
|
|
Theorem | xpeq1i 4529 |
Equality inference for cross product. (Contributed by NM,
21-Dec-2008.)
|
|
|
Theorem | xpeq2i 4530 |
Equality inference for cross product. (Contributed by NM,
21-Dec-2008.)
|
|
|
Theorem | xpeq12i 4531 |
Equality inference for cross product. (Contributed by FL,
31-Aug-2009.)
|
|
|
Theorem | xpeq1d 4532 |
Equality deduction for cross product. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
|
|
Theorem | xpeq2d 4533 |
Equality deduction for cross product. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
|
|
Theorem | xpeq12d 4534 |
Equality deduction for Cartesian product. (Contributed by NM,
8-Dec-2013.)
|
|
|
Theorem | sqxpeqd 4535 |
Equality deduction for a Cartesian square, see Wikipedia "Cartesian
product",
https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power.
(Contributed by AV, 13-Jan-2020.)
|
|
|
Theorem | nfxp 4536 |
Bound-variable hypothesis builder for cross product. (Contributed by
NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | 0nelxp 4537 |
The empty set is not a member of a cross product. (Contributed by NM,
2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | 0nelelxp 4538 |
A member of a cross product (ordered pair) doesn't contain the empty
set. (Contributed by NM, 15-Dec-2008.)
|
|
|
Theorem | opelxp 4539 |
Ordered pair membership in a cross product. (Contributed by NM,
15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brxp 4540 |
Binary relation on a cross product. (Contributed by NM,
22-Apr-2004.)
|
|
|
Theorem | opelxpi 4541 |
Ordered pair membership in a cross product (implication). (Contributed by
NM, 28-May-1995.)
|
|
|
Theorem | opelxpd 4542 |
Ordered pair membership in a Cartesian product, deduction form.
(Contributed by Glauco Siliprandi, 3-Mar-2021.)
|
|
|
Theorem | opelxp1 4543 |
The first member of an ordered pair of classes in a cross product belongs
to first cross product argument. (Contributed by NM, 28-May-2008.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opelxp2 4544 |
The second member of an ordered pair of classes in a cross product belongs
to second cross product argument. (Contributed by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | otelxp1 4545 |
The first member of an ordered triple of classes in a cross product
belongs to first cross product argument. (Contributed by NM,
28-May-2008.)
|
|
|
Theorem | rabxp 4546* |
Membership in a class builder restricted to a cross product.
(Contributed by NM, 20-Feb-2014.)
|
|
|
Theorem | brrelex12 4547 |
A true binary relation on a relation implies the arguments are sets.
(This is a property of our ordered pair definition.) (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brrelex1 4548 |
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.) (Contributed by NM,
18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brrelex 4549 |
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.) (Contributed by NM,
18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brrelex2 4550 |
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 | brrelex12i 4551 |
Two classes that are related by a binary relation are sets. (An
artifact of our ordered pair definition.) (Contributed by BJ,
3-Oct-2022.)
|
|
|
Theorem | brrelex1i 4552 |
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
|
|
|
Theorem | brrelex2i 4553 |
The second argument of a binary relation exists. (An artifact of our
ordered pair definition.) (Contributed by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | nprrel 4554 |
No proper class is related to anything via any relation. (Contributed
by Roy F. Longton, 30-Jul-2005.)
|
|
|
Theorem | 0nelrel 4555 |
A binary relation does not contain the empty set. (Contributed by AV,
15-Nov-2021.)
|
|
|
Theorem | fconstmpt 4556* |
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 4557* |
Variable to class conversion of transitive relation. (Contributed by
NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opelvvg 4558 |
Ordered pair membership in the universal class of ordered pairs.
(Contributed by Mario Carneiro, 3-May-2015.)
|
|
|
Theorem | opelvv 4559 |
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 4560 |
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 4561 |
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 4562* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 9-Nov-2015.)
|
|
|
Theorem | elxp3 4563* |
Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
|
|
|
Theorem | opeliunxp 4564 |
Membership in a union of cross products. (Contributed by Mario
Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
|
|
|
Theorem | xpundi 4565 |
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52. (Contributed by NM, 12-Aug-2004.)
|
|
|
Theorem | xpundir 4566 |
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52. (Contributed by NM,
30-Sep-2002.)
|
|
|
Theorem | xpiundi 4567* |
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27-Apr-2014.)
|
|
|
Theorem | xpiundir 4568* |
Distributive law for cross product over indexed union. (Contributed by
Mario Carneiro, 27-Apr-2014.)
|
|
|
Theorem | iunxpconst 4569* |
Membership in a union of cross products when the second factor is
constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | xpun 4570 |
The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
|
|
|
Theorem | elvv 4571* |
Membership in universal class of ordered pairs. (Contributed by NM,
4-Jul-1994.)
|
|
|
Theorem | elvvv 4572* |
Membership in universal class of ordered triples. (Contributed by NM,
17-Dec-2008.)
|
|
|
Theorem | elvvuni 4573 |
An ordered pair contains its union. (Contributed by NM,
16-Sep-2006.)
|
|
|
Theorem | mosubopt 4574* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-Aug-2007.)
|
|
|
Theorem | mosubop 4575* |
"At most one" remains true inside ordered pair quantification.
(Contributed by NM, 28-May-1995.)
|
|
|
Theorem | brinxp2 4576 |
Intersection of binary relation with cross product. (Contributed by NM,
3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | brinxp 4577 |
Intersection of binary relation with cross product. (Contributed by NM,
9-Mar-1997.)
|
|
|
Theorem | poinxp 4578 |
Intersection of partial order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
|
|
Theorem | soinxp 4579 |
Intersection of linear order with cross product of its field.
(Contributed by Mario Carneiro, 10-Jul-2014.)
|
|
|
Theorem | seinxp 4580 |
Intersection of set-like relation with cross product of its field.
(Contributed by Mario Carneiro, 22-Jun-2015.)
|
Se
Se |
|
Theorem | posng 4581 |
Partial ordering of a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
|
|
Theorem | sosng 4582 |
Strict linear ordering on a singleton. (Contributed by Jim Kingdon,
5-Dec-2018.)
|
|
|
Theorem | opabssxp 4583* |
An abstraction relation is a subset of a related cross product.
(Contributed by NM, 16-Jul-1995.)
|
|
|
Theorem | brab2ga 4584* |
The law of concretion for a binary relation. See brab2a 4562 for alternate
proof. TODO: should one of them be deleted? (Contributed by Mario
Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
|
|
|
Theorem | optocl 4585* |
Implicit substitution of class for ordered pair. (Contributed by NM,
5-Mar-1995.)
|
|
|
Theorem | 2optocl 4586* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
|
|
Theorem | 3optocl 4587* |
Implicit substitution of classes for ordered pairs. (Contributed by NM,
12-Mar-1995.)
|
|
|
Theorem | opbrop 4588* |
Ordered pair membership in a relation. Special case. (Contributed by
NM, 5-Aug-1995.)
|
|
|
Theorem | 0xp 4589 |
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 4590 |
Distribute proper substitution through the cross product of two classes.
(Contributed by Alan Sare, 10-Nov-2012.)
|
|
|
Theorem | releq 4591 |
Equality theorem for the relation predicate. (Contributed by NM,
1-Aug-1994.)
|
|
|
Theorem | releqi 4592 |
Equality inference for the relation predicate. (Contributed by NM,
8-Dec-2006.)
|
|
|
Theorem | releqd 4593 |
Equality deduction for the relation predicate. (Contributed by NM,
8-Mar-2014.)
|
|
|
Theorem | nfrel 4594 |
Bound-variable hypothesis builder for a relation. (Contributed by NM,
31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | sbcrel 4595 |
Distribute proper substitution through a relation predicate. (Contributed
by Alexander van der Vekens, 23-Jul-2017.)
|
|
|
Theorem | relss 4596 |
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
(Contributed by NM, 15-Aug-1994.)
|
|
|
Theorem | ssrel 4597* |
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 4598* |
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33. (Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | ssrel2 4599* |
A subclass relationship depends only on a relation's ordered pairs.
This version of ssrel 4597 is restricted to the relation's domain.
(Contributed by Thierry Arnoux, 25-Jan-2018.)
|
|
|
Theorem | relssi 4600* |
Inference from subclass principle for relations. (Contributed by NM,
31-Mar-1998.)
|
|