Theorem List for Intuitionistic Logic Explorer - 6101-6200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nnawordex 6101* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵)) |
|
Theorem | nnm00 6102 |
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |
|
2.6.24 Equivalence relations and
classes
|
|
Syntax | wer 6103 |
Extend the definition of a wff to include the equivalence predicate.
|
wff 𝑅 Er 𝐴 |
|
Syntax | cec 6104 |
Extend the definition of a class to include equivalence class.
|
class [𝐴]𝑅 |
|
Syntax | cqs 6105 |
Extend the definition of a class to include quotient set.
|
class (𝐴 / 𝑅) |
|
Definition | df-er 6106 |
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 6107 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6126, ersymb 6120, and ertr 6121.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) |
|
Theorem | dfer2 6107* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
|
Definition | df-ec 6108 |
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 Er 𝑅; see dfer2 6107). In this case,
𝐴 is a representative (member) of the
equivalence class [𝐴]𝑅,
which contains all sets that are equivalent to 𝐴. Definition of
[Enderton] p. 57 uses the notation [𝐴]
(subscript) 𝑅, although
we simply follow the brackets by 𝑅 since we don't have subscripted
expressions. For an alternate definition, see dfec2 6109. (Contributed by
NM, 23-Jul-1995.)
|
⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) |
|
Theorem | dfec2 6109* |
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.)
|
⊢ (𝐴 ∈ 𝑉 → [𝐴]𝑅 = {𝑦 ∣ 𝐴𝑅𝑦}) |
|
Theorem | ecexg 6110 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V) |
|
Theorem | ecexr 6111 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V) |
|
Definition | df-qs 6112* |
Define quotient set. 𝑅 is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
|
Theorem | ereq1 6113 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴)) |
|
Theorem | ereq2 6114 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵)) |
|
Theorem | errel 6115 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → Rel 𝑅) |
|
Theorem | erdm 6116 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) |
|
Theorem | ercl 6117 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑋) |
|
Theorem | ersym 6118 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) |
|
Theorem | ercl2 6119 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑋) |
|
Theorem | ersymb 6120 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
|
Theorem | ertr 6121 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
|
Theorem | ertrd 6122 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ertr2d 6123 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐴) |
|
Theorem | ertr3d 6124 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐵𝑅𝐴)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ertr4d 6125 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | erref 6126 |
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.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐴) |
|
Theorem | ercnv 6127 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅) |
|
Theorem | errn 6128 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → ran 𝑅 = 𝐴) |
|
Theorem | erssxp 6129 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) |
|
Theorem | erex 6130 |
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.)
|
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V)) |
|
Theorem | erexb 6131 |
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.)
|
⊢ (𝑅 Er 𝐴 → (𝑅 ∈ V ↔ 𝐴 ∈ V)) |
|
Theorem | iserd 6132* |
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.)
|
⊢ (𝜑 → Rel 𝑅)
& ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥)
& ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧)
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Er 𝐴) |
|
Theorem | brdifun 6133 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ <
)) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | swoer 6134* |
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.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Er 𝑋) |
|
Theorem | swoord1 6135* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) |
|
Theorem | swoord2 6136* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) |
|
Theorem | eqerlem 6137* |
Lemma for eqer 6138. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) |
|
Theorem | eqer 6138* |
Equivalence relation involving equality of dependent classes 𝐴(𝑥)
and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.)
(Revised by Mario
Carneiro, 12-Aug-2015.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ 𝑅 Er V |
|
Theorem | ider 6139 |
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 |
|
Theorem | 0er 6140 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
⊢ ∅ Er ∅ |
|
Theorem | eceq1 6141 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) |
|
Theorem | eceq1d 6142 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) |
|
Theorem | eceq2 6143 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) |
|
Theorem | elecg 6144 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
|
Theorem | elec 6145 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) |
|
Theorem | relelec 6146 |
Membership in an equivalence class when 𝑅 is a relation.
(Contributed by Mario Carneiro, 11-Sep-2015.)
|
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
|
Theorem | ecss 6147 |
An equivalence class is a subset of the domain. (Contributed by NM,
6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → [𝐴]𝑅 ⊆ 𝑋) |
|
Theorem | ecdmn0m 6148* |
A representative of an inhabited equivalence class belongs to the domain
of the equivalence relation. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
⊢ (𝐴 ∈ dom 𝑅 ↔ ∃𝑥 𝑥 ∈ [𝐴]𝑅) |
|
Theorem | ereldm 6149 |
Equality of equivalence classes implies equivalence of domain
membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) |
|
Theorem | erth 6150 |
Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro,
6-Jul-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) |
|
Theorem | erth2 6151 |
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.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) |
|
Theorem | erthi 6152 |
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.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) |
|
Theorem | ecidsn 6153 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
⊢ [𝐴] I = {𝐴} |
|
Theorem | qseq1 6154 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) |
|
Theorem | qseq2 6155 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) |
|
Theorem | elqsg 6156* |
Closed form of elqs 6157. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) |
|
Theorem | elqs 6157* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) |
|
Theorem | elqsi 6158* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) |
|
Theorem | ecelqsg 6159 |
Membership of an equivalence class in a quotient set. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) |
|
Theorem | ecelqsi 6160 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑅 ∈ V ⇒ ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) |
|
Theorem | ecopqsi 6161 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [〈𝐵, 𝐶〉]𝑅 ∈ 𝑆) |
|
Theorem | qsexg 6162 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) |
|
Theorem | qsex 6163 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V |
|
Theorem | uniqs 6164 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) |
|
Theorem | qsss 6165 |
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.)
|
⊢ (𝜑 → 𝑅 Er 𝐴) ⇒ ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴) |
|
Theorem | uniqs2 6166 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝐴)
& ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) |
|
Theorem | snec 6167 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) |
|
Theorem | ecqs 6168 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) |
|
Theorem | ecid 6169 |
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.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ [𝐴]◡
E = 𝐴 |
|
Theorem | ecidg 6170 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.) (Contributed by Jim Kingdon,
8-Jan-2020.)
|
⊢ (𝐴 ∈ 𝑉 → [𝐴]◡
E = 𝐴) |
|
Theorem | qsid 6171 |
A set is equal to its quotient set mod converse epsilon. (Note:
converse epsilon is not an equivalence relation.) (Contributed by NM,
13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 / ◡ E ) = 𝐴 |
|
Theorem | ectocld 6172* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑆 = (𝐵 / 𝑅)
& ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
|
Theorem | ectocl 6173* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑆 = (𝐵 / 𝑅)
& ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) |
|
Theorem | elqsn0m 6174* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → ∃𝑥 𝑥 ∈ 𝐵) |
|
Theorem | elqsn0 6175 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) |
|
Theorem | ecelqsdm 6176 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) |
|
Theorem | xpiderm 6177* |
A square Cartesian product is an equivalence relation (in general it's
not a poset). (Contributed by Jim Kingdon, 22-Aug-2019.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐴 × 𝐴) Er 𝐴) |
|
Theorem | iinerm 6178* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) |
|
Theorem | riinerm 6179* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((𝐵 × 𝐵) ∩ ∩
𝑥 ∈ 𝐴 𝑅) Er 𝐵) |
|
Theorem | erinxp 6180 |
A restricted equivalence relation is an equivalence relation.
(Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝐴)
& ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑅 ∩ (𝐵 × 𝐵)) Er 𝐵) |
|
Theorem | ecinxp 6181 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) |
|
Theorem | qsinxp 6182 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) |
|
Theorem | qsel 6183 |
If an element of a quotient set contains a given element, it is equal to
the equivalence class of the element. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ ((𝑅 Er 𝑋 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅) |
|
Theorem | qliftlem 6184* |
𝐹,
a function lift, is a subset of 𝑅 × 𝑆. (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) |
|
Theorem | qliftrel 6185* |
𝐹,
a function lift, is a subset of 𝑅 × 𝑆. (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) |
|
Theorem | qliftel 6186* |
Elementhood in the relation 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) |
|
Theorem | qliftel1 6187* |
Elementhood in the relation 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) |
|
Theorem | qliftfun 6188* |
The function 𝐹 is the unique function defined by
𝐹‘[𝑥] = 𝐴, provided that the well-definedness
condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵))) |
|
Theorem | qliftfund 6189* |
The function 𝐹 is the unique function defined by
𝐹‘[𝑥] = 𝐴, provided that the well-definedness
condition
holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Fun 𝐹) |
|
Theorem | qliftfuns 6190* |
The function 𝐹 is the unique function defined by
𝐹‘[𝑥] = 𝐴, provided that the well-definedness
condition holds.
(Contributed by Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦∀𝑧(𝑦𝑅𝑧 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴))) |
|
Theorem | qliftf 6191* |
The domain and range of the function 𝐹. (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) |
|
Theorem | qliftval 6192* |
The value of the function 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵)
& ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) |
|
Theorem | ecoptocl 6193* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) |
|
Theorem | 2ecoptocl 6194* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) |
|
Theorem | 3ecoptocl 6195* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([〈𝑣, 𝑢〉]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) |
|
Theorem | brecop 6196* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
⊢ ∼ ∈
V
& ⊢ ∼ Er (𝐺 × 𝐺)
& ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ∼ ∧ 𝑦 = [〈𝑣, 𝑢〉] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([〈𝑧, 𝑤〉] ∼ = [〈𝐴, 𝐵〉] ∼ ∧ [〈𝑣, 𝑢〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([〈𝐴, 𝐵〉] ∼ ≤ [〈𝐶, 𝐷〉] ∼ ↔ 𝜓)) |
|
Theorem | eroveu 6197* |
Lemma for eroprf 6199. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
|
Theorem | erovlem 6198* |
Lemma for eroprf 6199. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |
|
Theorem | eroprf 6199* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} & ⊢ (𝜑 → 𝑅 ∈ 𝑋)
& ⊢ (𝜑 → 𝑆 ∈ 𝑌)
& ⊢ 𝐿 = (𝐶 / 𝑇) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐾)⟶𝐿) |
|
Theorem | eroprf2 6200* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) |