HomeTheorem List (p. 333 of 510)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 333 of 510) | < 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: | Metamath Proof Explorer
(1-31502) |
Hilbert Space Explorer
(31503-33025) |
Users' Mathboxes
(33026-50934) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fresunsn 33201 | Recover the original function from a point-added function. See also funresdfunsn 7186 and fsnunres 7185. (Contributed by Thierry Arnoux, 15-Feb-2026.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ (𝐹‘𝑋) = 𝑌) → ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, 𝑌⟩}) = 𝐹) | ||
| Theorem | f1o3d 33202* | Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
| Theorem | eldmne0 33203 | A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ (𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅) | ||
| Theorem | f1rnen 33204 | Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉) → ran 𝐹 ≈ 𝐴) | ||
| Theorem | f1oeq3dd 33205 | Equality deduction for one-to-one onto functions. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) | ||
| Theorem | rinvf1o 33206 | Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
| ⊢ Fun 𝐹 & ⊢ ◡𝐹 = 𝐹 & ⊢ (𝐹 “ 𝐴) ⊆ 𝐵 & ⊢ (𝐹 “ 𝐵) ⊆ 𝐴 & ⊢ 𝐴 ⊆ dom 𝐹 & ⊢ 𝐵 ⊆ dom 𝐹 ⇒ ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→𝐵 | ||
| Theorem | fresf1o 33207 | Conditions for a restriction to be a one-to-one onto function. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
| ⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun (◡𝐹 ↾ 𝐶)) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–1-1-onto→𝐶) | ||
| Theorem | nfpconfp 33208 | The set of fixed points of 𝐹 is the complement of the set of points moved by 𝐹. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
| ⊢ (𝐹 Fn 𝐴 → (𝐴 ∖ dom (𝐹 ∖ I )) = dom (𝐹 ∩ I )) | ||
| Theorem | fmptco1f1o 33209* | The action of composing (to the right) with a bijection is itself a bijection of functions. (Contributed by Thierry Arnoux, 3-Jan-2021.) |
| ⊢ 𝐴 = (𝑅 ↑m 𝐸) & ⊢ 𝐵 = (𝑅 ↑m 𝐷) & ⊢ 𝐹 = (𝑓 ∈ 𝐴 ↦ (𝑓 ∘ 𝑇)) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑇:𝐷–1-1-onto→𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | cofmpt2 33210* | Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023.) |
| ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝐶) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝐷)) | ||
| Theorem | f1mptrn 33211* | Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃!𝑥 ∈ 𝐴 𝑦 = 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
| Theorem | dfimafnf 33212* | Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) | ||
| Theorem | funimass4f 33213 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
| Theorem | suppss2f 33214* | Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017.) (Revised by AV, 1-Sep-2020.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝑊 & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊) | ||
| Theorem | ofrn 33215 | The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ 𝐶) | ||
| Theorem | ofrn2 33216 | The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) | ||
| Theorem | off2 33217* | The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
| Theorem | ofresid 33218 | Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f (𝑅 ↾ (𝐵 × 𝐵))𝐺)) | ||
| Theorem | unipreima 33219* | Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
| Theorem | opfv 33220 | Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
| ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = ⟨((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)⟩) | ||
| Theorem | xppreima 33221 | The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
| ⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (◡𝐹 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍))) | ||
| Theorem | 2ndimaxp 33222 | Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵) | ||
| Theorem | dmdju 33223* | Domain of a disjoint union of non-empty sets. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → dom ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = 𝐴) | ||
| Theorem | djussxp2 33224* | Stronger version of djussxp 5823. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) | ||
| Theorem | 2ndresdju 33225* | The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴) | ||
| Theorem | 2ndresdjuf1o 33226* | The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 8101. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴) | ||
| Theorem | xppreima2 33227* | The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩) ⇒ ⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) | ||
| Theorem | abfmpunirn 33228* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓)) | ||
| Theorem | rabfmpunirn 33229* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑}) & ⊢ 𝑊 ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓)) | ||
| Theorem | abfmpeld 33230* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓}) & ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V) & ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒))) | ||
| Theorem | abfmpel 33231* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓)) | ||
| Theorem | fmptdf2 33232 | Domain and codomain of the mapping operation; deduction form. This version of fmptd 7106 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
| Theorem | fmptcof2 33233* | Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) (Revised by Thierry Arnoux, 10-May-2017.) |
| ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑇 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) | ||
| Theorem | fcomptf 33234* | Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 7126. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) | ||
| Theorem | acunirnmpt 33235* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) | ||
| Theorem | acunirnmpt2 33236* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
| Theorem | acunirnmpt2f 33237* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑗𝐶 & ⊢ Ⅎ𝑗𝐷 & ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵 & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
| Theorem | aciunf1lem 33238* | Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)) | ||
| Theorem | aciunf1 33239* | Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) | ||
| Theorem | ofoprabco 33240* | Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
| ⊢ Ⅎ𝑎𝑀 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩)) & ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀)) | ||
| Theorem | ofpreima 33241* | Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
| Theorem | ofpreima2 33242* | Express the preimage of a function operation as a union of preimages. This version of ofpreima 33241 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
| Theorem | funcnv5mpt 33243* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶))) | ||
| Theorem | funcnv4mpt 33244* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) | ||
| Theorem | preimane 33245 | Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.) |
| ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐹) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌})) | ||
| Theorem | fnpreimac 33246* | Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) | ||
| Theorem | fgreu 33247* | Exactly one point of a function's graph has a given first element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∃!𝑝 ∈ 𝐹 𝑋 = (1st ‘𝑝)) | ||
| Theorem | fcnvgreu 33248* | If the converse of a relation 𝐴 is a function, exactly one point of its graph has a given second element (that is, function value). (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ (((Rel 𝐴 ∧ Fun ◡𝐴) ∧ 𝑌 ∈ ran 𝐴) → ∃!𝑝 ∈ 𝐴 𝑌 = (2nd ‘𝑝)) | ||
| Theorem | rnmposs 33249* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷) | ||
| Theorem | mptssALT 33250* | Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 6036. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | dfcnv2 33251* | Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.) |
| ⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥}))) | ||
| Theorem | partfun2 33252* | Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. See also partfun 6678 and ifmpt2v 7514. (Contributed by Thierry Arnoux, 25-Jan-2026.) |
| ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ if(𝜑, 𝐵, 𝐶)) = ((𝑥 ∈ 𝐷 ↦ 𝐵) ∪ (𝑥 ∈ (𝐴 ∖ 𝐷) ↦ 𝐶)) | ||
| Theorem | rnressnsn 33253 | The range of a restriction to a singleton is a singleton. See dmressnsn 6014. (Contributed by Thierry Arnoux, 25-Jan-2026.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ran (𝐹 ↾ {𝐴}) = {(𝐹‘𝐴)}) | ||
| Theorem | mpomptxf 33254* | Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Thierry Arnoux, 31-Mar-2018.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
| Theorem | of0r 33255 | Function operation with the empty function. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ (𝐹 ∘f 𝑅∅) = ∅ | ||
| Theorem | suppovss 33256* | A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) | ||
| Theorem | elsuppfnd 33257 | Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → (𝐹‘𝑋) ≠ 𝑍) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐹 supp 𝑍)) | ||
| Theorem | fisuppov1 33258* | Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐸) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ( 0 𝑂𝑦) = 𝑍) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ ((𝐹‘𝑥)𝑂𝐵)) finSupp 𝑍) | ||
| Theorem | suppun2 33259 | The support of a union is the union of the supports. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) = ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍))) | ||
| Theorem | fdifsupp 33260 | Express the support of a function 𝐹 outside of 𝐵 in two different ways. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) = ((𝐹 supp 𝑍) ∖ 𝐵)) | ||
| Theorem | suppiniseg 33261 | Relation between the support (𝐹 supp 𝑍) and the initial segment (◡𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍})) | ||
| Theorem | fsuppinisegfi 33262 | The initial segment (◡𝐹 “ {𝑌}) of a nonzero 𝑌 is finite if 𝐹 has finite support. (Contributed by Thierry Arnoux, 21-Jun-2024.) |
| ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ (V ∖ { 0 })) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑌}) ∈ Fin) | ||
| Theorem | fressupp 33263 | The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍}))) | ||
| Theorem | fdifsuppconst 33264 | A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
| ⊢ 𝐴 = (dom 𝐹 ∖ (𝐹 supp 𝑍)) ⇒ ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ 𝐴) = (𝐴 × {𝑍})) | ||
| Theorem | ressupprn 33265 | The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) | ||
| Theorem | supppreima 33266 | Express the support of a function as the preimage of its range except zero. (Contributed by Thierry Arnoux, 24-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (ran 𝐹 ∖ {𝑍}))) | ||
| Theorem | fsupprnfi 33267 | Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024.) |
| ⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin) | ||
| Theorem | mptiffisupp 33268* | Conditions for a mapping function defined with a conditional to have finite support. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝑍)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
| Theorem | cosnopne 33269 | Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐷⟩}) = ∅) | ||
| Theorem | cosnop 33270 | Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐴⟩}) = {⟨𝐶, 𝐵⟩}) | ||
| Theorem | cnvprop 33271 | Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {⟨𝐵, 𝐴⟩, ⟨𝐷, 𝐶⟩}) | ||
| Theorem | brprop 33272 | Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷)))) | ||
| Theorem | mptprop 33273* | Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) | ||
| Theorem | coprprop 33274 | Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) ⇒ ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩}) | ||
| Theorem | fmptunsnop 33275* | Two ways to express a function with a value replaced. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 = 𝑋, 𝑌, (𝐹‘𝑥))) = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, 𝑌⟩})) | ||
| Theorem | gtiso 33276 | Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) | ||
| Theorem | isoun 33277* | Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017.) |
| ⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷) → 𝑧𝑆𝑤) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑧𝑆𝑤) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅) ⇒ ⊢ (𝜑 → (𝐻 ∪ 𝐺) Isom 𝑅, 𝑆 ((𝐴 ∪ 𝐶), (𝐵 ∪ 𝐷))) | ||
| Theorem | disjdsct 33278* | A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv 6601) (Contributed by Thierry Arnoux, 28-Feb-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅})) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
| Theorem | df1stres 33279* | Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥) | ||
| Theorem | df2ndres 33280* | Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦) | ||
| Theorem | 1stpreimas 33281 | The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
| ⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋}))) | ||
| Theorem | 1stpreima 33282 | The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
| ⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) | ||
| Theorem | 2ndpreima 33283 | The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
| ⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴)) | ||
| Theorem | curry2ima 33284* | The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)}) | ||
| Theorem | preiman0 33285 | The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ 𝐴) ≠ ∅) | ||
| Theorem | intimafv 33286* | The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ∩ (𝐹 “ 𝐴) = ∩ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
| Theorem | snct 33287 | A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω) | ||
| Theorem | prct 33288 | An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω) | ||
| Theorem | mpocti 33289* | An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
| ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ⇒ ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
| Theorem | mptctf 33290 | A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω) | ||
| Theorem | abrexctf 33291* | An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | ||
| Theorem | padct 33292* | Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.) Avoid ax-rep 5232. (Revised by GG, 2-Apr-2026.) |
| ⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) | ||
| Theorem | f1od2 33293* | Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌)) & ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))) ⇒ ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷) | ||
| Theorem | fcobij 33294* | Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017.) |
| ⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑓 ∈ (𝑆 ↑m 𝑅) ↦ (𝐺 ∘ 𝑓)):(𝑆 ↑m 𝑅)–1-1-onto→(𝑇 ↑m 𝑅)) | ||
| Theorem | fcobijfs 33295* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9384. (Contributed by Thierry Arnoux, 25-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
| ⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝑂 ∈ 𝑆) & ⊢ 𝑄 = (𝐺‘𝑂) & ⊢ 𝑋 = {𝑔 ∈ (𝑆 ↑m 𝑅) ∣ 𝑔 finSupp 𝑂} & ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑m 𝑅) ∣ ℎ finSupp 𝑄} ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝐺 ∘ 𝑓)):𝑋–1-1-onto→𝑌) | ||
| Theorem | fcobijfs2 33296* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also fcobijfs 33295 and mapfien 9384. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐺:𝑅–1-1-onto→𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝑂 ∈ 𝑇) & ⊢ 𝑋 = {𝑔 ∈ (𝑇 ↑m 𝑆) ∣ 𝑔 finSupp 𝑂} & ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑m 𝑅) ∣ ℎ finSupp 𝑂} ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝑓 ∘ 𝐺)):𝑋–1-1-onto→𝑌) | ||
| Theorem | suppss3 33297* | Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
| ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑍) → 𝐵 = 𝑍) ⇒ ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
| Theorem | fsuppcurry1 33298* | Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
| ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
| Theorem | fsuppcurry2 33299* | Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
| ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
| Theorem | offinsupp1 33300* | Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐹 finSupp 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑌𝑅𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) finSupp 𝑍) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |