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