![]() |
Metamath
Proof Explorer Theorem List (p. 72 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 | fnfvelrnd 7101 | A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | ffvelcdmi 7102 | A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelcdmda 7103 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelcdmd 7104 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | feldmfvelcdm 7105 | A class is an element of the domain iff it's function value is an element of the codomain of a function. (Contributed by AV, 22-Apr-2025.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∅ ∉ 𝐵) → (𝑋 ∈ 𝐴 ↔ (𝐹‘𝑋) ∈ 𝐵)) | ||
Theorem | rexrn 7106* | Restricted existential quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | ralrn 7107* | Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | elrnrexdm 7108* | For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ (Fun 𝐹 → (𝑌 ∈ ran 𝐹 → ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥))) | ||
Theorem | elrnrexdmb 7109* | For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
⊢ (Fun 𝐹 → (𝑌 ∈ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥))) | ||
Theorem | eldmrexrn 7110* | For any element in the domain of a function there is an element in the range of the function which is the function value for the element of the domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ (Fun 𝐹 → (𝑌 ∈ dom 𝐹 → ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌))) | ||
Theorem | eldmrexrnb 7111* | For any element in the domain of a function, there is an element in the range of the function which is the value of the function at that element. Because of the definition df-fv 6570 of the value of a function, the theorem is only valid in general if the empty set is not contained in the range of the function (the implication "to the right" is always valid). Indeed, with the definition df-fv 6570 of the value of a function, (𝐹‘𝑌) = ∅ may mean that the value of 𝐹 at 𝑌 is the empty set or that 𝐹 is not defined at 𝑌. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → (𝑌 ∈ dom 𝐹 ↔ ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌))) | ||
Theorem | fvcofneq 7112* | The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019.) |
⊢ ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋))) | ||
Theorem | ralrnmptw 7113* | A restricted quantifier over an image set. Version of ralrnmpt 7115 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2374. (Revised by GG, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexrnmptw 7114* | A restricted quantifier over an image set. Version of rexrnmpt 7116 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2374. (Revised by GG, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrnmpt 7115* | A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker ralrnmptw 7113 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexrnmpt 7116* | A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker rexrnmptw 7114 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | f0cli 7117 | Unconditional closure of a function when the codomain includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.) |
⊢ 𝐹:𝐴⟶𝐵 & ⊢ ∅ ∈ 𝐵 ⇒ ⊢ (𝐹‘𝐶) ∈ 𝐵 | ||
Theorem | dff2 7118 | Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵))) | ||
Theorem | dff3 7119* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) | ||
Theorem | dff4 7120* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) | ||
Theorem | dffo3 7121* | An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | dffo4 7122* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) | ||
Theorem | dffo5 7123* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) | ||
Theorem | exfo 7124* | A relation equivalent to the existence of an onto mapping. The right-hand 𝑓 is not necessarily a function. (Contributed by NM, 20-Mar-2007.) |
⊢ (∃𝑓 𝑓:𝐴–onto→𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦𝑓𝑥)) | ||
Theorem | dffo3f 7125* | An onto mapping expressed in terms of function values. As dffo3 7121 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | foelrn 7126* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foelrnf 7127* | Property of a surjective function. As foelrn 7126 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foco2 7128 | If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶) → 𝐹:𝐵–onto→𝐶) | ||
Theorem | fmpt 7129* | Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | f1ompt 7130* | Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) | ||
Theorem | fmpti 7131* | Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 | ||
Theorem | fvmptelcdm 7132* | The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
Theorem | fmptd 7133* | Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmpttd 7134* | Version of fmptd 7133 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) | ||
Theorem | fmpt3d 7135* | Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmptdf 7136* | A version of fmptd 7133 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fompt 7137* | Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = 𝐶)) | ||
Theorem | ffnfv 7138* | A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | ffnfvf 7139 | A function maps to a class to which all values belong. This version of ffnfv 7138 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | fnfvrnss 7140* | An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) | ||
Theorem | fcdmssb 7141* | A function is a function into a subset of its codomain if all of its values are elements of this subset. (Contributed by AV, 7-Feb-2021.) |
⊢ ((𝑉 ⊆ 𝑊 ∧ ∀𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈ 𝑉) → (𝐹:𝐴⟶𝑊 ↔ 𝐹:𝐴⟶𝑉)) | ||
Theorem | rnmptss 7142* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | fmpt2d 7143* | Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | ffvresb 7144* | A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵))) | ||
Theorem | fssrescdmd 7145 | Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝐶) ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐷) | ||
Theorem | f1oresrab 7146* | Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | f1ossf1o 7147* | Restricting a bijection, which is a mapping from a restricted class abstraction, to a subset is a bijection. (Contributed by AV, 7-Aug-2022.) |
⊢ 𝑋 = {𝑤 ∈ 𝐴 ∣ (𝜓 ∧ 𝜒)} & ⊢ 𝑌 = {𝑤 ∈ 𝐴 ∣ 𝜓} & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝑌 ↦ 𝐵) & ⊢ (𝜑 → 𝐺:𝑌–1-1-onto→𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 = 𝐵) → (𝜏 ↔ [𝑥 / 𝑤]𝜒)) ⇒ ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→{𝑦 ∈ 𝐶 ∣ 𝜏}) | ||
Theorem | fmptco 7148* | Composition of two functions expressed as ordered-pair class abstractions. If 𝐹 has the equation (𝑥 + 2) and 𝐺 the equation (3∗𝑧) then (𝐺 ∘ 𝐹) has the equation (3∗(𝑥 + 2)). (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) | ||
Theorem | fmptcof 7149* | Version of fmptco 7148 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) | ||
Theorem | fmptcos 7150* | Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆)) | ||
Theorem | cofmpt 7151* | Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.) |
⊢ (𝜑 → 𝐹:𝐶⟶𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) | ||
Theorem | fcompt 7152* | Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) | ||
Theorem | fcoconst 7153 | Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) | ||
Theorem | fsn 7154 | A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉}) | ||
Theorem | fsn2 7155 | A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹:{𝐴}⟶𝐵 ↔ ((𝐹‘𝐴) ∈ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) | ||
Theorem | fsng 7156 | A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉})) | ||
Theorem | fsn2g 7157 | A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐹:{𝐴}⟶𝐵 ↔ ((𝐹‘𝐴) ∈ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}))) | ||
Theorem | xpsng 7158 | The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) | ||
Theorem | xpprsng 7159 | The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {〈𝐴, 𝐶〉, 〈𝐵, 𝐶〉}) | ||
Theorem | xpsn 7160 | The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by NM, 4-Nov-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉} | ||
Theorem | f1o2sn 7161 | A singleton consisting in a nested ordered pair is a one-to-one function from the cartesian product of two singletons onto a singleton (case where the two singletons are equal). (Contributed by AV, 15-Aug-2019.) |
⊢ ((𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → {〈〈𝐸, 𝐸〉, 𝑋〉}:({𝐸} × {𝐸})–1-1-onto→{𝑋}) | ||
Theorem | residpr 7162 | Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( I ↾ {𝐴, 𝐵}) = {〈𝐴, 𝐴〉, 〈𝐵, 𝐵〉}) | ||
Theorem | dfmpt 7163 | Alternate definition for the maps-to notation df-mpt 5231 (although it requires that 𝐵 be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} | ||
Theorem | fnasrn 7164 | A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉) | ||
Theorem | idref 7165* | 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 7166* | A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.) |
⊢ (Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) | ||
Theorem | funopsn 7167* | 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.) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng 6618, as relsnopg 5815 is to relop 5863. (New usage is discouraged.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})) | ||
Theorem | funop 7168* | An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng 6618, as relsnopg 5815 is to relop 5863. (New usage is discouraged.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ (Fun 〈𝑋, 𝑌〉 ↔ ∃𝑎(𝑋 = {𝑎} ∧ 〈𝑋, 𝑌〉 = {〈𝑎, 𝑎〉})) | ||
Theorem | funopdmsn 7169 | 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 7170 | 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 7171 | 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 7172 | If 𝐴 is not in 𝐶, then the restriction of a singleton of 〈𝐴, 𝐵〉 to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.) |
⊢ (¬ 𝐴 ∈ 𝐶 → ({〈𝐴, 𝐵〉} ↾ 𝐶) = ∅) | ||
Theorem | fpr 7173 | 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 7174 | A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.) |
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) | ||
Theorem | ftpg 7175 | A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) | ||
Theorem | ftp 7176 | 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 7177 | A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) | ||
Theorem | funressn 7178 | A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (Fun 𝐹 → (𝐹 ↾ {𝐵}) ⊆ {〈𝐵, (𝐹‘𝐵)〉}) | ||
Theorem | fressnfv 7179 | The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) | ||
Theorem | fvrnressn 7180 | 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 7181 | 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 | fvn0fvelrnOLD 7182 | Obsolete version of fvn0fvelrn 6937 as of 13-Jan-2025. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐹‘𝑋) ≠ ∅ → (𝐹‘𝑋) ∈ ran 𝐹) | ||
Theorem | fvconst 7183 | The value of a constant function. (Contributed by NM, 30-May-1999.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) | ||
Theorem | fnsnr 7184 | 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 7185 | 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 7186* | 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 7187* | Express a singleton function in maps-to notation. Version of fmptsn 7186 allowing the value 𝐵 to depend on the variable 𝑥. (Contributed by AV, 27-Feb-2019.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptsnd 7188* | Express a singleton function in maps-to notation. Deduction form of fmptsng 7187. (Contributed by AV, 4-Aug-2019.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptap 7189* | Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑅 ∪ {𝐴}) = 𝑆 & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶) | ||
Theorem | fmptapd 7190* | Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) (Revised by AV, 10-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶)) | ||
Theorem | fmptpr 7191* | Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) | ||
Theorem | fvresi 7192 | The value of a restricted identity function. (Contributed by NM, 19-May-2004.) |
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) | ||
Theorem | fninfp 7193* | Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∩ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝑥}) | ||
Theorem | fnelfp 7194 | Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑋) = 𝑋)) | ||
Theorem | fndifnfp 7195* | Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∖ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝑥}) | ||
Theorem | fnelnfp 7196 | Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) | ||
Theorem | fnnfpeq0 7197 | A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ (𝐹 Fn 𝐴 → (dom (𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴))) | ||
Theorem | fvunsn 7198 | 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 7199 | 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 7200 | 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 ⇒ ⊢ ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |