Theorem List for Intuitionistic Logic Explorer - 4201-4300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | eqopab2b 4201 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | opabm 4202* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
|
|
Theorem | iunopab 4203* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|
|
|
2.3.6 Power class of union and
intersection
|
|
Theorem | pwin 4204 |
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 4205 |
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 4206 |
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 4207 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
|
|
Theorem | pwunim 4208 |
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.7 Epsilon and identity
relations
|
|
Syntax | cep 4209 |
Extend class notation to include the epsilon relation.
|
|
|
Syntax | cid 4210 |
Extend the definition of a class to include identity relation.
|
|
|
Definition | df-eprel 4211* |
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 4212. Thus, 5 { 1 , 5 }. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | epelg 4212 |
The epsilon relation and membership are the same. General version of
epel 4214. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
|
|
Theorem | epelc 4213 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
|
|
Theorem | epel 4214 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
|
|
Definition | df-id 4215* |
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.8 Partial and complete ordering
|
|
Syntax | wpo 4216 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'
|
|
|
Syntax | wor 4217 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' orders
.'
|
|
|
Definition | df-po 4218* |
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 4219* |
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 4220 |
Subset theorem for the partial ordering predicate. (Contributed by NM,
27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | poeq1 4221 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | poeq2 4222 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | nfpo 4223 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
|
|
Theorem | nfso 4224 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
|
|
Theorem | pocl 4225 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
|
|
Theorem | ispod 4226* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
|
|
Theorem | swopolem 4227* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | swopo 4228* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | poirr 4229 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | potr 4230 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | po2nr 4231 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | po3nr 4232 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | po0 4233 |
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 4234* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
|
|
Theorem | sopo 4235 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
|
|
Theorem | soss 4236 |
Subset theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | soeq1 4237 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
|
|
Theorem | soeq2 4238 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
|
|
Theorem | sonr 4239 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
|
|
Theorem | sotr 4240 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
|
|
Theorem | issod 4241* |
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of df-iso 4219). (Contributed by NM, 21-Jan-1996.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
|
|
Theorem | sowlin 4242 |
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6-Oct-2018.)
|
|
|
Theorem | so2nr 4243 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
|
|
Theorem | so3nr 4244 |
A strict order relation has no 3-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
|
|
Theorem | sotricim 4245 |
One direction of sotritric 4246 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28-Sep-2019.)
|
|
|
Theorem | sotritric 4246 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28-Sep-2019.)
|
|
|
Theorem | sotritrieq 4247 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13-Dec-2019.)
|
|
|
Theorem | so0 4248 |
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.9 Founded and set-like
relations
|
|
Syntax | wfrfor 4249 |
Extend wff notation to include the well-founded predicate.
|
FrFor |
|
Syntax | wfr 4250 |
Extend wff notation to include the well-founded predicate. Read: '
is a well-founded relation on .'
|
|
|
Syntax | wse 4251 |
Extend wff notation to include the set-like predicate. Read: ' is
set-like on .'
|
Se |
|
Syntax | wwe 4252 |
Extend wff notation to include the well-ordering predicate. Read:
' well-orders
.'
|
|
|
Definition | df-frfor 4253* |
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 4254* |
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 4255* |
Define the set-like predicate. (Contributed by Mario Carneiro,
19-Nov-2014.)
|
Se
|
|
Definition | df-wetr 4256* |
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 do not have that
as seen at ordtriexmid 4437). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the definition of is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23-Sep-2021.)
|
|
|
Theorem | seex 4257* |
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 4258 |
Any relation on a set is set-like on it. (Contributed by Mario
Carneiro, 22-Jun-2015.)
|
Se |
|
Theorem | sess1 4259 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se Se |
|
Theorem | sess2 4260 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se Se |
|
Theorem | seeq1 4261 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se
Se |
|
Theorem | seeq2 4262 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
Se
Se |
|
Theorem | nfse 4263 |
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 4264 |
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 4265 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
FrFor FrFor |
|
Theorem | freq1 4266 |
Equality theorem for the well-founded predicate. (Contributed by NM,
9-Mar-1997.)
|
|
|
Theorem | frforeq2 4267 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
FrFor FrFor |
|
Theorem | freq2 4268 |
Equality theorem for the well-founded predicate. (Contributed by NM,
3-Apr-1994.)
|
|
|
Theorem | frforeq3 4269 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
FrFor FrFor |
|
Theorem | nffrfor 4270 |
Bound-variable hypothesis builder for well-founded relations.
(Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario
Carneiro, 14-Oct-2016.)
|
FrFor
|
|
Theorem | nffr 4271 |
Bound-variable hypothesis builder for well-founded relations.
(Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario
Carneiro, 14-Oct-2016.)
|
|
|
Theorem | frirrg 4272 |
A well-founded relation is irreflexive. This is the case where
exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
|
|
|
Theorem | fr0 4273 |
Any relation is well-founded on the empty set. (Contributed by NM,
17-Sep-1993.)
|
|
|
Theorem | frind 4274* |
Induction over a well-founded set. (Contributed by Jim Kingdon,
28-Sep-2021.)
|
|
|
Theorem | efrirr 4275 |
Irreflexivity of the epsilon relation: a class founded by epsilon is not a
member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario
Carneiro, 22-Jun-2015.)
|
|
|
Theorem | tz7.2 4276 |
Similar to Theorem 7.2 of [TakeutiZaring]
p. 35, of except that the Axiom
of Regularity is not required due to antecedent .
(Contributed by NM, 4-May-1994.)
|
|
|
Theorem | nfwe 4277 |
Bound-variable hypothesis builder for well-orderings. (Contributed by
Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
|
|
Theorem | weeq1 4278 |
Equality theorem for the well-ordering predicate. (Contributed by NM,
9-Mar-1997.)
|
|
|
Theorem | weeq2 4279 |
Equality theorem for the well-ordering predicate. (Contributed by NM,
3-Apr-1994.)
|
|
|
Theorem | wefr 4280 |
A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|
|
|
Theorem | wepo 4281 |
A well-ordering is a partial ordering. (Contributed by Jim Kingdon,
23-Sep-2021.)
|
|
|
Theorem | wetrep 4282* |
An epsilon well-ordering is a transitive relation. (Contributed by NM,
22-Apr-1994.)
|
|
|
Theorem | we0 4283 |
Any relation is a well-ordering of the empty set. (Contributed by NM,
16-Mar-1997.)
|
|
|
2.3.10 Ordinals
|
|
Syntax | word 4284 |
Extend the definition of a wff to include the ordinal predicate.
|
|
|
Syntax | con0 4285 |
Extend the definition of a class to include the class of all ordinal
numbers. (The 0 in the name prevents creating a file called con.html,
which causes problems in Windows.)
|
|
|
Syntax | wlim 4286 |
Extend the definition of a wff to include the limit ordinal predicate.
|
|
|
Syntax | csuc 4287 |
Extend class notation to include the successor function.
|
|
|
Definition | df-iord 4288* |
Define the ordinal predicate, which is true for a class that is
transitive and whose elements are transitive. Definition of ordinal in
[Crosilla], p. "Set-theoretic
principles incompatible with
intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.)
Use
its alias dford3 4289 instead for naming consistency with set.mm.
(New usage is discouraged.)
|
|
|
Theorem | dford3 4289* |
Alias for df-iord 4288. Use it instead of df-iord 4288 for naming
consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
|
|
|
Definition | df-on 4290 |
Define the class of all ordinal numbers. Definition 7.11 of
[TakeutiZaring] p. 38. (Contributed
by NM, 5-Jun-1994.)
|
|
|
Definition | df-ilim 4291 |
Define the limit ordinal predicate, which is true for an ordinal that has
the empty set as an element and is not a successor (i.e. that is the union
of itself). Our definition combines the definition of Lim of
[BellMachover] p. 471 and Exercise 1
of [TakeutiZaring] p. 42, and then
changes to (which would be equivalent given the
law of the excluded middle, but which is not for us). (Contributed by Jim
Kingdon, 11-Nov-2018.) Use its alias dflim2 4292 instead for naming
consistency with set.mm. (New usage is discouraged.)
|
|
|
Theorem | dflim2 4292 |
Alias for df-ilim 4291. Use it instead of df-ilim 4291 for naming consistency
with set.mm. (Contributed by NM, 4-Nov-2004.)
|
|
|
Definition | df-suc 4293 |
Define the successor of a class. When applied to an ordinal number, the
successor means the same thing as "plus 1". Definition 7.22 of
[TakeutiZaring] p. 41, who use
"+ 1" to denote this function. Our
definition is a generalization to classes. Although it is not
conventional to use it with proper classes, it has no effect on a proper
class (sucprc 4334). Some authors denote the successor
operation with a
prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134
and the definition of successor in [Mendelson] p. 246 (who uses the symbol
"Suc" as a predicate to mean "is a successor
ordinal"). The definition of
successor of [Enderton] p. 68 denotes the
operation with a plus-sign
superscript. (Contributed by NM, 30-Aug-1993.)
|
|
|
Theorem | ordeq 4294 |
Equality theorem for the ordinal predicate. (Contributed by NM,
17-Sep-1993.)
|
|
|
Theorem | elong 4295 |
An ordinal number is an ordinal set. (Contributed by NM,
5-Jun-1994.)
|
|
|
Theorem | elon 4296 |
An ordinal number is an ordinal set. (Contributed by NM,
5-Jun-1994.)
|
|
|
Theorem | eloni 4297 |
An ordinal number has the ordinal property. (Contributed by NM,
5-Jun-1994.)
|
|
|
Theorem | elon2 4298 |
An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
|
|
|
Theorem | limeq 4299 |
Equality theorem for the limit predicate. (Contributed by NM,
22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ordtr 4300 |
An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
|
|