![]() |
Metamath
Proof Explorer Theorem List (p. 75 of 431) | < 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-28080) |
![]() (28081-29605) |
![]() (29606-43060) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fmpt2 7401* | Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) | ||
Theorem | fnmpt2 7402* | Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn (𝐴 × 𝐵)) | ||
Theorem | fnmpt2i 7403* | Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ 𝐹 Fn (𝐴 × 𝐵) | ||
Theorem | dmmpt2 7404* | Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐶 ∈ V ⇒ ⊢ dom 𝐹 = (𝐴 × 𝐵) | ||
Theorem | ovmpt2elrn 7405* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) ∈ 𝑀) | ||
Theorem | dmmpt2ga 7406* | Domain of an operation given by the "maps to" notation, closed form of dmmpt2 7404. (Contributed by Alexander van der Vekens, 10-Feb-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵)) | ||
Theorem | dmmpt2g 7407* | Domain of an operation given by the "maps to" notation, closed form of dmmpt2 7404. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵)) | ||
Theorem | mpt2exxg 7408* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | mpt2exg 7409* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 𝐹 ∈ V) | ||
Theorem | mpt2exga 7410* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by NM, 12-Sep-2011.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) | ||
Theorem | mpt2ex 7411* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V | ||
Theorem | mptmpt2opabbrd 7412* | The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) & ⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ 𝜓} ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓) & ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃)) & ⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏)) & ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)})) ⇒ ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)}) | ||
Theorem | mptmpt2opabovd 7413* | The operation value of a function value of a collection of ordered pairs of related elements (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺)) & ⊢ (𝜑 → {〈𝑓, ℎ〉 ∣ 𝜓} ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓) & ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {〈𝑓, ℎ〉 ∣ (𝑓(𝑎(𝐶‘𝑔)𝑏)ℎ ∧ 𝑓(𝐷‘𝑔)ℎ)})) ⇒ ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {〈𝑓, ℎ〉 ∣ (𝑓(𝑋(𝐶‘𝐺)𝑌)ℎ ∧ 𝑓(𝐷‘𝐺)ℎ)}) | ||
Theorem | el2mpt2csbcl 7414* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐸)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ ⦋𝑋 / 𝑥⦌⦋𝑌 / 𝑦⦌𝐶 ∧ 𝑇 ∈ ⦋𝑋 / 𝑥⦌⦋𝑌 / 𝑦⦌𝐷)))) | ||
Theorem | el2mpt2cl 7415* | If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. Using implicit substitution. (Contributed by AV, 21-May-2021.) |
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐸)) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝐶 = 𝐹 ∧ 𝐷 = 𝐺)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺)))) | ||
Theorem | fnmpt2ovd 7416* | A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) |
⊢ (𝜑 → 𝑀 Fn (𝐴 × 𝐵)) & ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) → 𝐷 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐵 (𝑖𝑀𝑗) = 𝐷)) | ||
Theorem | offval22 7417* | The function operation expressed as a mapping, variation of offval2 7075. (Contributed by SO, 15-Jul-2018.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷))) | ||
Theorem | brovpreldm 7418 | If a binary relation holds for the result of an operation, the operands are in the domain of the operation. (Contributed by AV, 31-Dec-2020.) |
⊢ (𝐷(𝐵𝐴𝐶)𝐸 → 〈𝐵, 𝐶〉 ∈ dom 𝐴) | ||
Theorem | bropopvvv 7419* | If a binary relation holds for the result of an operation which is a result of an operation, the involved classes are sets. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Proof shortened by AV, 3-Jan-2021.) |
⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ 𝜑})) & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓)) & ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ 𝜃}) ⇒ ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) | ||
Theorem | bropfvvvvlem 7420* | Lemma for bropfvvvv 7421. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑})) & ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) ⇒ ⊢ ((〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))) | ||
Theorem | bropfvvvv 7421* | If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑})) & ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) & ⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆) & ⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇) & ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) | ||
Theorem | ovmptss 7422* | If all the values of the mapping are subsets of a class 𝑋, then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → (𝐸𝐹𝐺) ⊆ 𝑋) | ||
Theorem | relmpt2opab 7423* | Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈𝑧, 𝑤〉 ∣ 𝜑}) ⇒ ⊢ Rel (𝐶𝐹𝐷) | ||
Theorem | fmpt2co 7424* | Composition of two functions. Variation of fmptco 6555 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) & ⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | ||
Theorem | oprabco 7425* | Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐷) & ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐻‘𝐶)) ⇒ ⊢ (𝐻 Fn 𝐷 → 𝐺 = (𝐻 ∘ 𝐹)) | ||
Theorem | oprab2co 7426* | Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑅) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈𝐶, 𝐷〉) & ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑀𝐷)) ⇒ ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹)) | ||
Theorem | df1st2 7427* | An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} = (1st ↾ (V × V)) | ||
Theorem | df2nd2 7428* | An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} = (2nd ↾ (V × V)) | ||
Theorem | 1stconst 7429 | The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐵 ∈ 𝑉 → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–1-1-onto→𝐴) | ||
Theorem | 2ndconst 7430 | The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.) |
⊢ (𝐴 ∈ 𝑉 → (2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–1-1-onto→𝐵) | ||
Theorem | dfmpt2 7431* | Alternate definition for the "maps to" notation df-mpt2 6814 (although it requires that 𝐶 be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 {〈〈𝑥, 𝑦〉, 𝐶〉} | ||
Theorem | mpt2sn 7432* | An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019.) |
⊢ 𝐹 = (𝑥 ∈ {𝐴}, 𝑦 ∈ {𝐵} ↦ 𝐶) & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑦 = 𝐵 → 𝐷 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈) → 𝐹 = {〈〈𝐴, 𝐵〉, 𝐸〉}) | ||
Theorem | curry1 7433* | Composition with ◡(2nd ↾ ({𝐶} × V)) turns any binary operation 𝐹 with a constant first operand into a function 𝐺 of the second operand only. This transformation is called "currying." (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥))) | ||
Theorem | curry1val 7434 | The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (𝐺‘𝐷) = (𝐶𝐹𝐷)) | ||
Theorem | curry1f 7435 | Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V))) ⇒ ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐴) → 𝐺:𝐵⟶𝐷) | ||
Theorem | curry2 7436* | Composition with ◡(1st ↾ (V × {𝐶})) turns any binary operation 𝐹 with a constant second operand into a function 𝐺 of the first operand only. This transformation is called "currying." (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶))) | ||
Theorem | curry2f 7437 | Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐵) → 𝐺:𝐴⟶𝐷) | ||
Theorem | curry2val 7438 | The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝐺‘𝐷) = (𝐷𝐹𝐶)) | ||
Theorem | cnvf1olem 7439 | Lemma for cnvf1o 7440. (Contributed by Mario Carneiro, 27-Apr-2014.) |
⊢ ((Rel 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (𝐶 ∈ ◡𝐴 ∧ 𝐵 = ∪ ◡{𝐶})) | ||
Theorem | cnvf1o 7440* | Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.) |
⊢ (Rel 𝐴 → (𝑥 ∈ 𝐴 ↦ ∪ ◡{𝑥}):𝐴–1-1-onto→◡𝐴) | ||
Theorem | fparlem1 7441 | Lemma for fpar 7445. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (◡(1st ↾ (V × V)) “ {𝑥}) = ({𝑥} × V) | ||
Theorem | fparlem2 7442 | Lemma for fpar 7445. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦}) | ||
Theorem | fparlem3 7443* | Lemma for fpar 7445. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) = ∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V))) | ||
Theorem | fparlem4 7444* | Lemma for fpar 7445. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) | ||
Theorem | fpar 7445* | Merge two functions in parallel. Use as the second argument of a composition with a (2-place) operation to build compound operations such as 𝑧 = ((√‘𝑥) + (abs‘𝑦)). (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V))))) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉)) | ||
Theorem | fsplit 7446 | A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar 7445 in order to build compound functions such as 𝑦 = ((√‘𝑥) + (abs‘𝑥)). (Contributed by NM, 17-Sep-2007.) |
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ 〈𝑥, 𝑥〉) | ||
Theorem | f2ndf 7447 | The 2nd (second member of an ordered pair) function restricted to a function 𝐹 is a function of 𝐹 into the codomain of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶𝐵) | ||
Theorem | fo2ndf 7448 | The 2nd (second member of an ordered pair) function restricted to a function 𝐹 is a function of 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹–onto→ran 𝐹) | ||
Theorem | f1o2ndf1 7449 | The 2nd (second member of an ordered pair) function restricted to a one-to-one function 𝐹 is a one-to-one function of 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 → (2nd ↾ 𝐹):𝐹–1-1-onto→ran 𝐹) | ||
Theorem | algrflem 7450 | Lemma for algrf 15484 and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵(𝐹 ∘ 1st )𝐶) = (𝐹‘𝐵) | ||
Theorem | frxp 7451* | A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵)) | ||
Theorem | xporderlem 7452* | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ (〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))) | ||
Theorem | poxp 7453* | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵)) | ||
Theorem | soxp 7454* | A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵)) | ||
Theorem | wexp 7455* | A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑆 We 𝐵) → 𝑇 We (𝐴 × 𝐵)) | ||
Theorem | fnwelem 7456* | Lemma for fnwe 7457. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑆 We 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) & ⊢ 𝑄 = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))))} & ⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ 〈(𝐹‘𝑧), 𝑧〉) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | fnwe 7457* | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑆 We 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | fnse 7458* | Condition for the well-order in fnwe 7457 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 Se 𝐵) & ⊢ (𝜑 → (◡𝐹 “ 𝑤) ∈ V) ⇒ ⊢ (𝜑 → 𝑇 Se 𝐴) | ||
In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 7461) are based on the Axiom of Union (usage of dmexg 7258), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (◡𝑅 “ (V ∖ {𝑍})) (see suppimacnv 7470). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now). | ||
Syntax | csupp 7459 | Extend class definition to include the support of functions. |
class supp | ||
Definition | df-supp 7460* | Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects.". The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
⊢ supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}}) | ||
Theorem | suppval 7461* | The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋 “ {𝑖}) ≠ {𝑍}}) | ||
Theorem | supp0prc 7462 | The support of a class is empty if either the class or the "zero" is a proper class. . (Contributed by AV, 28-May-2019.) |
⊢ (¬ (𝑋 ∈ V ∧ 𝑍 ∈ V) → (𝑋 supp 𝑍) = ∅) | ||
Theorem | suppvalbr 7463* | The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑦 𝑥𝑅𝑦 ∧ ∃𝑦(𝑥𝑅𝑦 ↔ 𝑦 ≠ 𝑍))}) | ||
Theorem | supp0 7464 | The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑍 ∈ 𝑊 → (∅ supp 𝑍) = ∅) | ||
Theorem | suppval1 7465* | The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.) |
⊢ ((Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋‘𝑖) ≠ 𝑍}) | ||
Theorem | suppvalfn 7466* | The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by AV, 22-Apr-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑖 ∈ 𝑋 ∣ (𝐹‘𝑖) ≠ 𝑍}) | ||
Theorem | elsuppfn 7467 | An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍))) | ||
Theorem | cnvimadfsn 7468* | The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)} | ||
Theorem | suppimacnvss 7469 | The support of functions "defined" by inverse images is a subset of the support defined by df-supp 7460. (Contributed by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍)) | ||
Theorem | suppimacnv 7470 | Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍}))) | ||
Theorem | frnsuppeq 7471 | Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 supp 𝑍) = (◡𝐹 “ (𝑆 ∖ {𝑍})))) | ||
Theorem | suppssdm 7472 | The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.) |
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 | ||
Theorem | suppsnop 7473 | The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝑌〉} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋})) | ||
Theorem | snopsuppss 7474 | The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019.) |
⊢ ({〈𝑋, 𝑌〉} supp 𝑍) ⊆ {𝑋} | ||
Theorem | fvn0elsupp 7475 | If the function value for a given argument is not empty, the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 2-Jul-2019.) (Revised by AV, 4-Apr-2020.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ (𝐺 Fn 𝐵 ∧ (𝐺‘𝑋) ≠ ∅)) → 𝑋 ∈ (𝐺 supp ∅)) | ||
Theorem | fvn0elsuppb 7476 | The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵) → ((𝐺‘𝑋) ≠ ∅ ↔ 𝑋 ∈ (𝐺 supp ∅))) | ||
Theorem | rexsupp 7477* | Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∃𝑥 ∈ (𝐹 supp 𝑍)𝜑 ↔ ∃𝑥 ∈ 𝑋 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑))) | ||
Theorem | ressuppss 7478 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐹 ↾ 𝐵) supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | suppun 7479 | The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019.) |
⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) | ||
Theorem | ressuppssdif 7480 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) ⊆ (((𝐹 ↾ 𝐵) supp 𝑍) ∪ (dom 𝐹 ∖ 𝐵))) | ||
Theorem | mptsuppdifd 7481* | The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})}) | ||
Theorem | mptsuppd 7482* | The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍}) | ||
Theorem | extmptsuppeq 7483* | The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐵 ∖ 𝐴)) → 𝑋 = 𝑍) ⇒ ⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍)) | ||
Theorem | suppfnss 7484* | The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 6-Jun-2022.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) | ||
Theorem | suppfnssOLD 7485* | Obsolete proof of suppfnss 7484 as of 6-Jun-2022. (Contributed by AV, 30-Apr-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) | ||
Theorem | funsssuppss 7486 | The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.) |
⊢ ((Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) | ||
Theorem | fnsuppres 7487 | Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ (𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 supp 𝑍) ⊆ 𝐴 ↔ (𝐹 ↾ 𝐵) = (𝐵 × {𝑍}))) | ||
Theorem | fnsuppeq0 7488 | The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) → ((𝐹 supp 𝑍) = ∅ ↔ 𝐹 = (𝐴 × {𝑍}))) | ||
Theorem | fczsupp0 7489 | The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.) |
⊢ ((𝐵 × {𝑍}) supp 𝑍) = ∅ | ||
Theorem | suppss 7490* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) | ||
Theorem | suppssr 7491 | A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍) | ||
Theorem | suppssov1 7492* | Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppssof1 7493* | Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → (𝐴 supp 𝑌) ⊆ 𝐿) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ (𝜑 → 𝐴:𝐷⟶𝑉) & ⊢ (𝜑 → 𝐵:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 ∘𝑓 𝑂𝐵) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppss2 7494* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊) | ||
Theorem | suppsssn 7495* | Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ {𝑊}) | ||
Theorem | suppssfv 7496* | Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) & ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppofss1d 7497* | Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑍𝑋𝑥) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | suppofss2d 7498* | Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥𝑋𝑍) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑋𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑍)) | ||
Theorem | supp0cosupp0 7499 | The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 supp 𝑍) = ∅ → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅)) | ||
Theorem | imacosupp 7500 | The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |