![]() |
Metamath
Proof Explorer Theorem List (p. 73 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fvsnun1 7201 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7202. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | fvsnun2 7202 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 7201. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) & ⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴})) ⇒ ⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷)) | ||
Theorem | fnsnsplit 7203 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉})) | ||
Theorem | fsnunf 7204 | Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {〈𝑋, 𝑌〉}):(𝑆 ∪ {𝑋})⟶𝑇) | ||
Theorem | fsnunf2 7205 | Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:(𝑆 ∖ {𝑋})⟶𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {〈𝑋, 𝑌〉}):𝑆⟶𝑇) | ||
Theorem | fsnunfv 7206 | Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋) = 𝑌) | ||
Theorem | fsnunres 7207 | Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ 𝑆) = 𝐹) | ||
Theorem | funresdfunsn 7208 | Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉}) = 𝐹) | ||
Theorem | fvpr1g 7209 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) | ||
Theorem | fvpr2g 7210 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened by BJ, 26-Sep-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐵) = 𝐷) | ||
Theorem | fvpr1 7211 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by BJ, 26-Sep-2024.) |
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) | ||
Theorem | fvpr2 7212 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by BJ, 26-Sep-2024.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐵) = 𝐷) | ||
Theorem | fprb 7213* | A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) | ||
Theorem | fvtp1 7214 | The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐴) = 𝐷) | ||
Theorem | fvtp2 7215 | The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐵) = 𝐸) | ||
Theorem | fvtp3 7216 | The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐶 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐶) = 𝐹) | ||
Theorem | fvtp1g 7217 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐴) = 𝐷) | ||
Theorem | fvtp2g 7218 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐵) = 𝐸) | ||
Theorem | fvtp3g 7219 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐶) = 𝐹) | ||
Theorem | tpres 7220 | An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020.) |
⊢ (𝜑 → 𝑇 = {〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐴) & ⊢ (𝜑 → 𝐶 ≠ 𝐴) ⇒ ⊢ (𝜑 → (𝑇 ↾ (V ∖ {𝐴})) = {〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}) | ||
Theorem | fvconst2g 7221 | The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2g 7222 | A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007.) |
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))) | ||
Theorem | fvconst2 7223 | The value of a constant function. (Contributed by NM, 16-Apr-2005.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2 7224 | A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | fconst5 7225 | Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅) → (𝐹 = (𝐴 × {𝐵}) ↔ ran 𝐹 = {𝐵})) | ||
Theorem | rnmptc 7226* | Range of a constant function in maps-to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Remove extra hypothesis. (Revised by SN, 17-Apr-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ran 𝐹 = {𝐵}) | ||
Theorem | fnprb 7227 | A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by FL, 26-Jun-2011.) (Proof shortened by Scott Fenton, 12-Oct-2017.) Eliminate unnecessary antecedent 𝐴 ≠ 𝐵. (Revised by NM, 29-Dec-2018.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) | ||
Theorem | fntpb 7228 | A function whose domain has at most three elements can be represented as a set of at most three ordered pairs. (Contributed by AV, 26-Jan-2021.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) | ||
Theorem | fnpr2g 7229 | A function whose domain has at most two elements can be represented as a set of at most two ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) | ||
Theorem | fpr2g 7230 | A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹:{𝐴, 𝐵}⟶𝐶 ↔ ((𝐹‘𝐴) ∈ 𝐶 ∧ (𝐹‘𝐵) ∈ 𝐶 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}))) | ||
Theorem | fconstfv 7231* | A constant function expressed in terms of its functionality, domain, and value. See also fconst2 7224. (Contributed by NM, 27-Aug-2004.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) | ||
Theorem | fconst3 7232 | Two ways to express a constant function. (Contributed by NM, 15-Mar-2007.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
Theorem | fconst4 7233 | Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴)) | ||
Theorem | resfunexg 7234 | The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | resiexd 7235 | The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V) | ||
Theorem | fnex 7236 | If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 7234. See fnexALT 7973 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | fnexd 7237 | If the domain of a function is a set, the function is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | funex 7238 | If the domain of a function exists, so does the function. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex 7236. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.) (Contributed by NM, 11-Nov-1995.) |
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | opabex 7239* | Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | mptexg 7240* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptexgf 7241 | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) (Revised by Thierry Arnoux, 17-May-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptex 7242* | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7240. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | mptexd 7243* | If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7240. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptrabex 7244* | If the domain of a function given by maps-to notation is a class abstraction based on a set, the function is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↦ 𝐵) ∈ V | ||
Theorem | fex 7245 | If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | ||
Theorem | fexd 7246 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | mptfvmpt 7247* | A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022.) |
⊢ (𝑦 = 𝑌 → 𝑀 = (𝑥 ∈ 𝑉 ↦ 𝐴)) & ⊢ 𝐺 = (𝑦 ∈ 𝑊 ↦ 𝑀) & ⊢ 𝑉 = (𝐹‘𝑋) ⇒ ⊢ (𝑌 ∈ 𝑊 → (𝐺‘𝑌) = (𝑥 ∈ 𝑉 ↦ 𝐴)) | ||
Theorem | eufnfv 7248* | A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵) | ||
Theorem | funfvima 7249 | A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2 7250 | A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2d 7251 | A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.) (Revised by AV, 23-Mar-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ (𝐹 “ 𝐴)) | ||
Theorem | fnfvima 7252 | The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)) | ||
Theorem | fnfvimad 7253 | A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐶)) | ||
Theorem | resfvresima 7254 | The value of the function value of a restriction for a function restricted to the image of the restricting subset. (Contributed by AV, 6-Mar-2021.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑆 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐻 ↾ (𝐹 “ 𝑆))‘((𝐹 ↾ 𝑆)‘𝑋)) = (𝐻‘(𝐹‘𝑋))) | ||
Theorem | funfvima3 7255 | A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ 𝐺) → (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) ∈ (𝐺 “ {𝐴}))) | ||
Theorem | ralima 7256* | Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | rexima 7257* | Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reximaOLD 7258* | Obsolete version of rexima 7257 as of 14-Aug-2025. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ralimaOLD 7259* | Obsolete version of ralima 7256 as of 14-Aug-2025. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | fvclss 7260* | Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.) |
⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ⊆ (ran 𝐹 ∪ {∅}) | ||
Theorem | elabrex 7261* | Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | elabrexg 7262* | Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | abrexco 7263* | Composition of two image maps 𝐶(𝑦) and 𝐵(𝑤). (Contributed by NM, 27-May-2013.) |
⊢ 𝐵 ∈ V & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} | ||
Theorem | imaiun 7264* | The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶) | ||
Theorem | imauni 7265* | The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (Contributed by NM, 9-Aug-2004.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝑥) | ||
Theorem | fniunfv 7266* | The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹) | ||
Theorem | funiunfv 7267* |
The indexed union of a function's values is the union of its image under
the index class.
Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to 𝐹 Fn 𝐴, the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) | ||
Theorem | funiunfvf 7268* | The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 7267 uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006.) (Revised by David Abernethy, 15-Apr-2013.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) | ||
Theorem | eluniima 7269* | Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐵 ∈ ∪ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn 7270* | Membership in the union of the range of a function. See elunirnALT 7271 for a shorter proof which uses ax-pow 5370. See elfvunirn 6938 for a more general version of the reverse direction. (Contributed by NM, 24-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirnALT 7271* | Alternate proof of elunirn 7270. It is shorter but requires ax-pow 5370 (through eluniima 7269, funiunfv 7267, ndmfv 6941). (Contributed by NM, 24-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn2OLD 7272 | Obsolete version of elfvunirn 6938 as of 12-Jan-2025. (Contributed by Thierry Arnoux, 13-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (𝐹‘𝐴)) → 𝐵 ∈ ∪ ran 𝐹) | ||
Theorem | fnunirn 7273* | Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐹 Fn 𝐼 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝐼 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | dff13 7274* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | dff13f 7275* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 31-Jul-2003.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐹 ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1veqaeq 7276 | If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
Theorem | f1cofveqaeq 7277 | If the values of a composition of one-to-one functions for two arguments are equal, the arguments themselves must be equal. (Contributed by AV, 3-Feb-2021.) |
⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐹‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑌)) → 𝑋 = 𝑌)) | ||
Theorem | f1cofveqaeqALT 7278 | Alternate proof of f1cofveqaeq 7277, 1 essential step shorter, but having more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐹‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑌)) → 𝑋 = 𝑌)) | ||
Theorem | 2f1fvneq 7279 | If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌)) | ||
Theorem | f1mpt 7280* | Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦))) | ||
Theorem | f1fveq 7281 | Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1elima 7282 | Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌)) | ||
Theorem | f1imass 7283 | Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊆ (𝐹 “ 𝐷) ↔ 𝐶 ⊆ 𝐷)) | ||
Theorem | f1imaeq 7284 | Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) = (𝐹 “ 𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1imapss 7285 | Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊊ (𝐹 “ 𝐷) ↔ 𝐶 ⊊ 𝐷)) | ||
Theorem | fpropnf1 7286 | A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) |
⊢ 𝐹 = {〈𝑋, 𝑍〉, 〈𝑌, 𝑍〉} ⇒ ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑋 ≠ 𝑌) → (Fun 𝐹 ∧ ¬ Fun ◡𝐹)) | ||
Theorem | f1dom3fv3dif 7287 | The function values for a 1-1 function from a set with three different elements are different. (Contributed by AV, 20-Mar-2019.) |
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ (𝐹‘𝐶) ∧ (𝐹‘𝐵) ≠ (𝐹‘𝐶))) | ||
Theorem | f1dom3el3dif 7288* | The codomain of a 1-1 function from a set with three different elements has (at least) three different elements. (Contributed by AV, 20-Mar-2019.) |
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 ∃𝑧 ∈ 𝑅 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧)) | ||
Theorem | dff14a 7289* | A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐹‘𝑥) ≠ (𝐹‘𝑦)))) | ||
Theorem | dff14b 7290* | A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))) | ||
Theorem | f1ounsn 7291 | Extension of a bijection by an ordered pair. (Contributed by AV, 15-Sep-2025.) |
⊢ 𝐹 = (𝐺 ∪ {〈𝑋, 𝑌〉}) ⇒ ⊢ ((𝐺:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (𝑋 ∉ 𝐴 ∧ 𝑌 ∉ 𝐵)) → 𝐹:(𝐴 ∪ {𝑋})–1-1-onto→(𝐵 ∪ {𝑌})) | ||
Theorem | f12dfv 7292 | A one-to-one function with a domain with at least two different elements in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ 𝐴 = {𝑋, 𝑌} ⇒ ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))) | ||
Theorem | f13dfv 7293 | A one-to-one function with a domain with at least three different elements in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ 𝐴 = {𝑋, 𝑌, 𝑍} ⇒ ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))) | ||
Theorem | dff1o6 7294* | A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1ocnvfv1 7295 | The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv2 7296 | The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv 7297 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶)) | ||
Theorem | f1ocnvfvb 7298 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐹‘𝐶) = 𝐷 ↔ (◡𝐹‘𝐷) = 𝐶)) | ||
Theorem | nvof1o 7299 | An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | nvocnv 7300* | The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019.) |
⊢ ((𝐹:𝐴⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥) → ◡𝐹 = 𝐹) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |