Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | relelec 6601 |
Membership in an equivalence class when 𝑅 is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
|
Theorem | ecss 6602 |
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 6603* |
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 6604 |
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 6605 |
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 6606 |
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 6607 |
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 6608 |
An equivalence class modulo the identity relation is a singleton.
(Contributed by NM, 24-Oct-2004.)
|
⊢ [𝐴] I = {𝐴} |
|
Theorem | qseq1 6609 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) |
|
Theorem | qseq2 6610 |
Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) |
|
Theorem | elqsg 6611* |
Closed form of elqs 6612. (Contributed by Rodolfo Medina,
12-Oct-2010.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)) |
|
Theorem | elqs 6612* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) |
|
Theorem | elqsi 6613* |
Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅) |
|
Theorem | ecelqsg 6614 |
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 6615 |
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 6616 |
"Closure" law for equivalence class of ordered pairs. (Contributed
by
NM, 25-Mar-1996.)
|
⊢ 𝑅 ∈ V & ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [〈𝐵, 𝐶〉]𝑅 ∈ 𝑆) |
|
Theorem | qsexg 6617 |
A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by
Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V) |
|
Theorem | qsex 6618 |
A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 / 𝑅) ∈ V |
|
Theorem | uniqs 6619 |
The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴)) |
|
Theorem | qsss 6620 |
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 6621 |
The union of a quotient set. (Contributed by Mario Carneiro,
11-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝐴)
& ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴) |
|
Theorem | snec 6622 |
The singleton of an equivalence class. (Contributed by NM,
29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅) |
|
Theorem | ecqs 6623 |
Equivalence class in terms of quotient set. (Contributed by NM,
29-Jan-1999.)
|
⊢ 𝑅 ∈ V ⇒ ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅) |
|
Theorem | ecid 6624 |
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 6625 |
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 6626 |
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 6627* |
Implicit substitution of class for equivalence class. (Contributed by
Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑆 = (𝐵 / 𝑅)
& ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑) ⇒ ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓) |
|
Theorem | ectocl 6628* |
Implicit substitution of class for equivalence class. (Contributed by
NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝑆 = (𝐵 / 𝑅)
& ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ 𝐵 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) |
|
Theorem | elqsn0m 6629* |
An element of a quotient set is inhabited. (Contributed by Jim Kingdon,
21-Aug-2019.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → ∃𝑥 𝑥 ∈ 𝐵) |
|
Theorem | elqsn0 6630 |
A quotient set doesn't contain the empty set. (Contributed by NM,
24-Aug-1995.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅) |
|
Theorem | ecelqsdm 6631 |
Membership of an equivalence class in a quotient set. (Contributed by
NM, 30-Jul-1995.)
|
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴) |
|
Theorem | xpider 6632 |
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 6633* |
The intersection of a nonempty family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵) |
|
Theorem | riinerm 6634* |
The relative intersection of a family of equivalence relations is an
equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|
⊢ ((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((𝐵 × 𝐵) ∩ ∩
𝑥 ∈ 𝐴 𝑅) Er 𝐵) |
|
Theorem | erinxp 6635 |
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 6636 |
Restrict the relation in an equivalence class to a base set. (Contributed
by Mario Carneiro, 10-Jul-2015.)
|
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴))) |
|
Theorem | qsinxp 6637 |
Restrict the equivalence relation in a quotient set to the base set.
(Contributed by Mario Carneiro, 23-Feb-2015.)
|
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) |
|
Theorem | qsel 6638 |
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 6639* |
𝐹,
a function lift, is a subset of 𝑅 × 𝑆. (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) |
|
Theorem | qliftrel 6640* |
𝐹,
a function lift, is a subset of 𝑅 × 𝑆. (Contributed by
Mario Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) |
|
Theorem | qliftel 6641* |
Elementhood in the relation 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) |
|
Theorem | qliftel1 6642* |
Elementhood in the relation 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) |
|
Theorem | qliftfun 6643* |
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 6644* |
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 6645* |
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 6646* |
The domain and codomain of the function 𝐹. (Contributed by Mario
Carneiro, 23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) |
|
Theorem | qliftval 6647* |
The value of the function 𝐹. (Contributed by Mario Carneiro,
23-Dec-2016.)
|
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈[𝑥]𝑅, 𝐴〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)
& ⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵)
& ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) |
|
Theorem | ecoptocl 6648* |
Implicit substitution of class for equivalence class of ordered pair.
(Contributed by NM, 23-Jul-1995.)
|
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) |
|
Theorem | 2ecoptocl 6649* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 23-Jul-1995.)
|
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) |
|
Theorem | 3ecoptocl 6650* |
Implicit substitution of classes for equivalence classes of ordered
pairs. (Contributed by NM, 9-Aug-1995.)
|
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅)
& ⊢ ([〈𝑥, 𝑦〉]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([〈𝑧, 𝑤〉]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([〈𝑣, 𝑢〉]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) |
|
Theorem | brecop 6651* |
Binary relation on a quotient set. Lemma for real number construction.
(Contributed by NM, 29-Jan-1996.)
|
⊢ ∼ ∈
V
& ⊢ ∼ Er (𝐺 × 𝐺)
& ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ∼ ∧ 𝑦 = [〈𝑣, 𝑢〉] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([〈𝑧, 𝑤〉] ∼ = [〈𝐴, 𝐵〉] ∼ ∧ [〈𝑣, 𝑢〉] ∼ = [〈𝐶, 𝐷〉] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([〈𝐴, 𝐵〉] ∼ ≤ [〈𝐶, 𝐷〉] ∼ ↔ 𝜓)) |
|
Theorem | eroveu 6652* |
Lemma for eroprf 6654. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
|
Theorem | erovlem 6653* |
Lemma for eroprf 6654. (Contributed by Jeff Madsen, 10-Jun-2010.)
(Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ 𝐽 = (𝐴 / 𝑅)
& ⊢ 𝐾 = (𝐵 / 𝑆)
& ⊢ (𝜑 → 𝑇 ∈ 𝑍)
& ⊢ (𝜑 → 𝑅 Er 𝑈)
& ⊢ (𝜑 → 𝑆 Er 𝑉)
& ⊢ (𝜑 → 𝑇 Er 𝑊)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → 𝐵 ⊆ 𝑉)
& ⊢ (𝜑 → 𝐶 ⊆ 𝑊)
& ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |
|
Theorem | eroprf 6654* |
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 6655* |
Functionality of an operation defined on equivalence classes.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
& ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)
& ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) |
|
Theorem | ecopoveq 6656* |
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 6657* |
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 6658* |
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 6659* |
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 6660* |
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 6661* |
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 6662* |
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 6663* |
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 6664* |
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 6665* |
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 6666* |
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 6667* |
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 6668* |
Lemma used to transfer a commutative law via an equivalence relation.
Most uses will want ecovicom 6669 instead. (Contributed by NM,
29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ 𝐷 = 𝐻
& ⊢ 𝐺 = 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | ecovicom 6669* |
Lemma used to transfer a commutative law via an equivalence relation.
(Contributed by Jim Kingdon, 15-Sep-2019.)
|
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐷, 𝐺〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑥, 𝑦〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐷 = 𝐻)
& ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → 𝐺 = 𝐽) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | ecovass 6670* |
Lemma used to transfer an associative law via an equivalence relation.
In most cases ecoviass 6671 will be more useful. (Contributed by NM,
31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐺, 𝐻〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑁, 𝑄〉] ∼ ) & ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ ) = [〈𝐿, 𝑀〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) & ⊢ 𝐽 = 𝐿
& ⊢ 𝐾 = 𝑀 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
|
Theorem | ecoviass 6671* |
Lemma used to transfer an associative law via an equivalence relation.
(Contributed by Jim Kingdon, 16-Sep-2019.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑧, 𝑤〉] ∼ ) = [〈𝐺, 𝐻〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑁, 𝑄〉] ∼ ) & ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝐺, 𝐻〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝐽, 𝐾〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ + [〈𝑁, 𝑄〉] ∼ ) = [〈𝐿, 𝑀〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐽 = 𝐿)
& ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐾 = 𝑀) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
|
Theorem | ecovdi 6672* |
Lemma used to transfer a distributive law via an equivalence relation.
Most likely ecovidi 6673 will be more helpful. (Contributed by NM,
2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑀, 𝑁〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑀, 𝑁〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑧, 𝑤〉] ∼ ) = [〈𝑊, 𝑋〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑣, 𝑢〉] ∼ ) = [〈𝑌, 𝑍〉] ∼ ) & ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([〈𝑊, 𝑋〉] ∼ + [〈𝑌, 𝑍〉] ∼ ) = [〈𝐾, 𝐿〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) & ⊢ 𝐻 = 𝐾
& ⊢ 𝐽 = 𝐿 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
|
Theorem | ecovidi 6673* |
Lemma used to transfer a distributive law via an equivalence relation.
(Contributed by Jim Kingdon, 17-Sep-2019.)
|
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑧, 𝑤〉] ∼ + [〈𝑣, 𝑢〉] ∼ ) = [〈𝑀, 𝑁〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑀, 𝑁〉] ∼ ) = [〈𝐻, 𝐽〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑧, 𝑤〉] ∼ ) = [〈𝑊, 𝑋〉] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([〈𝑥, 𝑦〉] ∼ · [〈𝑣, 𝑢〉] ∼ ) = [〈𝑌, 𝑍〉] ∼ ) & ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([〈𝑊, 𝑋〉] ∼ + [〈𝑌, 𝑍〉] ∼ ) = [〈𝐾, 𝐿〉] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐻 = 𝐾)
& ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → 𝐽 = 𝐿) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
|
2.6.26 The mapping operation
|
|
Syntax | cmap 6674 |
Extend the definition of a class to include the mapping operation. (Read
for 𝐴
↑𝑚 𝐵, "the set of all functions that
map from 𝐵 to
𝐴.)
|
class ↑𝑚 |
|
Syntax | cpm 6675 |
Extend the definition of a class to include the partial mapping operation.
(Read for 𝐴 ↑pm 𝐵, "the set of all
partial functions that map from
𝐵 to 𝐴.)
|
class ↑pm |
|
Definition | df-map 6676* |
Define the mapping operation or set exponentiation. The set of all
functions that map from 𝐵 to 𝐴 is written (𝐴
↑𝑚 𝐵) (see
mapval 6686). Many authors write 𝐴 followed by 𝐵 as a
superscript
for this operation and rely on context to avoid confusion other
exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring]
p. 95). Other authors show 𝐵 as a prefixed superscript, which is
read "𝐴 pre 𝐵 " (e.g., definition
of [Enderton] p. 52).
Definition 8.21 of [Eisenberg] p. 125
uses the notation Map(𝐵,
𝐴) for our (𝐴 ↑𝑚
𝐵). The up-arrow is
used by Donald Knuth
for iterated exponentiation (Science 194, 1235-1242, 1976). We
adopt
the first case of his notation (simple exponentiation) and subscript it
with m to distinguish it from other kinds of exponentiation.
(Contributed by NM, 8-Dec-2003.)
|
⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) |
|
Definition | df-pm 6677* |
Define the partial mapping operation. A partial function from 𝐵 to
𝐴 is a function from a subset of 𝐵 to
𝐴.
The set of all
partial functions from 𝐵 to 𝐴 is written (𝐴
↑pm 𝐵) (see
pmvalg 6685). A notation for this operation apparently
does not appear in
the literature. We use ↑pm to distinguish it from the less
general
set exponentiation operation ↑𝑚 (df-map 6676) . See mapsspm 6708 for
its relationship to set exponentiation. (Contributed by NM,
15-Nov-2007.)
|
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) |
|
Theorem | mapprc 6678* |
When 𝐴 is a proper class, the class of all
functions mapping 𝐴
to 𝐵 is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed
by NM, 8-Dec-2003.)
|
⊢ (¬ 𝐴 ∈ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅) |
|
Theorem | pmex 6679* |
The class of all partial functions from one set to another is a set.
(Contributed by NM, 15-Nov-2007.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ (Fun 𝑓 ∧ 𝑓 ⊆ (𝐴 × 𝐵))} ∈ V) |
|
Theorem | mapex 6680* |
The class of all functions mapping one set to another is a set. Remark
after Definition 10.24 of [Kunen] p. 31.
(Contributed by Raph Levien,
4-Dec-2003.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) |
|
Theorem | fnmap 6681 |
Set exponentiation has a universal domain. (Contributed by NM,
8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⊢ ↑𝑚 Fn (V ×
V) |
|
Theorem | fnpm 6682 |
Partial function exponentiation has a universal domain. (Contributed by
Mario Carneiro, 14-Nov-2013.)
|
⊢ ↑pm Fn (V ×
V) |
|
Theorem | reldmmap 6683 |
Set exponentiation is a well-behaved binary operator. (Contributed by
Stefan O'Rear, 27-Feb-2015.)
|
⊢ Rel dom
↑𝑚 |
|
Theorem | mapvalg 6684* |
The value of set exponentiation. (𝐴 ↑𝑚 𝐵) is the set of all
functions that map from 𝐵 to 𝐴. Definition 10.24 of
[Kunen]
p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑𝑚 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴}) |
|
Theorem | pmvalg 6685* |
The value of the partial mapping operation. (𝐴 ↑pm 𝐵) is the set
of all partial functions that map from 𝐵 to 𝐴.
(Contributed by
NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) |
|
Theorem | mapval 6686* |
The value of set exponentiation (inference version). (𝐴 ↑𝑚
𝐵) is
the set of all functions that map from 𝐵 to 𝐴.
Definition
10.24 of [Kunen] p. 24. (Contributed by
NM, 8-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ↑𝑚 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴} |
|
Theorem | elmapg 6687 |
Membership relation for set exponentiation. (Contributed by NM,
17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
|
Theorem | elmapd 6688 |
Deduction form of elmapg 6687. (Contributed by BJ, 11-Apr-2020.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
|
Theorem | mapdm0 6689 |
The empty set is the only map with empty domain. (Contributed by Glauco
Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux,
3-Dec-2021.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐵 ↑𝑚 ∅) =
{∅}) |
|
Theorem | elpmg 6690 |
The predicate "is a partial function". (Contributed by Mario
Carneiro,
14-Nov-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐶 ∧ 𝐶 ⊆ (𝐵 × 𝐴)))) |
|
Theorem | elpm2g 6691 |
The predicate "is a partial function". (Contributed by NM,
31-Dec-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) |
|
Theorem | elpm2r 6692 |
Sufficient condition for being a partial function. (Contributed by NM,
31-Dec-2013.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) |
|
Theorem | elpmi 6693 |
A partial function is a function. (Contributed by Mario Carneiro,
15-Sep-2015.)
|
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) |
|
Theorem | pmfun 6694 |
A partial function is a function. (Contributed by Mario Carneiro,
30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → Fun 𝐹) |
|
Theorem | elmapex 6695 |
Eliminate antecedent for mapping theorems: domain can be taken to be a
set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V)) |
|
Theorem | elmapi 6696 |
A mapping is a function, forward direction only with superfluous
antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵) |
|
Theorem | elmapfn 6697 |
A mapping is a function with the appropriate domain. (Contributed by AV,
6-Apr-2019.)
|
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴 Fn 𝐶) |
|
Theorem | elmapfun 6698 |
A mapping is always a function. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → Fun 𝐴) |
|
Theorem | elmapssres 6699 |
A restricted mapping is a mapping. (Contributed by Stefan O'Rear,
9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|
⊢ ((𝐴 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑𝑚 𝐷)) |
|
Theorem | fpmg 6700 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴)) |