Home | Metamath
Proof Explorer Theorem List (p. 70 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | idref 6901* | Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Revised by NM, 30-Mar-2016.) |
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | funiun 6902* | A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.) |
⊢ (Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) | ||
Theorem | funopsn 6903* | If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) (Proof shortened by AV, 15-Jul-2021.) (Avoid depending on this detail.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})) | ||
Theorem | funop 6904* | An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) (Avoid depending on this detail.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ (Fun 〈𝑋, 𝑌〉 ↔ ∃𝑎(𝑋 = {𝑎} ∧ 〈𝑋, 𝑌〉 = {〈𝑎, 𝑎〉})) | ||
Theorem | funopdmsn 6905 | The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021.) (Avoid depending on this detail.) |
⊢ 𝐺 = 〈𝑋, 𝑌〉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑊 ⇒ ⊢ ((Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺) → 𝐴 = 𝐵) | ||
Theorem | funsndifnop 6906 | A singleton of an ordered pair is not an ordered pair if the components are different. (Contributed by AV, 23-Sep-2020.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐴, 𝐵〉} ⇒ ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐺 ∈ (V × V)) | ||
Theorem | funsneqopb 6907 | A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐴, 𝐵〉} ⇒ ⊢ (𝐴 = 𝐵 ↔ 𝐺 ∈ (V × V)) | ||
Theorem | ressnop0 6908 | If 𝐴 is not in 𝐶, then the restriction of a singleton of 〈𝐴, 𝐵〉 to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.) |
⊢ (¬ 𝐴 ∈ 𝐶 → ({〈𝐴, 𝐵〉} ↾ 𝐶) = ∅) | ||
Theorem | fpr 6909 | A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) | ||
Theorem | fprg 6910 | A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.) |
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) | ||
Theorem | ftpg 6911 | A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) | ||
Theorem | ftp 6912 | A function with a domain of three elements. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens, 23-Jan-2018.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V & ⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 & ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉}:{𝐴, 𝐵, 𝐶}⟶{𝑋, 𝑌, 𝑍} | ||
Theorem | fnressn 6913 | A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) | ||
Theorem | funressn 6914 | A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (Fun 𝐹 → (𝐹 ↾ {𝐵}) ⊆ {〈𝐵, (𝐹‘𝐵)〉}) | ||
Theorem | fressnfv 6915 | The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) | ||
Theorem | fvrnressn 6916 | If the value of a function is in the range of the function restricted to the singleton containing the argument, then the value of the function is in the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝑋 ∈ 𝑉 → ((𝐹‘𝑋) ∈ ran (𝐹 ↾ {𝑋}) → (𝐹‘𝑋) ∈ ran 𝐹)) | ||
Theorem | fvressn 6917 | The value of a function restricted to the singleton containing the argument equals the value of the function for this argument. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝑋 ∈ 𝑉 → ((𝐹 ↾ {𝑋})‘𝑋) = (𝐹‘𝑋)) | ||
Theorem | fvn0fvelrn 6918 | If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ ((𝐹‘𝑋) ≠ ∅ → (𝐹‘𝑋) ∈ ran 𝐹) | ||
Theorem | fvconst 6919 | The value of a constant function. (Contributed by NM, 30-May-1999.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) | ||
Theorem | fnsnr 6920 | If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when 𝐴 is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) |
⊢ (𝐹 Fn {𝐴} → (𝐵 ∈ 𝐹 → 𝐵 = 〈𝐴, (𝐹‘𝐴)〉)) | ||
Theorem | fnsnb 6921 | A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Revised to add reverse implication. (Revised by NM, 29-Dec-2018.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) | ||
Theorem | fmptsn 6922* | Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptsng 6923* | Express a singleton function in maps-to notation. Version of fmptsn 6922 allowing the value 𝐵 to depend on the variable 𝑥. (Contributed by AV, 27-Feb-2019.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptsnd 6924* | Express a singleton function in maps-to notation. Deduction form of fmptsng 6923. (Contributed by AV, 4-Aug-2019.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptap 6925* | Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑅 ∪ {𝐴}) = 𝑆 & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶) | ||
Theorem | fmptapd 6926* | Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶)) | ||
Theorem | fmptpr 6927* | Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) | ||
Theorem | fvresi 6928 | The value of a restricted identity function. (Contributed by NM, 19-May-2004.) |
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) | ||
Theorem | fninfp 6929* | Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∩ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝑥}) | ||
Theorem | fnelfp 6930 | Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑋) = 𝑋)) | ||
Theorem | fndifnfp 6931* | Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∖ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝑥}) | ||
Theorem | fnelnfp 6932 | Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) | ||
Theorem | fnnfpeq0 6933 | A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ (𝐹 Fn 𝐴 → (dom (𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴))) | ||
Theorem | fvunsn 6934 | Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013.) (Revised by Mario Carneiro, 28-May-2014.) |
⊢ (𝐵 ≠ 𝐷 → ((𝐴 ∪ {〈𝐵, 𝐶〉})‘𝐷) = (𝐴‘𝐷)) | ||
Theorem | fvsng 6935 | The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.) (Proof shortened by BJ, 25-Feb-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) | ||
Theorem | fvsn 6936 | The value of a singleton of an ordered pair is the second member. (Contributed by NM, 12-Aug-1994.) (Proof shortened by BJ, 25-Feb-2023.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵 | ||
Theorem | fvsnun1 6937 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 6938. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | fvsnun2 6938 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 6937. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) & ⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴})) ⇒ ⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷)) | ||
Theorem | fnsnsplit 6939 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉})) | ||
Theorem | fsnunf 6940 | Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {〈𝑋, 𝑌〉}):(𝑆 ∪ {𝑋})⟶𝑇) | ||
Theorem | fsnunf2 6941 | Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:(𝑆 ∖ {𝑋})⟶𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {〈𝑋, 𝑌〉}):𝑆⟶𝑇) | ||
Theorem | fsnunfv 6942 | 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 6943 | Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ 𝑆) = 𝐹) | ||
Theorem | funresdfunsn 6944 | 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 | fvpr1 6945 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) | ||
Theorem | fvpr2 6946 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐵) = 𝐷) | ||
Theorem | fvpr1g 6947 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) | ||
Theorem | fvpr2g 6948 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐵) = 𝐷) | ||
Theorem | fprb 6949* | A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) | ||
Theorem | fvtp1 6950 | The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐴) = 𝐷) | ||
Theorem | fvtp2 6951 | The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐵) = 𝐸) | ||
Theorem | fvtp3 6952 | The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐶 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐶) = 𝐹) | ||
Theorem | fvtp1g 6953 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐴) = 𝐷) | ||
Theorem | fvtp2g 6954 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐵) = 𝐸) | ||
Theorem | fvtp3g 6955 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐶) = 𝐹) | ||
Theorem | tpres 6956 | 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 6957 | The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2g 6958 | A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007.) |
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))) | ||
Theorem | fvconst2 6959 | The value of a constant function. (Contributed by NM, 16-Apr-2005.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2 6960 | A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | fconst5 6961 | Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅) → (𝐹 = (𝐴 × {𝐵}) ↔ ran 𝐹 = {𝐵})) | ||
Theorem | rnmptc 6962* | Range of a constant function in maps-to notation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ran 𝐹 = {𝐵}) | ||
Theorem | fnprb 6963 | 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 6964 | 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 6965 | 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 6966 | A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹:{𝐴, 𝐵}⟶𝐶 ↔ ((𝐹‘𝐴) ∈ 𝐶 ∧ (𝐹‘𝐵) ∈ 𝐶 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}))) | ||
Theorem | fconstfv 6967* | A constant function expressed in terms of its functionality, domain, and value. See also fconst2 6960. (Contributed by NM, 27-Aug-2004.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) | ||
Theorem | fconst3 6968 | Two ways to express a constant function. (Contributed by NM, 15-Mar-2007.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
Theorem | fconst4 6969 | Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴)) | ||
Theorem | resfunexg 6970 | 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 6971 | The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V) | ||
Theorem | fnex 6972 | 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 6970. See fnexALT 7643 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | fnexd 6973 | 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 6974 | 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 6972. (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 6975* | Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | mptexg 6976* | 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 6977 | 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 6978* | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6976. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | mptexd 6979* | If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 6976. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptrabex 6980* | 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 6981 | If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | ||
Theorem | mptfvmpt 6982* | A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022.) |
⊢ (𝑦 = 𝑌 → 𝑀 = (𝑥 ∈ 𝑉 ↦ 𝐴)) & ⊢ 𝐺 = (𝑦 ∈ 𝑊 ↦ 𝑀) & ⊢ 𝑉 = (𝐹‘𝑋) ⇒ ⊢ (𝑌 ∈ 𝑊 → (𝐺‘𝑌) = (𝑥 ∈ 𝑉 ↦ 𝐴)) | ||
Theorem | eufnfv 6983* | A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵) | ||
Theorem | funfvima 6984 | A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2 6985 | A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | fnfvima 6986 | 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 6987 | A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐶)) | ||
Theorem | resfvresima 6988 | 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 6989 | 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 | rexima 6990* | Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ralima 6991* | Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | fvclss 6992* | Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.) |
⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ⊆ (ran 𝐹 ∪ {∅}) | ||
Theorem | elabrex 6993* | Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | abrexco 6994* | Composition of two image maps 𝐶(𝑦) and 𝐵(𝑤). (Contributed by NM, 27-May-2013.) |
⊢ 𝐵 ∈ V & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} | ||
Theorem | imaiun 6995* | The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶) | ||
Theorem | imauni 6996* | 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 6997* | 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 6998* |
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 6999* | The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 6998 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 7000* | Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐵 ∈ ∪ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (𝐹‘𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |