Theorem List for Intuitionistic Logic Explorer - 6501-6600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | errel 6501 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → Rel 𝑅) |
|
Theorem | erdm 6502 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) |
|
Theorem | ercl 6503 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑋) |
|
Theorem | ersym 6504 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) |
|
Theorem | ercl2 6505 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑋) |
|
Theorem | ersymb 6506 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
|
Theorem | ertr 6507 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
|
Theorem | ertrd 6508 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ertr2d 6509 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐴) |
|
Theorem | ertr3d 6510 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐵𝑅𝐴)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ertr4d 6511 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | erref 6512 |
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 6513 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅) |
|
Theorem | errn 6514 |
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 6515 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) |
|
Theorem | erex 6516 |
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 6517 |
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 6518* |
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 6519 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ <
)) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | swoer 6520* |
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 6521* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) |
|
Theorem | swoord2 6522* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) |
|
Theorem | eqerlem 6523* |
Lemma for eqer 6524. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) |
|
Theorem | eqer 6524* |
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 6525 |
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 6526 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
⊢ ∅ Er ∅ |
|
Theorem | eceq1 6527 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) |
|
Theorem | eceq1d 6528 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) |
|
Theorem | eceq2 6529 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) |
|
Theorem | elecg 6530 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
|
Theorem | elec 6531 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) |
|
Theorem | relelec 6532 |
Membership in an equivalence class when 𝑅 is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
|
Theorem | ecss 6533 |
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 6534* |
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 6535 |
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 6536 |
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 6537 |
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 6538 |
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 6539 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
⊢ [𝐴] I = {𝐴} |
|
Theorem | qseq1 6540 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) |
|
Theorem | qseq2 6541 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) |
|
Theorem | elqsg 6542* |
Closed form of elqs 6543. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) |
|
Theorem | elqs 6543* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) |
|
Theorem | elqsi 6544* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) |
|
Theorem | ecelqsg 6545 |
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 6546 |
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 6547 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [〈𝐵, 𝐶〉]𝑅 ∈ 𝑆) |
|
Theorem | qsexg 6548 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) |
|
Theorem | qsex 6549 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V |
|
Theorem | uniqs 6550 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) |
|
Theorem | qsss 6551 |
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 6552 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝐴)
& ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) |
|
Theorem | snec 6553 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) |
|
Theorem | ecqs 6554 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) |
|
Theorem | ecid 6555 |
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 6556 |
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 6557 |
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 6558* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑆 = (𝐵 / 𝑅)
& ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
|
Theorem | ectocl 6559* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑆 = (𝐵 / 𝑅)
& ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) |
|
Theorem | elqsn0m 6560* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → ∃𝑥 𝑥 ∈ 𝐵) |
|
Theorem | elqsn0 6561 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) |
|
Theorem | ecelqsdm 6562 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) |
|
Theorem | xpider 6563 |
A square Cartesian product is an equivalence relation (in general it's not
a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝐴 × 𝐴) Er 𝐴 |
|
Theorem | iinerm 6564* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) |
|
Theorem | riinerm 6565* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((𝐵 × 𝐵) ∩ ∩
𝑥 ∈ 𝐴 𝑅) Er 𝐵) |
|
Theorem | erinxp 6566 |
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 6567 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) |
|
Theorem | qsinxp 6568 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) |
|
Theorem | qsel 6569 |
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 6570* |
𝐹,
a function lift, is a subset of 𝑅 × 𝑆. (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) |
|
Theorem | qliftrel 6571* |
𝐹,
a function lift, is a subset of 𝑅 × 𝑆. (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) |
|
Theorem | qliftel 6572* |
Elementhood in the relation 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) |
|
Theorem | qliftel1 6573* |
Elementhood in the relation 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) |
|
Theorem | qliftfun 6574* |
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 6575* |
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 6576* |
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 6577* |
The domain and range of the function 𝐹. (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) |
|
Theorem | qliftval 6578* |
The value of the function 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵)
& ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) |
|
Theorem | ecoptocl 6579* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) |
|
Theorem | 2ecoptocl 6580* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) |
|
Theorem | 3ecoptocl 6581* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([〈𝑣, 𝑢〉]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) |
|
Theorem | brecop 6582* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
⊢ ∼ ∈
V
& ⊢ ∼ Er (𝐺 × 𝐺)
& ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ∼ ∧ 𝑦 = [〈𝑣, 𝑢〉] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([〈𝑧, 𝑤〉] ∼ = [〈𝐴, 𝐵〉] ∼ ∧ [〈𝑣, 𝑢〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([〈𝐴, 𝐵〉] ∼ ≤ [〈𝐶, 𝐷〉] ∼ ↔ 𝜓)) |
|
Theorem | eroveu 6583* |
Lemma for eroprf 6585. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
|
Theorem | erovlem 6584* |
Lemma for eroprf 6585. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |
|
Theorem | eroprf 6585* |
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 6586* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) |
|
Theorem | ecopoveq 6587* |
This is the first of several theorems about equivalence relations of
the kind used in construction of fractions and signed reals, involving
operations on equivalent classes of ordered pairs. This theorem
expresses the relation ∼ (specified
by the hypothesis) in terms
of its operation 𝐹. (Contributed by NM, 16-Aug-1995.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (〈𝐴, 𝐵〉 ∼ 〈𝐶, 𝐷〉 ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) |
|
Theorem | ecopovsym 6588* |
Assuming the operation 𝐹 is commutative, show that the
relation
∼, specified
by the first hypothesis, is symmetric.
(Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) ⇒ ⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) |
|
Theorem | ecopovtrn 6589* |
Assuming that operation 𝐹 is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
∼, specified
by the first hypothesis, is transitive.
(Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶) |
|
Theorem | ecopover 6590* |
Assuming that operation 𝐹 is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
∼, specified
by the first hypothesis, is an equivalence
relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario
Carneiro, 12-Aug-2015.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ∼ Er (𝑆 × 𝑆) |
|
Theorem | ecopovsymg 6591* |
Assuming the operation 𝐹 is commutative, show that the
relation
∼, specified
by the first hypothesis, is symmetric.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴) |
|
Theorem | ecopovtrng 6592* |
Assuming that operation 𝐹 is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
∼, specified
by the first hypothesis, is transitive.
(Contributed by Jim Kingdon, 1-Sep-2019.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶) |
|
Theorem | ecopoverg 6593* |
Assuming that operation 𝐹 is commutative (second hypothesis),
closed (third hypothesis), associative (fourth hypothesis), and has
the cancellation property (fifth hypothesis), show that the relation
∼, specified
by the first hypothesis, is an equivalence
relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
|
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ∼ Er (𝑆 × 𝑆) |
|
Theorem | th3qlem1 6594* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The
third hypothesis is the compatibility assumption. (Contributed by NM,
3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ ∼ Er 𝑆 & ⊢ (((𝑦 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∼ 𝑤 ∧ 𝑧 ∼ 𝑣) → (𝑦 + 𝑧) ∼ (𝑤 + 𝑣))) ⇒ ⊢ ((𝐴 ∈ (𝑆 / ∼ ) ∧ 𝐵 ∈ (𝑆 / ∼ )) →
∃*𝑥∃𝑦∃𝑧((𝐴 = [𝑦] ∼ ∧ 𝐵 = [𝑧] ∼ ) ∧ 𝑥 = [(𝑦 + 𝑧)] ∼
)) |
|
Theorem | th3qlem2 6595* |
Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60,
extended to operations on ordered pairs. The fourth hypothesis is the
compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
⊢ ∼ ∈
V
& ⊢ ∼ Er (𝑆 × 𝑆)
& ⊢ ((((𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ 𝑓 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((〈𝑤, 𝑣〉 ∼ 〈𝑢, 𝑡〉 ∧ 〈𝑠, 𝑓〉 ∼ 〈𝑔, ℎ〉) → (〈𝑤, 𝑣〉 + 〈𝑠, 𝑓〉) ∼ (〈𝑢, 𝑡〉 + 〈𝑔, ℎ〉))) ⇒ ⊢ ((𝐴 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝐵 ∈ ((𝑆 × 𝑆) / ∼ )) →
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ∼ ∧ 𝐵 = [〈𝑢, 𝑡〉] ∼ ) ∧ 𝑧 = [(〈𝑤, 𝑣〉 + 〈𝑢, 𝑡〉)] ∼
)) |
|
Theorem | th3qcor 6596* |
Corollary of Theorem 3Q of [Enderton] p. 60.
(Contributed by NM,
12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ ∼ ∈
V
& ⊢ ∼ Er (𝑆 × 𝑆)
& ⊢ ((((𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ 𝑓 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((〈𝑤, 𝑣〉 ∼ 〈𝑢, 𝑡〉 ∧ 〈𝑠, 𝑓〉 ∼ 〈𝑔, ℎ〉) → (〈𝑤, 𝑣〉 + 〈𝑠, 𝑓〉) ∼ (〈𝑢, 𝑡〉 + 〈𝑔, ℎ〉))) & ⊢ 𝐺 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ∼ ∧ 𝑦 = [〈𝑢, 𝑡〉] ∼ ) ∧ 𝑧 = [(〈𝑤, 𝑣〉 + 〈𝑢, 𝑡〉)] ∼
))} ⇒ ⊢ Fun 𝐺 |
|
Theorem | th3q 6597* |
Theorem 3Q of [Enderton] p. 60, extended to
operations on ordered
pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
⊢ ∼ ∈
V
& ⊢ ∼ Er (𝑆 × 𝑆)
& ⊢ ((((𝑤 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) ∧ ((𝑠 ∈ 𝑆 ∧ 𝑓 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆))) → ((〈𝑤, 𝑣〉 ∼ 〈𝑢, 𝑡〉 ∧ 〈𝑠, 𝑓〉 ∼ 〈𝑔, ℎ〉) → (〈𝑤, 𝑣〉 + 〈𝑠, 𝑓〉) ∼ (〈𝑢, 𝑡〉 + 〈𝑔, ℎ〉))) & ⊢ 𝐺 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((𝑆 × 𝑆) / ∼ ) ∧ 𝑦 ∈ ((𝑆 × 𝑆) / ∼ )) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ∼ ∧ 𝑦 = [〈𝑢, 𝑡〉] ∼ ) ∧ 𝑧 = [(〈𝑤, 𝑣〉 + 〈𝑢, 𝑡〉)] ∼
))} ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈𝐴, 𝐵〉] ∼ 𝐺[〈𝐶, 𝐷〉] ∼ ) = [(〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉)] ∼ ) |
|
Theorem | oviec 6598* |
Express an operation on equivalence classes of ordered pairs in terms of
equivalence class of operations on ordered pairs. See iset.mm for
additional comments describing the hypotheses. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 4-Jun-2013.)
(Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro,
4-Jun-2013.)
|
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 𝐻 ∈ (𝑆 × 𝑆)) & ⊢ (((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆)) → 𝐾 ∈ (𝑆 × 𝑆)) & ⊢ (((𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → 𝐿 ∈ (𝑆 × 𝑆)) & ⊢ ∼
∈ V
& ⊢ ∼ Er (𝑆 × 𝑆)
& ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ 𝜑))} & ⊢ (((𝑧 = 𝑎 ∧ 𝑤 = 𝑏) ∧ (𝑣 = 𝑐 ∧ 𝑢 = 𝑑)) → (𝜑 ↔ 𝜓)) & ⊢ (((𝑧 = 𝑔 ∧ 𝑤 = ℎ) ∧ (𝑣 = 𝑡 ∧ 𝑢 = 𝑠)) → (𝜑 ↔ 𝜒)) & ⊢ + =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝐽))} & ⊢ (((𝑤 = 𝑎 ∧ 𝑣 = 𝑏) ∧ (𝑢 = 𝑔 ∧ 𝑓 = ℎ)) → 𝐽 = 𝐾)
& ⊢ (((𝑤 = 𝑐 ∧ 𝑣 = 𝑑) ∧ (𝑢 = 𝑡 ∧ 𝑓 = 𝑠)) → 𝐽 = 𝐿)
& ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝐽 = 𝐻)
& ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ∧ ∃𝑎∃𝑏∃𝑐∃𝑑((𝑥 = [〈𝑎, 𝑏〉] ∼ ∧ 𝑦 = [〈𝑐, 𝑑〉] ∼ ) ∧ 𝑧 = [(〈𝑎, 𝑏〉 + 〈𝑐, 𝑑〉)] ∼ ))} & ⊢ 𝑄 = ((𝑆 × 𝑆) / ∼ ) & ⊢ ((((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) ∧ (𝑐 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ ((𝑔 ∈ 𝑆 ∧ ℎ ∈ 𝑆) ∧ (𝑡 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆))) → ((𝜓 ∧ 𝜒) → 𝐾 ∼ 𝐿)) ⇒ ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ([〈𝐴, 𝐵〉] ∼ ⨣ [〈𝐶, 𝐷〉] ∼ ) = [𝐻] ∼ ) |
|
Theorem | ecovcom 6599* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6600 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ 𝐷 = 𝐻
& ⊢ 𝐺 = 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | ecovicom 6600* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐷 = 𝐻)
& ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐺 = 𝐽) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |