![]() |
Metamath
Proof Explorer Theorem List (p. 72 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dff4 7101* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) | ||
Theorem | dffo3 7102* | An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | dffo4 7103* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) | ||
Theorem | dffo5 7104* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) | ||
Theorem | exfo 7105* | 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 7106* | An onto mapping expressed in terms of function values. As dffo3 7102 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | foelrn 7107* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foelrnf 7108* | Property of a surjective function. As foelrn 7107 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foco2 7109 | 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 7110* | Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | f1ompt 7111* | 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 7112* | Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 | ||
Theorem | fvmptelcdm 7113* | The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
Theorem | fmptd 7114* | Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmpttd 7115* | Version of fmptd 7114 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 7116* | Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmptdf 7117* | A version of fmptd 7114 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fompt 7118* | Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = 𝐶)) | ||
Theorem | ffnfv 7119* | A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | ffnfvf 7120 | A function maps to a class to which all values belong. This version of ffnfv 7119 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | fnfvrnss 7121* | An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) | ||
Theorem | fcdmssb 7122* | 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 7123* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | fmpt2d 7124* | Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | ffvresb 7125* | A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵))) | ||
Theorem | f1oresrab 7126* | 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 7127* | 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 7128* | 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 7129* | Version of fmptco 7128 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) | ||
Theorem | fmptcos 7130* | Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆)) | ||
Theorem | cofmpt 7131* | Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.) |
⊢ (𝜑 → 𝐹:𝐶⟶𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) | ||
Theorem | fcompt 7132* | 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 7133 | Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) | ||
Theorem | fsn 7134 | 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 7135 | 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 7136 | 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 7137 | 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 7138 | The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩}) | ||
Theorem | xpprsng 7139 | The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐶⟩}) | ||
Theorem | xpsn 7140 | 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 7141 | 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 7142 | Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( I ↾ {𝐴, 𝐵}) = {⟨𝐴, 𝐴⟩, ⟨𝐵, 𝐵⟩}) | ||
Theorem | dfmpt 7143 | 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 7144 | 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 7145* | 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 7146* | A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020.) |
⊢ (Fun 𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{⟨𝑥, (𝐹‘𝑥)⟩}) | ||
Theorem | funopsn 7147* | 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 6598, as relsnopg 5802 is to relop 5849. (New usage is discouraged.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐹 = ⟨𝑋, 𝑌⟩) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {⟨𝑎, 𝑎⟩})) | ||
Theorem | funop 7148* | 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 6598, as relsnopg 5802 is to relop 5849. (New usage is discouraged.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V ⇒ ⊢ (Fun ⟨𝑋, 𝑌⟩ ↔ ∃𝑎(𝑋 = {𝑎} ∧ ⟨𝑋, 𝑌⟩ = {⟨𝑎, 𝑎⟩})) | ||
Theorem | funopdmsn 7149 | 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 7150 | 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 7151 | 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 7152 | If 𝐴 is not in 𝐶, then the restriction of a singleton of ⟨𝐴, 𝐵⟩ to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.) |
⊢ (¬ 𝐴 ∈ 𝐶 → ({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅) | ||
Theorem | fpr 7153 | 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 7154 | A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.) |
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) | ||
Theorem | ftpg 7155 | A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) | ||
Theorem | ftp 7156 | 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 7157 | A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩}) | ||
Theorem | funressn 7158 | A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (Fun 𝐹 → (𝐹 ↾ {𝐵}) ⊆ {⟨𝐵, (𝐹‘𝐵)⟩}) | ||
Theorem | fressnfv 7159 | The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) | ||
Theorem | fvrnressn 7160 | 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 7161 | 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 7162 | Obsolete version of fvn0fvelrn 6921 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 7163 | The value of a constant function. (Contributed by NM, 30-May-1999.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) | ||
Theorem | fnsnr 7164 | 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 7165 | 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 7166* | 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 7167* | Express a singleton function in maps-to notation. Version of fmptsn 7166 allowing the value 𝐵 to depend on the variable 𝑥. (Contributed by AV, 27-Feb-2019.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptsnd 7168* | Express a singleton function in maps-to notation. Deduction form of fmptsng 7167. (Contributed by AV, 4-Aug-2019.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {⟨𝐴, 𝐶⟩} = (𝑥 ∈ {𝐴} ↦ 𝐵)) | ||
Theorem | fmptap 7169* | Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑅 ∪ {𝐴}) = 𝑆 & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶) | ||
Theorem | fmptapd 7170* | Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) (Revised by AV, 10-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶)) | ||
Theorem | fmptpr 7171* | Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) ⇒ ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) | ||
Theorem | fvresi 7172 | The value of a restricted identity function. (Contributed by NM, 19-May-2004.) |
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) | ||
Theorem | fninfp 7173* | Express the class of fixed points of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∩ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝑥}) | ||
Theorem | fnelfp 7174 | Property of a fixed point of a function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑋) = 𝑋)) | ||
Theorem | fndifnfp 7175* | Express the class of non-fixed points of a function. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
⊢ (𝐹 Fn 𝐴 → dom (𝐹 ∖ I ) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝑥}) | ||
Theorem | fnelnfp 7176 | Property of a non-fixed point of a function. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑋) ≠ 𝑋)) | ||
Theorem | fnnfpeq0 7177 | A function is the identity iff it moves no points. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ (𝐹 Fn 𝐴 → (dom (𝐹 ∖ I ) = ∅ ↔ 𝐹 = ( I ↾ 𝐴))) | ||
Theorem | fvunsn 7178 | 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 7179 | 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 7180 | 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 7181 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7182. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | fvsnun2 7182 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 7181. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 25-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) & ⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴})) ⇒ ⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷)) | ||
Theorem | fnsnsplit 7183 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩})) | ||
Theorem | fsnunf 7184 | Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):(𝑆 ∪ {𝑋})⟶𝑇) | ||
Theorem | fsnunf2 7185 | Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:(𝑆 ∖ {𝑋})⟶𝑇 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):𝑆⟶𝑇) | ||
Theorem | fsnunfv 7186 | 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 7187 | Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ 𝑆) = 𝐹) | ||
Theorem | funresdfunsn 7188 | 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 7189 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶) | ||
Theorem | fvpr2g 7190 | 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 | fvpr2gOLD 7191 | Obsolete version of fvpr2g 7190 as of 26-Sep-2024. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷) | ||
Theorem | fvpr1 7192 | 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 | fvpr1OLD 7193 | Obsolete version of fvpr1 7192 as of 26-Sep-2024. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶) | ||
Theorem | fvpr2 7194 | 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 | fvpr2OLD 7195 | Obsolete version of fvpr2 7194 as of 26-Sep-2024. (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷) | ||
Theorem | fprb 7196* | A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩})) | ||
Theorem | fvtp1 7197 | The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷) | ||
Theorem | fvtp2 7198 | The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸) | ||
Theorem | fvtp3 7199 | The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐶 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹) | ||
Theorem | fvtp1g 7200 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |