Metamath Proof Explorer - mmtheorems33

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 3201-3300 - Page 33 of 58

Type	Label	Description
Statement
Theorem	er2 3201	Alternate definition of equivalence predicate.
|- (Er R <-> A.xA.yA.z((xRy -> yRx) /\ ((xRy /\ yRz) -> xRz)))
Definition	df-ec 3202	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. The Definition of [Enderton] p. 57 uses the notation [A] (subscript) R, although we simply follow the brackets by R since we don't have subscripts. For an alternate definition, see ec2 3203.
|- [A]R = (R"{A})
Theorem	ec2 3203	Alternate definition of R-coset of A. Definition 34 of [Suppes] p. 81.
|- A e. V   =>   |- [A]R = {y | ARy}
Theorem	ecexg 3204	An equivalence class modulo a set is a set.
|- (R e. B -> [A]R e. V)
Definition	df-qs 3205	Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58.
|- (A/.R) = {y | E.x e. A y = [x]R}
Theorem	ereq 3206	Equality theorem for equivalence predicate.
|- (R = S -> (Er R <-> Er S))
Theorem	ster 3207	A symmetric, transitive relation is an equivalence relation.
|- (xRy -> yRx)   &   |- ((xRy /\ yRz) -> xRz)   =>   |- Er R
Theorem	ider 3208	The identity relation is an equivalence relation.
|- Er I
Theorem	ersym 3209	An equivalence relation is symmetric.
|- A e. V   &   |- B e. V   &   |- Er R   =>   |- (ARB -> BRA)
Theorem	ersymb 3210	An equivalence relation is symmetric.
|- A e. V   &   |- B e. V   &   |- Er R   =>   |- (ARB <-> BRA)
Theorem	ertr 3211	An equivalence relation is transitive.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- Er R   =>   |- ((ARB /\ BRC) -> ARC)
Theorem	erref 3212	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56.
|- Er R   =>   |- (A e. (dom R u. ran R) -> ARA)
Theorem	erdmrn 3213	The range and domain of an equivalence relation are equal.
|- Er R   =>   |- dom R = ran R
Theorem	eceq1 3214	Equality theorem for equivalence class.
|- (A = B -> [C]A = [C]B)
Theorem	eceq2 3215	Equality theorem for equivalence class.
|- (A = B -> [A]C = [B]C)
Theorem	elec 3216	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
|- A e. V   &   |- B e. V   =>   |- (A e. [B]R <-> BRA)
Theorem	ecdmn0 3217	An equivalence class is not empty in its domain.
|- A e. V   =>   |- (A e. dom R <-> -. [A]R = (/))
Theorem	erthi 3218	Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57.
|- A e. V   &   |- B e. V   &   |- Er R   =>   |- (ARB -> [A]R = [B]R)
Theorem	erth 3219	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
|- B e. V   &   |- Er R   =>   |- (A e. (dom R u. ran R) -> ([A]R = [B]R <-> ARB))
Theorem	erthdm 3220	Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership in the domain instead of just the field.
|- B e. V   &   |- Er R   =>   |- (A e. dom R -> ([A]R = [B]R <-> ARB))
Theorem	erthdmr 3221	Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain.
|- A e. V   &   |- B e. V   &   |- Er R   =>   |- (B e. dom R -> ([A]R = [B]R <-> ARB))
Theorem	ereldm 3222	Equality of equivalence classes implies equivalence of domain membership.
|- A e. V   &   |- B e. V   &   |- Er R   &   |- dom R = D   =>   |- ([A]R = [B]R -> (A e. D <-> B e. D))
Theorem	erdisj 3223	Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83.
|- A e. V   &   |- B e. V   &   |- Er R   =>   |- ([A]R = [B]R \/ ([A]R i^i [B]R) = (/))
Theorem	ecidsn 3224	An equivalence class modulo the identity relation is a singleton.
|- [A]I = {A}
Theorem	qseq1 3225	Equality theorem for quotient set.
|- (A = B -> (A/.C) = (B/.C))
Theorem	qseq2 3226	Equality theorem for quotient set.
|- (A = B -> (C/.A) = (C/.B))
Theorem	elqs 3227	Membership in a quotient set.
|- B e. V   =>   |- (B e. (A/.R) <-> E.x(x e. A /\ B = [x]R))
Theorem	elqsi 3228	Membership in a quotient set.
|- (B e. (A/.R) -> E.x(x e. A /\ B = [x]R))
Theorem	ecelqsi 3229	Membership of an equivalence class in a quotient set.
|- R e. V   =>   |- (B e. A -> [B]R e. (A/.R))
Theorem	ecopqsi 3230	"Closure" law for equivalence class of ordered pairs.
|- R e. V   &   |- S = ((A X. A)/.R)   =>   |- ((B e. A /\ C e. A) -> [<.B, C>.]R e. S)
Theorem	qsex 3231	A quotient set exists.
|- A e. V   =>   |- (A/.R) e. V
Theorem	snec 3232	The singleton of an equivalence class.
|- A e. V   =>   |- {[A]R} = ({A}/.R)
Theorem	ecqs 3233	Equivalence class in terms of quotient set.
|- A e. V   &   |- R e. V   =>   |- [A]R = U.({A}/.R)
Theorem	0nelqs 3234	A quotient set doesn't contain the empty set.
|- Er R   &   |- dom R = A   =>   |- -. (/) e. (A/.R)
Theorem	ecelqsdm 3235	Membership of an equivalence class in a quotient set.
|- B e. V   &   |- Er R   &   |- dom R = A   =>   |- ([B]R e. (A/.R) -> B e. A)
Theorem	ecid 3236	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.)
|- A e. V   =>   |- [A]`'E = A
Theorem	qsid 3237	A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.)
|- A e. V   =>   |- (A/.`'E) = A
Theorem	ectocl 3238	Implicit substitution of class for equivalence class.
|- S = (B/.R)   &   |- ([x]R = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. S -> ps)
Theorem	ecoptocl 3239	Implicit substitution of class for equivalence class of ordered pair.
|- S = ((B X. C)/.R)   &   |- ([<.x, y>.]R = A -> (ph <-> ps))   &   |- ((x e. B /\ y e. C) -> ph)   =>   |- (A e. S -> ps)
Theorem	2ecoptocl 3240	Implicit substitution of classes for equivalence classes of ordered pairs.
|- S = ((C X. D)/.R)   &   |- ([<.x, y>.]R = A -> (ph <-> ps))   &   |- ([<.z, w>.]R = B -> (ps <-> ch))   &   |- (((x e. C /\ y e. D) /\ (z e. C /\ w e. D)) -> ph)   =>   |- ((A e. S /\ B e. S) -> ch)
Theorem	3ecoptocl 3241	Implicit substitution of classes for equivalence classes of ordered pairs.
|- S = ((D X. D)/.R)   &   |- ([<.x, y>.]R = A -> (ph <-> ps))   &   |- ([<.z, w>.]R = B -> (ps <-> ch))   &   |- ([<.v, u>.]R = C -> (ch <-> th))   &   |- (((x e. D /\ y e. D) /\ (z e. D /\ w e. D) /\ (v e. D /\ u e. D)) -> ph)   =>   |- ((A e. S /\ B e. S /\ C e. S) -> th)
Theorem	brecop 3242	Binary relation on a quotient set. Lemma for real number construction.
|- S e. V   &   |- Er S   &   |- dom S = (G X. G)   &   |- H = ((G X. G)/.S)   &   |- R = {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))}   &   |- ((((z e. G /\ w e. G) /\ (A e. G /\ B e. G)) /\ ((v e. G /\ u e. G) /\ (C e. G /\ D e. G))) -> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (ph <-> ps)))   =>   |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ([<.A, B>.]SR[<.C, D>.]S <-> ps))
Theorem	brecop2 3243	Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis.
|- S e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   &   |- Er S   &   |- dom S = (G X. G)   &   |- H = ((G X. G)/.S)   &   |- R (_ (H X. H)   &   |- Q (_ (G X. G)   &   |- -. (/) e. G   &   |- dom F = (G X. G)   &   |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ([<.A, B>.]SR[<.C, D>.]S <-> (AFD)Q(BFC)))   =>   |- ([<.A, B>.]SR[<.C, D>.]S <-> (AFD)Q(BFC))
Theorem	ecopopreq 3244	Express the relation R (specified by the hypothesis) in terms of its operation F.
|- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ (zFu) = (wFv)))}   =>   |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> (<.A, B>.R<.C, D>. <-> (AFD) = (BFC)))
Theorem	ecopoprdm 3245	Assuming the operation F is commutative, compute the domain the relation R specified by the first hypothesis.
|- R = {<.x, y