HomeTheorem List (p. 319 of 476)
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. 319 of 476) | < 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-30098) |
Hilbert Space Explorer
(30099-31621) |
Users' Mathboxes
(31622-47564) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fimarab 31801* | Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝐹 “ 𝑋) = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑦}) | ||
| Theorem | unipreima 31802* | Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
| ⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
| Theorem | opfv 31803 | Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
| ⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = ⟨((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)⟩) | ||
| Theorem | xppreima 31804 | 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 31805 | Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵) | ||
| Theorem | djussxp2 31806* | Stronger version of djussxp 5838. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) | ||
| Theorem | 2ndresdju 31807* | The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴) | ||
| Theorem | 2ndresdjuf1o 31808* | The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 8071. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
| ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴) | ||
| Theorem | xppreima2 31809* | 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 31810* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓)) | ||
| Theorem | rabfmpunirn 31811* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑}) & ⊢ 𝑊 ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓)) | ||
| Theorem | abfmpeld 31812* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓}) & ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V) & ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒))) | ||
| Theorem | abfmpel 31813* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓)) | ||
| Theorem | fmptdF 31814 | Domain and codomain of the mapping operation; deduction form. This version of fmptd 7099 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
| Theorem | fmptcof2 31815* | 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 31816* | Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 7116. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) | ||
| Theorem | acunirnmpt 31817* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) | ||
| Theorem | acunirnmpt2 31818* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
| Theorem | acunirnmpt2f 31819* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑗𝐶 & ⊢ Ⅎ𝑗𝐷 & ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵 & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
| Theorem | aciunf1lem 31820* | Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)) | ||
| Theorem | aciunf1 31821* | Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) | ||
| Theorem | ofoprabco 31822* | Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
| ⊢ Ⅎ𝑎𝑀 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩)) & ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀)) | ||
| Theorem | ofpreima 31823* | 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 31824* | Express the preimage of a function operation as a union of preimages. This version of ofpreima 31823 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
| Theorem | funcnvmpt 31825* | Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) | ||
| Theorem | funcnv5mpt 31826* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶))) | ||
| Theorem | funcnv4mpt 31827* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) | ||
| Theorem | preimane 31828 | Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.) |
| ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐹) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌})) | ||
| Theorem | fnpreimac 31829* | Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) | ||
| Theorem | fgreu 31830* | 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 31831* | 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 31832* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷) | ||
| Theorem | mptssALT 31833* | Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 6033. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | dfcnv2 31834* | Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.) |
| ⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥}))) | ||
| Theorem | fnimatp 31835 | The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 “ {𝐴, 𝐵, 𝐶}) = {(𝐹‘𝐴), (𝐹‘𝐵), (𝐹‘𝐶)}) | ||
| Theorem | fnunres2 31836 | Restriction of a disjoint union to the domain of the second function. (Contributed by Thierry Arnoux, 12-Oct-2023.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺) | ||
| Theorem | rnexd 31837 | The range of a set is a set. Deduction version of rnexd 31837. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran 𝐴 ∈ V) | ||
| Theorem | imaexd 31838 | The image of a set is a set. Deduction version of imaexg 7890. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) ∈ V) | ||
| Theorem | mpomptxf 31839* | 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 | suppovss 31840* | A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) | ||
| Theorem | fvdifsupp 31841 | Function value is zero outside of its support. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∖ (𝐹 supp 𝑍))) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) = 𝑍) | ||
| Theorem | fmptssfisupp 31842* | The restriction of a mapping function has finite support if that function has finite support. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) finSupp 𝑍) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) finSupp 𝑍) | ||
| Theorem | suppiniseg 31843 | Relation between the support (𝐹 supp 𝑍) and the initial segment (◡𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍})) | ||
| Theorem | fsuppinisegfi 31844 | 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 31845 | The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍}))) | ||
| Theorem | fdifsuppconst 31846 | A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
| ⊢ 𝐴 = (dom 𝐹 ∖ (𝐹 supp 𝑍)) ⇒ ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ 𝐴) = (𝐴 × {𝑍})) | ||
| Theorem | ressupprn 31847 | 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 31848 | 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 31849 | Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024.) |
| ⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin) | ||
| Theorem | mptiffisupp 31850* | 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 31851 | Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐷⟩}) = ∅) | ||
| Theorem | cosnop 31852 | Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐴⟩}) = {⟨𝐶, 𝐵⟩}) | ||
| Theorem | cnvprop 31853 | Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {⟨𝐵, 𝐴⟩, ⟨𝐷, 𝐶⟩}) | ||
| Theorem | brprop 31854 | Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷)))) | ||
| Theorem | mptprop 31855* | Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) | ||
| Theorem | coprprop 31856 | Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) ⇒ ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩}) | ||
| Theorem | gtiso 31857 | Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
| ⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) | ||
| Theorem | isoun 31858* | Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017.) |
| ⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷) → 𝑧𝑆𝑤) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑧𝑆𝑤) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅) ⇒ ⊢ (𝜑 → (𝐻 ∪ 𝐺) Isom 𝑅, 𝑆 ((𝐴 ∪ 𝐶), (𝐵 ∪ 𝐷))) | ||
| Theorem | disjdsct 31859* | 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 6607) (Contributed by Thierry Arnoux, 28-Feb-2017.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅})) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
| Theorem | df1stres 31860* | Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥) | ||
| Theorem | df2ndres 31861* | Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦) | ||
| Theorem | 1stpreimas 31862 | The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
| ⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋}))) | ||
| Theorem | 1stpreima 31863 | The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
| ⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) | ||
| Theorem | 2ndpreima 31864 | The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
| ⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴)) | ||
| Theorem | curry2ima 31865* | The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)}) | ||
| Theorem | preiman0 31866 | The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ 𝐴) ≠ ∅) | ||
| Theorem | intimafv 31867* | The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024.) |
| ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ∩ (𝐹 “ 𝐴) = ∩ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
| Theorem | ecref 31868 | All elements are in their own equivalence class. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
| ⊢ ((𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴]𝑅) | ||
| Theorem | supssd 31869* | Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅)) | ||
| Theorem | infssd 31870* | Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ¬ inf(𝐶, 𝐴, 𝑅)𝑅inf(𝐵, 𝐴, 𝑅)) | ||
| Theorem | imafi2 31871 | The image by a finite set is finite. See also imafi 9160. (Contributed by Thierry Arnoux, 25-Apr-2020.) |
| ⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin) | ||
| Theorem | unifi3 31872 | If a union is finite, then all its elements are finite. See unifi 9326. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
| ⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin) | ||
| Theorem | snct 31873 | A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω) | ||
| Theorem | prct 31874 | An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω) | ||
| Theorem | mpocti 31875* | An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
| ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ⇒ ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
| Theorem | abrexct 31876* | An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
| ⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | ||
| Theorem | mptctf 31877 | A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω) | ||
| Theorem | abrexctf 31878* | 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 31879* | Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.) |
| ⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) | ||
| Theorem | cnvoprabOLD 31880* | The converse of a class abstraction of nested ordered pairs. Obsolete version of cnvoprab 8030 as of 16-Oct-2022, which has nonfreeness hypotheses instead of disjoint variable conditions. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜑)) & ⊢ (𝜓 → 𝑎 ∈ (V × V)) ⇒ ⊢ ◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑧, 𝑎⟩ ∣ 𝜓} | ||
| Theorem | f1od2 31881* | 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 31882* | 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 31883* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9387. (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 | suppss3 31884* | 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 31885* | Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
| ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
| Theorem | fsuppcurry2 31886* | Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
| ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
| Theorem | offinsupp1 31887* | Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐹 finSupp 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑌𝑅𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) finSupp 𝑍) | ||
| Theorem | ffs2 31888 | Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq 8144. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
| ⊢ 𝐶 = (𝐵 ∖ {𝑍}) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 supp 𝑍) = (◡𝐹 “ 𝐶)) | ||
| Theorem | ffsrn 31889 | The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
| ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ Fin) | ||
| Theorem | resf1o 31890* | Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
| ⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶} & ⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶)) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑m 𝐶)) | ||
| Theorem | maprnin 31891* | Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ∩ 𝐶) ↑m 𝐴) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ran 𝑓 ⊆ 𝐶} | ||
| Theorem | fpwrelmapffslem 31892* | Lemma for fpwrelmapffs 31894. For this theorem, the sets 𝐴 and 𝐵 could be infinite, but the relation 𝑅 itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵) & ⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) ⇒ ⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin))) | ||
| Theorem | fpwrelmap 31893* | Define a canonical mapping between functions from 𝐴 into subsets of 𝐵 and the relations with domain 𝐴 and range within 𝐵. Note that the same relation is used in axdc2lem 10427 and marypha2lem1 9414. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ⇒ ⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵) | ||
| Theorem | fpwrelmapffs 31894* | Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) & ⊢ 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin} ⇒ ⊢ (𝑀 ↾ 𝑆):𝑆–1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin) | ||
| Theorem | creq0 31895 | The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 12189. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ (𝐴 + (i · 𝐵)) = 0)) | ||
| Theorem | 1nei 31896 | The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
| ⊢ 1 ≠ i | ||
| Theorem | 1neg1t1neg1 31897 | An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ (𝑁 ∈ {-1, 1} → (𝑁 · 𝑁) = 1) | ||
| Theorem | nnmulge 31898 | Multiplying by a positive integer 𝑀 yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
| ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (𝑀 · 𝑁)) | ||
| Theorem | lt2addrd 31899* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) | ||
| Theorem | xrlelttric 31900 | Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |