Theorem List for Intuitionistic Logic Explorer - 4001-4100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | copsex2g 4001* |
Implicit substitution inference for ordered pairs. (Contributed by NM,
28-May-1995.)
|
|
|
Theorem | copsex4g 4002* |
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5-Aug-1995.)
|
|
|
Theorem | 0nelop 4003 |
A property of ordered pairs. (Contributed by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | opeqex 4004 |
Equivalence of existence implied by equality of ordered pairs.
(Contributed by NM, 28-May-2008.)
|
|
|
Theorem | opcom 4005 |
An ordered pair commutes iff its members are equal. (Contributed by NM,
28-May-2009.)
|
|
|
Theorem | moop2 4006* |
"At most one" property of an ordered pair. (Contributed by NM,
11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opeqsn 4007 |
Equivalence for an ordered pair equal to a singleton. (Contributed by
NM, 3-Jun-2008.)
|
|
|
Theorem | opeqpr 4008 |
Equivalence for an ordered pair equal to an unordered pair.
(Contributed by NM, 3-Jun-2008.)
|
|
|
Theorem | euotd 4009* |
Prove existential uniqueness for an ordered triple. (Contributed by
Mario Carneiro, 20-May-2015.)
|
|
|
Theorem | uniop 4010 |
The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
(Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | uniopel 4011 |
Ordered pair membership is inherited by class union. (Contributed by
NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
2.3.4 Ordered-pair class abstractions
(cont.)
|
|
Theorem | opabid 4012 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon,
25-Jul-2011.)
|
|
|
Theorem | elopab 4013* |
Membership in a class abstraction of pairs. (Contributed by NM,
24-Mar-1998.)
|
|
|
Theorem | opelopabsbALT 4014* |
The law of concretion in terms of substitutions. Less general than
opelopabsb 4015, but having a much shorter proof.
(Contributed by NM,
30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
|
Theorem | opelopabsb 4015* |
The law of concretion in terms of substitutions. (Contributed by NM,
30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | brabsb 4016* |
The law of concretion in terms of substitutions. (Contributed by NM,
17-Mar-2008.)
|
|
|
Theorem | opelopabt 4017* |
Closed theorem form of opelopab 4026. (Contributed by NM,
19-Feb-2013.)
|
|
|
Theorem | opelopabga 4018* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | brabga 4019* |
The law of concretion for a binary relation. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
|
|
Theorem | opelopab2a 4020* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | opelopaba 4021* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | braba 4022* |
The law of concretion for a binary relation. (Contributed by NM,
19-Dec-2013.)
|
|
|
Theorem | opelopabg 4023* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | brabg 4024* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | opelopab2 4025* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
|
|
Theorem | opelopab 4026* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 16-May-1995.)
|
|
|
Theorem | brab 4027* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.)
|
|
|
Theorem | opelopabaf 4028* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4026 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof
shortened by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | opelopabf 4029* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4026 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19-Dec-2008.)
|
|
|
Theorem | ssopab2 4030 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro,
19-May-2013.)
|
|
|
Theorem | ssopab2b 4031 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro,
18-Nov-2016.)
|
|
|
Theorem | ssopab2i 4032 |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5-Apr-1995.)
|
|
|
Theorem | ssopab2dv 4033* |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
|
|
Theorem | eqopab2b 4034 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | opabm 4035* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
|
|
Theorem | iunopab 4036* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|
|
|
2.3.5 Power class of union and
intersection
|
|
Theorem | pwin 4037 |
The power class of the intersection of two classes is the intersection
of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
(Contributed by NM, 23-Nov-2003.)
|
|
|
Theorem | pwunss 4038 |
The power class of the union of two classes includes the union of their
power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by
NM, 23-Nov-2003.)
|
|
|
Theorem | pwssunim 4039 |
The power class of the union of two classes is a subset of the union of
their power classes, if one class is a subclass of the other. One
direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by
Jim Kingdon, 30-Sep-2018.)
|
|
|
Theorem | pwundifss 4040 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
|
|
Theorem | pwunim 4041 |
The power class of the union of two classes equals the union of their
power classes, iff one class is a subclass of the other. Part of Exercise
7(b) of [Enderton] p. 28. (Contributed
by Jim Kingdon, 30-Sep-2018.)
|
|
|
2.3.6 Epsilon and identity
relations
|
|
Syntax | cep 4042 |
Extend class notation to include the epsilon relation.
|
|
|
Syntax | cid 4043 |
Extend the definition of a class to include identity relation.
|
|
|
Definition | df-eprel 4044* |
Define the epsilon relation. Similar to Definition 6.22 of
[TakeutiZaring] p. 30. The
epsilon relation and set membership are the
same, that is, when is a set by
epelg 4045. Thus, 5 { 1 , 5 }. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | epelg 4045 |
The epsilon relation and membership are the same. General version of
epel 4047. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
|
|
Theorem | epelc 4046 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
|
|
Theorem | epel 4047 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
|
|
Definition | df-id 4048* |
Define the identity relation. Definition 9.15 of [Quine] p. 64. For
example, 5 5
and 4 5. (Contributed by NM,
13-Aug-1995.)
|
|
|
2.3.7 Partial and complete ordering
|
|
Syntax | wpo 4049 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'
|
|
|
Syntax | wor 4050 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' orders
.'
|
|
|
Definition | df-po 4051* |
Define the strict partial order predicate. Definition of [Enderton]
p. 168. The expression means is a partial order on
. (Contributed
by NM, 16-Mar-1997.)
|
|
|
Definition | df-iso 4052* |
Define the strict linear order predicate. The expression
is
true if relationship orders .
The property
is called
weak linearity by Proposition
11.2.3 of [HoTT], p. (varies). If we
assumed excluded middle, it would
be equivalent to trichotomy, . (Contributed
by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|
|
|
Theorem | poss 4053 |
Subset theorem for the partial ordering predicate. (Contributed by NM,
27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | poeq1 4054 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | poeq2 4055 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | nfpo 4056 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
|
|
Theorem | nfso 4057 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
|
|
Theorem | pocl 4058 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
|
|
Theorem | ispod 4059* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
|
|
Theorem | swopolem 4060* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | swopo 4061* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | poirr 4062 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | potr 4063 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | po2nr 4064 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | po3nr 4065 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | po0 4066 |
Any relation is a partial ordering of the empty set. (Contributed by
NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | pofun 4067* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
|
|
Theorem | sopo 4068 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
|
|
Theorem | soss 4069 |
Subset theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | soeq1 4070 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
|
|
Theorem | soeq2 4071 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
|
|
Theorem | sonr 4072 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
|
|
Theorem | sotr 4073 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
|
|
Theorem | issod 4074* |
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of df-iso 4052). (Contributed by NM, 21-Jan-1996.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | sowlin 4075 |
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6-Oct-2018.)
|
|
|
Theorem | so2nr 4076 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
|
|
Theorem | so3nr 4077 |
A strict order relation has no 3-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
|
|
Theorem | sotricim 4078 |
One direction of sotritric 4079 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28-Sep-2019.)
|
|
|
Theorem | sotritric 4079 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28-Sep-2019.)
|
|
|
Theorem | sotritrieq 4080 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13-Dec-2019.)
|
|
|
Theorem | so0 4081 |
Any relation is a strict ordering of the empty set. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
2.3.8 Founded and set-like
relations
|
|
Syntax | wfrfor 4082 |
Extend wff notation to include the well-founded predicate.
|
FrFor |
|
Syntax | wfr 4083 |
Extend wff notation to include the well-founded predicate. Read: '
is a well-founded relation on .'
|
|
|
Syntax | wse 4084 |
Extend wff notation to include the set-like predicate. Read: ' is
set-like on .'
|
Se |
|
Syntax | wwe 4085 |
Extend wff notation to include the well-ordering predicate. Read:
' well-orders
.'
|
|
|
Definition | df-frfor 4086* |
Define the well-founded relation predicate where might be a proper
class. By passing in we allow it potentially to be a proper class
rather than a set. (Contributed by Jim Kingdon and Mario Carneiro,
22-Sep-2021.)
|
FrFor
|
|
Definition | df-frind 4087* |
Define the well-founded relation predicate. In the presence of excluded
middle, there are a variety of equivalent ways to define this. In our
case, this definition, in terms of an inductive principle, works better
than one along the lines of "there is an element which is minimal
when A
is ordered by R". Because is constrained to be a set (not a
proper class) here, sometimes it may be necessary to use FrFor
directly rather than via . (Contributed by Jim Kingdon and Mario
Carneiro, 21-Sep-2021.)
|
FrFor |
|
Definition | df-se 4088* |
Define the set-like predicate. (Contributed by Mario Carneiro,
19-Nov-2014.)
|
Se
|
|
Definition | df-wetr 4089* |
Define the well-ordering predicate. It is unusual to define
"well-ordering" in the absence of excluded middle, but we mean
an
ordering which is like the ordering which we have for ordinals (for
example, it does not entail trichotomy because ordinals don't have that
as seen at ordtriexmid 4265). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the defintion of is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23-Sep-2021.)
|
|
|
Theorem | seex 4090* |
The -preimage of an
element of the base set in a set-like relation
is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
|
Se |
|
Theorem | exse 4091 |
Any relation on a set is set-like on it. (Contributed by Mario
Carneiro, 22-Jun-2015.)
|
Se |
|
Theorem | sess1 4092 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se Se |
|
Theorem | sess2 4093 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se Se |
|
Theorem | seeq1 4094 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se
Se |
|
Theorem | seeq2 4095 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se
Se |
|
Theorem | nfse 4096 |
Bound-variable hypothesis builder for set-like relations. (Contributed
by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
Se |
|
Theorem | epse 4097 |
The epsilon relation is set-like on any class. (This is the origin of
the term "set-like": a set-like relation "acts like"
the epsilon
relation of sets and their elements.) (Contributed by Mario Carneiro,
22-Jun-2015.)
|
Se |
|
Theorem | frforeq1 4098 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
FrFor FrFor |
|
Theorem | freq1 4099 |
Equality theorem for the well-founded predicate. (Contributed by NM,
9-Mar-1997.)
|
|
|
Theorem | frforeq2 4100 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
FrFor FrFor |