Theorem List for Intuitionistic Logic Explorer - 6401-6500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nntri3 6401 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-May-2020.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nntri2or2 6402 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nndceq 6403 |
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where is zero, see nndceq0 4539.
(Contributed by Jim Kingdon, 31-Aug-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) DECID
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | nndcel 6404 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) DECID
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | nnsseleq 6405 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnsssuc 6406 |
A natural number is a subset of another natural number if and only if it
belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nntr2 6407 |
Transitive law for natural numbers. (Contributed by Jim Kingdon,
22-Jul-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dcdifsnid 6408* |
If we remove a single element from a set with decidable equality then
put it back in, we end up with the original set. This strengthens
difsnss 3674 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) DECID
![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![{
{](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | fnsnsplitdc 6409* |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) DECID ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![X X](_cx.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | funresdfunsndc 6410* |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon,
30-Jan-2023.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![F F](_cf.gif) ![A. A.](forall.gif) DECID
![F
F](_cf.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![X X](_cx.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![X X](_cx.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![X X](_cx.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | nndifsnid 6411 |
If we remove a single element from a natural number then put it back in,
we end up with the original natural number. This strengthens difsnss 3674
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | nnaordi 6412 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnaord 6413 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnaordr 6414 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnaword 6415 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnacan 6416 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnaword1 6417 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnaword2 6418 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnawordi 6419 |
Adding to both sides of an inequality in (Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnmordi 6420 |
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnmord 6421 |
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![(
(](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnmword 6422 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnmcan 6423 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 1onn 6424 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
![om om](omega.gif) |
|
Theorem | 2onn 6425 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
![om om](omega.gif) |
|
Theorem | 3onn 6426 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
![om om](omega.gif) |
|
Theorem | 4onn 6427 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
![om om](omega.gif) |
|
Theorem | nnm1 6428 |
Multiply an element of by .
(Contributed by Mario
Carneiro, 17-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![1o 1o](_1o.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | nnm2 6429 |
Multiply an element of by
(Contributed by Scott Fenton,
18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![2o 2o](_2o.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nn2m 6430 |
Multiply an element of by
(Contributed by Scott Fenton,
16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnaordex 6431* |
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![E.
E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif)
![x x](_x.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | nnawordex 6432* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![E.
E.](exists.gif) ![( (](lp.gif)
![x x](_x.gif)
![B B](_cb.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | nnm00 6433 |
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
2.6.24 Equivalence relations and
classes
|
|
Syntax | wer 6434 |
Extend the definition of a wff to include the equivalence predicate.
|
![A A](_ca.gif) |
|
Syntax | cec 6435 |
Extend the definition of a class to include equivalence class.
|
![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) |
|
Syntax | cqs 6436 |
Extend the definition of a class to include quotient set.
|
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Definition | df-er 6437 |
Define the equivalence relation predicate. Our notation is not standard.
A formal notation doesn't seem to exist in the literature; instead only
informal English tends to be used. The present definition, although
somewhat cryptic, nicely avoids dummy variables. In dfer2 6438 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6457, ersymb 6451, and ertr 6452.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif)
![( (](lp.gif) ![R R](_cr.gif) ![) )](rp.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | dfer2 6438* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![x x](_x.gif) ![A. A.](forall.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![z z](_z.gif) ![(
(](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif)
![y y](_y.gif) ![R R](_cr.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![R R](_cr.gif) ![z z](_z.gif) ![x x](_x.gif) ![R R](_cr.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Definition | df-ec 6439 |
Define the -coset of
. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of modulo when is an
equivalence relation (i.e. when ; see dfer2 6438). In this case,
is a
representative (member) of the equivalence class ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ,
which contains all sets that are equivalent to . Definition of
[Enderton] p. 57 uses the notation ![[ [](lbrack.gif) ![A A](_ca.gif) (subscript) , although
we simply follow the brackets by since we don't have subscripted
expressions. For an alternate definition, see dfec2 6440. (Contributed by
NM, 23-Jul-1995.)
|
![[
[](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![( (](lp.gif) ![R R](_cr.gif) ![" "](backquote.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | dfec2 6440* |
Alternate definition of -coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3-Jan-1997.) (Proof shortened by
Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
Theorem | ecexg 6441 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | ecexr 6442 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Definition | df-qs 6443* |
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![{ {](lbrace.gif) ![E. E.](exists.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![} }](rbrace.gif) |
|
Theorem | ereq1 6444 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ereq2 6445 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | errel 6446 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | erdm 6447 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ercl 6448 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) |
|
Theorem | ersym 6449 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ercl2 6450 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) |
|
Theorem | ersymb 6451 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ertr 6452 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ertrd 6453 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ertr2d 6454 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ertr3d 6455 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | ertr4d 6456 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | erref 6457 |
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6-May-2013.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ercnv 6458 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![`' `'](_cnv.gif)
![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | errn 6459 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | erssxp 6460 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | erex 6461 |
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | erexb 6462 |
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | iserd 6463* |
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised
by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![y y](_y.gif) ![R R](_cr.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![y y](_y.gif) ![R R](_cr.gif) ![z z](_z.gif) ![) )](rp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![z z](_z.gif) ![( (](lp.gif)
![( (](lp.gif) ![x x](_x.gif) ![R R](_cr.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | brdifun 6464 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | swoer 6465* |
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![X X](_cx.gif) ![) )](rp.gif)
![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) |
|
Theorem | swoord1 6466* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![X X](_cx.gif) ![) )](rp.gif)
![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | swoord2 6467* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![X X](_cx.gif) ![) )](rp.gif)
![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![( (](lp.gif) ![X X](_cx.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![y y](_y.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | eqerlem 6468* |
Lemma for eqer 6469. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
![( (](lp.gif) ![B B](_cb.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![( (](lp.gif) ![z z](_z.gif) ![R R](_cr.gif) ![[_ [_](_ulbrack.gif)
![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![[_ [_](_ulbrack.gif) ![x x](_x.gif) ![]_ ]_](_urbrack.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | eqer 6469* |
Equivalence relation involving equality of dependent classes ![A A](_ca.gif) ![(
(](lp.gif) ![x x](_x.gif)
and ![B B](_cb.gif) ![( (](lp.gif) ![y y](_y.gif) . (Contributed by NM, 17-Mar-2008.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![B B](_cb.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![B B](_cb.gif) ![_V _V](rmcv.gif) |
|
Theorem | ider 6470 |
The identity relation is an equivalence relation. (Contributed by NM,
10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof
shortened by Mario Carneiro, 9-Jul-2014.)
|
![_V _V](rmcv.gif) |
|
Theorem | 0er 6471 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
![(/) (/)](varnothing.gif) |
|
Theorem | eceq1 6472 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eceq1d 6473 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | eceq2 6474 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![C C](_cc.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![C C](_cc.gif) ![] ]](rbrack.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | elecg 6475 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![W W](_cw.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elec 6476 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | relelec 6477 |
Membership in an equivalence class when is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif)
![B B](_cb.gif) ![R R](_cr.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecss 6478 |
An equivalence class is a subset of the domain. (Contributed by NM,
6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif)
![X X](_cx.gif) ![) )](rp.gif) |
|
Theorem | ecdmn0m 6479* |
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
![( (](lp.gif) ![E. E.](exists.gif)
![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | ereldm 6480 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![( (](lp.gif)
![( (](lp.gif)
![X X](_cx.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | erth 6481 |
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | erth2 6482 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
(Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | erthi 6483 |
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro,
9-Jul-2014.)
|
![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R R](_cr.gif) ![B B](_cb.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | ecidsn 6484 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
![[
[](lbrack.gif) ![A A](_ca.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) |
|
Theorem | qseq1 6485 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![/. /.](diagup.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qseq2 6486 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![/. /.](diagup.gif) ![A A](_ca.gif)
![( (](lp.gif) ![C C](_cc.gif) ![/. /.](diagup.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elqsg 6487* |
Closed form of elqs 6488. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![E. E.](exists.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | elqs 6488* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![E. E.](exists.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | elqsi 6489* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![E. E.](exists.gif)
![[ [](lbrack.gif) ![x x](_x.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | ecelqsg 6490 |
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif)
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecelqsi 6491 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![[ [](lbrack.gif) ![B B](_cb.gif) ![] ]](rbrack.gif)
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ecopqsi 6492 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![S S](_cs.gif) ![) )](rp.gif) |
|
Theorem | qsexg 6493 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
|
Theorem | qsex 6494 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![_V _V](rmcv.gif) |
|
Theorem | uniqs 6495 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
![( (](lp.gif) ![U. U.](bigcup.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![( (](lp.gif) ![R R](_cr.gif) ![" "](backquote.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qsss 6496 |
A quotient set is a set of subsets of the base set. (Contributed by
Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![~P ~P](scrp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | uniqs2 6497 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![V V](_cv.gif) ![( (](lp.gif) ![U. U.](bigcup.gif) ![( (](lp.gif) ![A A](_ca.gif) ![/. /.](diagup.gif) ![R R](_cr.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | snec 6498 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
![{ {](lbrace.gif) ![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![R R](_cr.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | ecqs 6499 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif)
![U. U.](bigcup.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![/. /.](diagup.gif) ![R R](_cr.gif) ![) )](rp.gif) |
|
Theorem | ecid 6500 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
![[ [](lbrack.gif) ![A A](_ca.gif) ![] ]](rbrack.gif) ![A A](_ca.gif) |