P. 68 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	o1p1e2 6701	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	oawordi 6702	Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( C +o A ) C_ ( C +o B ) ) )
Theorem	oawordriexmid 6703*	A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6702. (Contributed by Jim Kingdon, 15-May-2022.)
|- ( ( a e. On /\ b e. On /\ c e. On ) -> ( a C_ b -> ( a +o c ) C_ ( b +o c ) ) )   =>    |- ( ph \/ -. ph )
Theorem	oaword1 6704	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	omsuc 6705	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	onmsuc 6706	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
2.6.25  Natural number arithmetic
Theorem	nna0 6707	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 6708	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 6709	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	nnmsuc 6710	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	nna0r 6711	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( A e. om -> ( (/) +o A ) = A )
Theorem	nnm0r 6712	Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( A e. om -> ( (/) .o A ) = (/) )
Theorem	nnacl 6713	Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) e. om )
Theorem	nnmcl 6714	Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) e. om )
Theorem	nnacli 6715	om is closed under addition. Inference form of nnacl 6713. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 6716	om is closed under multiplication. Inference form of nnmcl 6714. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnacom 6717	Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) = ( B +o A ) )
Theorem	nnaass 6718	Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )
Theorem	nndi 6719	Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
Theorem	nnmass 6720	Multiplication of natural numbers is associative. Theorem 4K(4) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )
Theorem	nnmsucr 6721	Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( suc A .o B ) = ( ( A .o B ) +o B ) )
Theorem	nnmcom 6722	Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) = ( B .o A ) )
Theorem	nndir 6723	Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) .o C ) = ( ( A .o C ) +o ( B .o C ) ) )
Theorem	nnsucelsuc 6724	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4630, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4652. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( B e. om -> ( A e. B <-> suc A e. suc B ) )
Theorem	nnsucsssuc 6725	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4631, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4649. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )
Theorem	nntri3or 6726	Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	nntri2 6727	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
Theorem	nnsucuniel 6728	Given an element A of the union of a natural number B, suc A is an element of B itself. The reverse direction holds for all ordinals (sucunielr 4632). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4653). (Contributed by Jim Kingdon, 13-Mar-2022.)
|- ( B e. om -> ( A e. U. B <-> suc A e. B ) )
Theorem	nntri1 6729	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> -. B e. A ) )
Theorem	nntri3 6730	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
|- ( ( A e. om /\ B e. om ) -> ( A = B <-> ( -. A e. B /\ -. B e. A ) ) )
Theorem	nntri2or2 6731	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B \/ B C_ A ) )
Theorem	nndceq 6732	Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where B is zero, see nndceq0 4740. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A = B )
Theorem	nndcel 6733	Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A e. B )
Theorem	nnsseleq 6734	For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
Theorem	nnsssuc 6735	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.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> A e. suc B ) )
Theorem	nntr2 6736	Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.)
|- ( ( A e. om /\ C e. om ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )
Theorem	dcdifsnid 6737*	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 3840 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ B e. A ) -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	fnsnsplitdc 6738*	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.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ F Fn A /\ X e. A ) -> F = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
Theorem	funresdfunsndc 6739*	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.)
|- ( ( A. x e. dom F A. y e. dom FDECID x = y /\ Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )
Theorem	nndifsnid 6740	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 3840 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|- ( ( A e. om /\ B e. A ) -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	nnaordi 6741	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.)
|- ( ( B e. om /\ C e. om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaord 6742	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.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaordr 6743	Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )
Theorem	nnaword 6744	Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	nnacan 6745	Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	nnaword1 6746	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( A +o B ) )
Theorem	nnaword2 6747	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnawordi 6748	Adding to both sides of an inequality in om. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	nnmordi 6749	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.)
|- ( ( ( B e. om /\ C e. om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmord 6750	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.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmword 6751	Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmcan 6752	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	1onn 6753	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 6754	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 6755	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 6756	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	2ssom 6757	The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
|- 2o C_ om
Theorem	nnm1 6758	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 6759	Multiply an element of om by 2o. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 2o ) = ( A +o A ) )
Theorem	nn2m 6760	Multiply an element of om by 2o. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( 2o .o A ) = ( A +o A ) )
Theorem	nnaordex 6761*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> E. x e. om ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	nnawordex 6762*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> E. x e. om ( A +o x ) = B ) )
Theorem	nnm00 6763	The product of two natural numbers is zero iff at least one of them is zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|- ( ( A e. om /\ B e. om ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
2.6.26  Equivalence relations and classes
Syntax	wer 6764	Extend the definition of a wff to include the equivalence predicate.
wff R Er A
Syntax	cec 6765	Extend the definition of a class to include equivalence class.
class [ A ] R
Syntax	cqs 6766	Extend the definition of a class to include quotient set.
class ( A /. R )
Definition	df-er 6767	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 6768 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6787, ersymb 6781, and ertr 6782. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
Theorem	dfer2 6768*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A <-> ( Rel R /\ dom R = A /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
Definition	df-ec 6769	Define the R-coset of A. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of A modulo R when R is an equivalence relation (i.e. when Er R; see dfer2 6768). In this case, A is a representative (member) of the equivalence class [ A ] R, which contains all sets that are equivalent to A. Definition of [Enderton] p. 57 uses the notation [ A ] (subscript) R, although we simply follow the brackets by R since we don't have subscripted expressions. For an alternate definition, see dfec2 6770. (Contributed by NM, 23-Jul-1995.)
|- [ A ] R = ( R " { A } )
Theorem	dfec2 6770*	Alternate definition of R-coset of A. Definition 34 of [Suppes] p. 81. (Contributed by NM, 3-Jan-1997.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> [ A ] R = { y | A R y } )
Theorem	ecexg 6771	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
|- ( R e. B -> [ A ] R e. _V )
Theorem	ecexr 6772	An inhabited equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( A e. [ B ] R -> B e. _V )
Definition	df-qs 6773*	Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
Theorem	ereq1 6774	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R = S -> ( R Er A <-> S Er A ) )
Theorem	ereq2 6775	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( A = B -> ( R Er A <-> R Er B ) )
Theorem	errel 6776	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> Rel R )
Theorem	erdm 6777	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> dom R = A )
Theorem	ercl 6778	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> A e. X )
Theorem	ersym 6779	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> B R A )
Theorem	ercl2 6780	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> B e. X )
Theorem	ersymb 6781	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> ( A R B <-> B R A ) )
Theorem	ertr 6782	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> ( ( A R B /\ B R C ) -> A R C ) )
Theorem	ertrd 6783	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	ertr2d 6784	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> B R C )   =>    |- ( ph -> C R A )
Theorem	ertr3d 6785	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> B R A )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	ertr4d 6786	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> C R B )   =>    |- ( ph -> A R C )
Theorem	erref 6787	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.)
|- ( ph -> R Er X )   &    |- ( ph -> A e. X )   =>    |- ( ph -> A R A )
Theorem	ercnv 6788	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> `' R = R )
Theorem	errn 6789	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> ran R = A )
Theorem	erssxp 6790	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> R C_ ( A X. A ) )
Theorem	erex 6791	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.)
|- ( R Er A -> ( A e. V -> R e. _V ) )
Theorem	erexb 6792	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.)
|- ( R Er A -> ( R e. _V <-> A e. _V ) )
Theorem	iserd 6793*	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.)
|- ( ph -> Rel R )   &    |- ( ( ph /\ x R y ) -> y R x )   &    |- ( ( ph /\ ( x R y /\ y R z ) ) -> x R z )   &    |- ( ph -> ( x e. A <-> x R x ) )   =>    |- ( ph -> R Er A )
Theorem	brdifun 6794	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   =>    |- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
Theorem	swoer 6795*	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.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   =>    |- ( ph -> R Er X )
Theorem	swoord1 6796*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> A R B )   =>    |- ( ph -> ( A .< C <-> B .< C ) )
Theorem	swoord2 6797*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> A R B )   =>    |- ( ph -> ( C .< A <-> C .< B ) )
Theorem	eqerlem 6798*	Lemma for eqer 6799. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- ( z R w <-> [_ z / x ]_ A = [_ w / x ]_ A )
Theorem	eqer 6799*	Equivalence relation involving equality of dependent classes A ( x ) and B ( y ). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- R Er _V
Theorem	ider 6800	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.)
|- _I Er _V