![]() |
Metamath
Proof Explorer Theorem List (p. 89 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qsinxp 8801 | Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | qsdisj 8802 | Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) |
⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅)) ⇒ ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
Theorem | qsdisj2 8803* | A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥) | ||
Theorem | qsel 8804 | 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 | uniinqs 8805 | Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4929. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.) |
⊢ 𝑅 Er 𝑋 ⇒ ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶)) | ||
Theorem | qliftlem 8806* | Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅)) | ||
Theorem | qliftrel 8807* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌)) | ||
Theorem | qliftel 8808* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴))) | ||
Theorem | qliftel1 8809* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴) | ||
Theorem | qliftfun 8810* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵))) | ||
Theorem | qliftfund 8811* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | qliftfuns 8812* | The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦∀𝑧(𝑦𝑅𝑧 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴))) | ||
Theorem | qliftf 8813* | The domain and codomain of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌)) | ||
Theorem | qliftval 8814* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵) | ||
Theorem | ecoptocl 8815* | Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅) & ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑆 → 𝜓) | ||
Theorem | 2ecoptocl 8816* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.) |
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅) & ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒) | ||
Theorem | 3ecoptocl 8817* | Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.) |
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅) & ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ([⟨𝑣, 𝑢⟩]𝑅 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃) | ||
Theorem | brecop 8818* | Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.) |
⊢ ∼ ∈ V & ⊢ ∼ Er (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ∼ ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ∼ ) ∧ 𝜑))} & ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([⟨𝑧, 𝑤⟩] ∼ = [⟨𝐴, 𝐵⟩] ∼ ∧ [⟨𝑣, 𝑢⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → (𝜑 ↔ 𝜓))) ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ ≤ [⟨𝐶, 𝐷⟩] ∼ ↔ 𝜓)) | ||
Theorem | brecop2 8819 | Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996.) (Revised by AV, 12-Jul-2022.) |
⊢ dom ∼ = (𝐺 × 𝐺) & ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ ) & ⊢ 𝑅 ⊆ (𝐻 × 𝐻) & ⊢ ≤ ⊆ (𝐺 × 𝐺) & ⊢ ¬ ∅ ∈ 𝐺 & ⊢ dom + = (𝐺 × 𝐺) & ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶))) ⇒ ⊢ ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶)) | ||
Theorem | eroveu 8820* | Lemma for erov 8822 and eroprf 8823. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) | ||
Theorem | erovlem 8821* | Lemma for erov 8822 and eroprf 8823. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.) |
⊢ 𝐽 = (𝐴 / 𝑅) & ⊢ 𝐾 = (𝐵 / 𝑆) & ⊢ (𝜑 → 𝑇 ∈ 𝑍) & ⊢ (𝜑 → 𝑅 Er 𝑈) & ⊢ (𝜑 → 𝑆 Er 𝑉) & ⊢ (𝜑 → 𝑇 Er 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ 𝑊) & ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} ⇒ ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) | ||
Theorem | erov 8822* | The value 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 | eroprf 8823* | 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 | erov2 8824* | The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ ) | ||
Theorem | eroprf2 8825* | Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐽 = (𝐴 / ∼ ) & ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )} & ⊢ (𝜑 → ∼ ∈ 𝑋) & ⊢ (𝜑 → ∼ Er 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝑈) & ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴) & ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢))) ⇒ ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽) | ||
Theorem | ecopoveq 8826* | 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 8827* | 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 8828* | 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 8829* | 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.) (Proof shortened by AV, 1-May-2021.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} & ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ∼ Er (𝑆 × 𝑆) | ||
Theorem | eceqoveq 8830* | Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ Er (𝑆 × 𝑆) & ⊢ dom + = (𝑆 × 𝑆) & ⊢ ¬ ∅ ∈ 𝑆 & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶))) | ||
Theorem | ecovcom 8831* | Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐷, 𝐺⟩] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑥, 𝑦⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ ) & ⊢ 𝐷 = 𝐻 & ⊢ 𝐺 = 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | ecovass 8832* | Lemma used to transfer an associative law via an equivalence relation. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐺, 𝐻⟩] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑁, 𝑄⟩] ∼ ) & ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝐺, 𝐻⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝐽, 𝐾⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑁, 𝑄⟩] ∼ ) = [⟨𝐿, 𝑀⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) & ⊢ 𝐽 = 𝐿 & ⊢ 𝐾 = 𝑀 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | ecovdi 8833* | Lemma used to transfer a distributive law via an equivalence relation. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.) |
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ ) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ ) & ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ ) & ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆)) & ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) & ⊢ 𝐻 = 𝐾 & ⊢ 𝐽 = 𝐿 ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Syntax | cmap 8834 | Extend the definition of a class to include the mapping operation. (Read for 𝐴 ↑m 𝐵, "the set of all functions that map from 𝐵 to 𝐴.) |
class ↑m | ||
Syntax | cpm 8835 | 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 8836* | Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑m 𝐵) (see mapval 8846). 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 (𝐴 ↑m 𝐵). 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.) |
⊢ ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥}) | ||
Definition | df-pm 8837* | 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 8845). 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 ↑m (df-map 8836). See mapsspm 8884 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.) |
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) | ||
Theorem | mapprc 8838* | 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 8839* | The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ (Fun 𝑓 ∧ 𝑓 ⊆ (𝐴 × 𝐵))} ∈ V) | ||
Theorem | mapex 8840* | 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 8841 | Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ↑m Fn (V × V) | ||
Theorem | fnpm 8842 | Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ ↑pm Fn (V × V) | ||
Theorem | reldmmap 8843 | Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ Rel dom ↑m | ||
Theorem | mapvalg 8844* | The value of set exponentiation. (𝐴 ↑m 𝐵) 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.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑m 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴}) | ||
Theorem | pmvalg 8845* | 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 8846* | The value of set exponentiation (inference version). (𝐴 ↑m 𝐵) 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 ⇒ ⊢ (𝐴 ↑m 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴} | ||
Theorem | elmapg 8847 | Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | ||
Theorem | elmapd 8848 | Deduction form of elmapg 8847. (Contributed by BJ, 11-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | ||
Theorem | elmapdd 8849 | Deduction associated with elmapd 8848. (Contributed by SN, 29-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶:𝐵⟶𝐴) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑m 𝐵)) | ||
Theorem | mapdm0 8850 | 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.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ↑m ∅) = {∅}) | ||
Theorem | elpmg 8851 | The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐶 ∧ 𝐶 ⊆ (𝐵 × 𝐴)))) | ||
Theorem | elpm2g 8852 | The predicate "is a partial function". (Contributed by NM, 31-Dec-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) | ||
Theorem | elpm2r 8853 | Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) | ||
Theorem | elpmi 8854 | A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) | ||
Theorem | pmfun 8855 | A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → Fun 𝐹) | ||
Theorem | elmapex 8856 | Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V)) | ||
Theorem | elmapi 8857 | A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵) | ||
Theorem | mapfset 8858* | If 𝐵 is a set, the value of the set exponentiation (𝐵 ↑m 𝐴) is the class of all functions from 𝐴 to 𝐵. Generalisation of mapvalg 8844 (which does not require ax-rep 5279) to arbitrary domains. Note that the class {𝑓 ∣ 𝑓:𝐴⟶𝐵} can only contain set-functions, as opposed to arbitrary class-functions. When 𝐴 is a proper class, there can be no set-functions on it, so the above class is empty (see also fsetdmprc0 8863), hence a set. In this case, both sides of the equality in this theorem are the empty set. (Contributed by AV, 8-Aug-2024.) |
⊢ (𝐵 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = (𝐵 ↑m 𝐴)) | ||
Theorem | mapssfset 8859* | The value of the set exponentiation (𝐵 ↑m 𝐴) is a subset of the class of functions from 𝐴 to 𝐵. (Contributed by AV, 10-Aug-2024.) |
⊢ (𝐵 ↑m 𝐴) ⊆ {𝑓 ∣ 𝑓:𝐴⟶𝐵} | ||
Theorem | mapfoss 8860* | The value of the set exponentiation (𝐵 ↑m 𝐴) is a superset of the set of all functions from 𝐴 onto 𝐵. (Contributed by AV, 7-Aug-2024.) |
⊢ {𝑓 ∣ 𝑓:𝐴–onto→𝐵} ⊆ (𝐵 ↑m 𝐴) | ||
Theorem | fsetsspwxp 8861* | The class of all functions from 𝐴 into 𝐵 is a subclass of the power class of the cartesion product of 𝐴 and 𝐵. (Contributed by AV, 13-Sep-2024.) |
⊢ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ⊆ 𝒫 (𝐴 × 𝐵) | ||
Theorem | fset0 8862 | The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.) |
⊢ {𝑓 ∣ 𝑓:∅⟶𝐵} = {∅} | ||
Theorem | fsetdmprc0 8863* | The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.) |
⊢ (𝐴 ∉ V → {𝑓 ∣ 𝑓 Fn 𝐴} = ∅) | ||
Theorem | fsetex 8864* | The set of functions between two classes exists if the codomain exists. Generalization of mapex 8840 to arbitrary domains. (Contributed by AV, 14-Aug-2024.) |
⊢ (𝐵 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) | ||
Theorem | f1setex 8865* | The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024.) |
⊢ (𝐵 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ∈ V) | ||
Theorem | fosetex 8866* | The set of surjections between two classes exists (without any precondition). (Contributed by AV, 8-Aug-2024.) |
⊢ {𝑓 ∣ 𝑓:𝐴–onto→𝐵} ∈ V | ||
Theorem | f1osetex 8867* | The set of bijections between two classes exists. (Contributed by AV, 30-Mar-2024.) (Revised by AV, 8-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
⊢ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐵} ∈ V | ||
Theorem | fsetfcdm 8868* | The class of functions with a given domain and a given codomain is mapped, through evaluation at a point of the domain, into the codomain. (Contributed by AV, 15-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ 𝑓:𝐴⟶𝐵} & ⊢ 𝑆 = (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋)) ⇒ ⊢ (𝑋 ∈ 𝐴 → 𝑆:𝐹⟶𝐵) | ||
Theorem | fsetfocdm 8869* | The class of functions with a given domain that is a set and a given codomain is mapped, through evaluation at a point of the domain, onto the codomain. (Contributed by AV, 15-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ 𝑓:𝐴⟶𝐵} & ⊢ 𝑆 = (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑆:𝐹–onto→𝐵) | ||
Theorem | fsetprcnex 8870* | The class of all functions from a nonempty set 𝐴 into a proper class 𝐵 is not a set. If one of the preconditions is not fufilled, then {𝑓 ∣ 𝑓:𝐴⟶𝐵} is a set, see fsetdmprc0 8863 for 𝐴 ∉ V, fset0 8862 for 𝐴 = ∅, and fsetex 8864 for 𝐵 ∈ V, see also fsetexb 8872. (Contributed by AV, 14-Sep-2024.) (Proof shortened by BJ, 15-Sep-2024.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) | ||
Theorem | fsetcdmex 8871* | The class of all functions from a nonempty set 𝐴 into a class 𝐵 is a set iff 𝐵 is a set . (Contributed by AV, 15-Sep-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → (𝐵 ∈ V ↔ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V)) | ||
Theorem | fsetexb 8872* | The class of all functions from a class 𝐴 into a class 𝐵 is a set iff 𝐵 is a set or 𝐴 is not a set or 𝐴 is empty. (Contributed by AV, 15-Sep-2024.) |
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V ↔ (𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V)) | ||
Theorem | elmapfn 8873 | A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶) | ||
Theorem | elmapfun 8874 | A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → Fun 𝐴) | ||
Theorem | elmapssres 8875 | A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷)) | ||
Theorem | fpmg 8876 | A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | pmss12g 8877 | Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷)) | ||
Theorem | pmresg 8878 | Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) | ||
Theorem | elmap 8879 | Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴) | ||
Theorem | mapval2 8880* | Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵}) | ||
Theorem | elpm 8881 | The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (𝐵 × 𝐴))) | ||
Theorem | elpm2 8882 | The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) | ||
Theorem | fpm 8883 | A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | mapsspm 8884 | Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝐴 ↑m 𝐵) ⊆ (𝐴 ↑pm 𝐵) | ||
Theorem | pmsspw 8885 | Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ↑pm 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) | ||
Theorem | mapsspw 8886 | Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ↑m 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) | ||
Theorem | mapfvd 8887 | The value of a function that maps from 𝐵 to 𝐴. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝑀 = (𝐴 ↑m 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | elmapresaun 8888 | fresaun 6762 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵))) | ||
Theorem | fvmptmap 8889* | Special case of fvmpt 6999 for operator theorems. (Contributed by NM, 27-Nov-2007.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑅 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑m 𝐷) ↦ 𝐵) ⇒ ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | map0e 8890 | Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 14-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑m ∅) = 1o) | ||
Theorem | map0b 8891 | Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≠ ∅ → (∅ ↑m 𝐴) = ∅) | ||
Theorem | map0g 8892 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅))) | ||
Theorem | 0map0sn0 8893 | The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024.) |
⊢ (∅ ↑m ∅) = {∅} | ||
Theorem | mapsnd 8894* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}) | ||
Theorem | map0 8895 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅)) | ||
Theorem | mapsn 8896* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}} | ||
Theorem | mapss 8897 | Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) | ||
Theorem | fdiagfn 8898* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) | ||
Theorem | fvdiagfn 8899* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋})) | ||
Theorem | mapsnconst 8900 | Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐵 ↑m 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |