Home | Metamath
Proof Explorer Theorem List (p. 61 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fnresdisj 6001 | A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004.) |
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐹 ↾ 𝐵) = ∅)) | ||
Theorem | 2elresin 6002 | Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) ↔ (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) | ||
Theorem | fnssresb 6003 | Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007.) |
⊢ (𝐹 Fn 𝐴 → ((𝐹 ↾ 𝐵) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴)) | ||
Theorem | fnssres 6004 | Restriction of a function with a subclass of its domain. (Contributed by NM, 2-Aug-1994.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) Fn 𝐵) | ||
Theorem | fnresin1 6005 | Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐴 ∩ 𝐵)) Fn (𝐴 ∩ 𝐵)) | ||
Theorem | fnresin2 6006 | Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ (𝐵 ∩ 𝐴)) Fn (𝐵 ∩ 𝐴)) | ||
Theorem | fnres 6007* | An equivalence for functionality of a restriction. Compare dffun8 5916. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) | ||
Theorem | fnresi 6008 | Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.) |
⊢ ( I ↾ 𝐴) Fn 𝐴 | ||
Theorem | idssxp 6009 | A diagonal set as a subset of a Cartesian product. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴) | ||
Theorem | fnima 6010 | The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) = ran 𝐹) | ||
Theorem | fn0 6011 | A function with empty domain is empty. (Contributed by NM, 15-Apr-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) | ||
Theorem | fnimadisj 6012 | A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐹 Fn 𝐴 ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 “ 𝐶) = ∅) | ||
Theorem | fnimaeq0 6013 | Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 37621. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐹 “ 𝐵) = ∅ ↔ 𝐵 = ∅)) | ||
Theorem | dfmpt3 6014 | Alternate definition for the "maps to" notation df-mpt 4730. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 ({𝑥} × {𝐵}) | ||
Theorem | mptfnf 6015 | The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
Theorem | fnmptf 6016 | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
Theorem | fnopabg 6017* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) |
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ↔ 𝐹 Fn 𝐴) | ||
Theorem | fnopab 6018* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 5-Mar-1996.) |
⊢ (𝑥 ∈ 𝐴 → ∃!𝑦𝜑) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ 𝐹 Fn 𝐴 | ||
Theorem | mptfng 6019* | The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴) | ||
Theorem | fnmpt 6020* | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴) | ||
Theorem | mpt0 6021 | A mapping operation with empty domain. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝑥 ∈ ∅ ↦ 𝐴) = ∅ | ||
Theorem | fnmpti 6022* | Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ 𝐹 Fn 𝐴 | ||
Theorem | dmmpti 6023* | Domain of the mapping operation. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
Theorem | dmmptd 6024* | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
Theorem | mptun 6025 | Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↦ 𝐶) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ∪ (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | feq1 6026 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | ||
Theorem | feq2 6027 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | ||
Theorem | feq3 6028 | Equality theorem for functions. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵)) | ||
Theorem | feq23 6029 | Equality theorem for functions. (Contributed by FL, 14-Jul-2007.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)) | ||
Theorem | feq1d 6030 | Equality deduction for functions. (Contributed by NM, 19-Feb-2008.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | ||
Theorem | feq2d 6031 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)) | ||
Theorem | feq3d 6032 | Equality deduction for functions. (Contributed by AV, 1-Jan-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵)) | ||
Theorem | feq12d 6033 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶)) | ||
Theorem | feq123d 6034 | Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐷)) | ||
Theorem | feq123 6035 | Equality theorem for functions. (Contributed by FL, 16-Nov-2008.) |
⊢ ((𝐹 = 𝐺 ∧ 𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐶⟶𝐷)) | ||
Theorem | feq1i 6036 | Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵) | ||
Theorem | feq2i 6037 | Equality inference for functions. (Contributed by NM, 5-Sep-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶) | ||
Theorem | feq12i 6038 | Equality inference for functions. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝐹 = 𝐺 & ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶) | ||
Theorem | feq23i 6039 | Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷) | ||
Theorem | feq23d 6040 | Equality deduction for functions. (Contributed by NM, 8-Jun-2013.) |
⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷)) | ||
Theorem | nff 6041 | Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐹:𝐴⟶𝐵 | ||
Theorem | sbcfng 6042* | Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑥]𝐹 Fn 𝐴 ↔ ⦋𝑋 / 𝑥⦌𝐹 Fn ⦋𝑋 / 𝑥⦌𝐴)) | ||
Theorem | sbcfg 6043* | Distribute proper substitution through the function predicate with domain and codomain. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑥]𝐹:𝐴⟶𝐵 ↔ ⦋𝑋 / 𝑥⦌𝐹:⦋𝑋 / 𝑥⦌𝐴⟶⦋𝑋 / 𝑥⦌𝐵)) | ||
Theorem | elimf 6044 | Eliminate a mapping hypothesis for the weak deduction theorem dedth 4139, when a special case 𝐺:𝐴⟶𝐵 is provable, in order to convert 𝐹:𝐴⟶𝐵 from a hypothesis to an antecedent. (Contributed by NM, 24-Aug-2006.) |
⊢ 𝐺:𝐴⟶𝐵 ⇒ ⊢ if(𝐹:𝐴⟶𝐵, 𝐹, 𝐺):𝐴⟶𝐵 | ||
Theorem | ffn 6045 | A mapping is a function with domain. (Contributed by NM, 2-Aug-1994.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | ||
Theorem | ffnd 6046 | A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 Fn 𝐴) | ||
Theorem | dffn2 6047 | Any function is a mapping into V. (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V) | ||
Theorem | ffun 6048 | A mapping is a function. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) | ||
Theorem | ffund 6049 | A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | frel 6050 | A mapping is a relation. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) | ||
Theorem | fdm 6051 | The domain of a mapping. (Contributed by NM, 2-Aug-1994.) |
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | ||
Theorem | fdmi 6052 | The domain of a mapping. (Contributed by NM, 28-Jul-2008.) |
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ dom 𝐹 = 𝐴 | ||
Theorem | frn 6053 | The range of a mapping. (Contributed by NM, 3-Aug-1994.) |
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) | ||
Theorem | dffn3 6054 | A function maps to its range. (Contributed by NM, 1-Sep-1999.) |
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) | ||
Theorem | ffrn 6055 | A function maps to its range. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶ran 𝐹) | ||
Theorem | fss 6056 | Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶) | ||
Theorem | fssd 6057 | Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fco 6058 | Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
Theorem | fco2 6059 | Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
⊢ (((𝐹 ↾ 𝐵):𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
Theorem | fssxp 6060 | A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) | ||
Theorem | funssxp 6061 | Two ways of specifying a partial function from 𝐴 to 𝐵. (Contributed by NM, 13-Nov-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ (𝐴 × 𝐵)) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) | ||
Theorem | ffdm 6062 | A mapping is a partial function. (Contributed by NM, 25-Nov-2007.) |
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) | ||
Theorem | ffdmd 6063 | The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵) | ||
Theorem | fdmrn 6064 | A different way to write 𝐹 is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ (Fun 𝐹 ↔ 𝐹:dom 𝐹⟶ran 𝐹) | ||
Theorem | opelf 6065 | The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 〈𝐶, 𝐷〉 ∈ 𝐹) → (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) | ||
Theorem | fun 6066 | The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.) |
⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷)) | ||
Theorem | fun2 6067 | The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶) | ||
Theorem | fun2d 6068 | The union of functions with disjoint domains is a function, deduction version of fun2 6067. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶) | ||
Theorem | fnfco 6069 | Composition of two functions. (Contributed by NM, 22-May-2006.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺:𝐵⟶𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵) | ||
Theorem | fssres 6070 | Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) | ||
Theorem | fssresd 6071 | Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵) | ||
Theorem | fssres2 6072 | Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005.) |
⊢ (((𝐹 ↾ 𝐴):𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) | ||
Theorem | fresin 6073 | An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ 𝑋):(𝐴 ∩ 𝑋)⟶𝐵) | ||
Theorem | resasplit 6074 | If two functions agree on their common domain, express their union as a union of three functions with pairwise disjoint domains. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) = ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴))))) | ||
Theorem | fresaun 6075 | The union of two functions which agree on their common domain is a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶) | ||
Theorem | fresaunres2 6076 | From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺) | ||
Theorem | fresaunres1 6077 | From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹) | ||
Theorem | fcoi1 6078 | Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹) | ||
Theorem | fcoi2 6079 | Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹) | ||
Theorem | feu 6080* | There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ∃!𝑦 ∈ 𝐵 〈𝐶, 𝑦〉 ∈ 𝐹) | ||
Theorem | fimass 6081 | The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝑋) ⊆ 𝐵) | ||
Theorem | fcnvres 6082 | The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998.) |
⊢ (𝐹:𝐴⟶𝐵 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ 𝐵)) | ||
Theorem | fimacnvdisj 6083 | The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (◡𝐹 “ 𝐶) = ∅) | ||
Theorem | fint 6084* | Function into an intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ 𝐵 ≠ ∅ ⇒ ⊢ (𝐹:𝐴⟶∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐹:𝐴⟶𝑥) | ||
Theorem | fin 6085 | Mapping into an intersection. (Contributed by NM, 14-Sep-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝐹:𝐴⟶(𝐵 ∩ 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴⟶𝐶)) | ||
Theorem | f0 6086 | The empty function. (Contributed by NM, 14-Aug-1999.) |
⊢ ∅:∅⟶𝐴 | ||
Theorem | f00 6087 | A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003.) |
⊢ (𝐹:𝐴⟶∅ ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) | ||
Theorem | f0bi 6088 | A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅) | ||
Theorem | f0dom0 6089 | A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019.) |
⊢ (𝐹:𝑋⟶𝑌 → (𝑋 = ∅ ↔ 𝐹 = ∅)) | ||
Theorem | f0rn0 6090* | If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018.) |
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → 𝑋 = ∅) | ||
Theorem | fconst 6091 | A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵} | ||
Theorem | fconstg 6092 | A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | ||
Theorem | fnconstg 6093 | A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴) | ||
Theorem | fconst6g 6094 | Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶) | ||
Theorem | fconst6 6095 | A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009.) (Revised by Mario Carneiro, 22-Apr-2015.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝐴 × {𝐵}):𝐴⟶𝐶 | ||
Theorem | f1eq1 6096 | Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵)) | ||
Theorem | f1eq2 6097 | Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶)) | ||
Theorem | f1eq3 6098 | Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵)) | ||
Theorem | nff1 6099 | Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐹:𝐴–1-1→𝐵 | ||
Theorem | dff12 6100* | Alternate definition of a one-to-one function. (Contributed by NM, 31-Dec-1996.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦∃*𝑥 𝑥𝐹𝑦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |