Home | Metamath
Proof Explorer Theorem List (p. 69 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 | fvreseq0 6801* | Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fvreseq1 6802* | Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fvreseq 6803* | Equality of restricted functions is determined by their values. (Contributed by NM, 3-Aug-1994.) (Proof shortened by AV, 4-Mar-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fnmptfvd 6804* | A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.) |
⊢ (𝜑 → 𝑀 Fn 𝐴) & ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷)) | ||
Theorem | fndmdif 6805* | Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)}) | ||
Theorem | fndmdifcom 6806 | The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹)) | ||
Theorem | fndmdifeq0 6807 | The difference set of two functions is empty if and only if the functions are equal. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (dom (𝐹 ∖ 𝐺) = ∅ ↔ 𝐹 = 𝐺)) | ||
Theorem | fndmin 6808* | Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)}) | ||
Theorem | fneqeql 6809 | Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴)) | ||
Theorem | fneqeql2 6810 | Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) | ||
Theorem | fnreseql 6811 | Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → ((𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ↔ 𝑋 ⊆ dom (𝐹 ∩ 𝐺))) | ||
Theorem | chfnrn 6812* | The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain. (Contributed by NM, 31-Aug-1999.) |
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝑥) → ran 𝐹 ⊆ ∪ 𝐴) | ||
Theorem | funfvop 6813 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 14-Oct-1996.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) | ||
Theorem | funfvbrb 6814 | Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.) |
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴))) | ||
Theorem | fvimacnvi 6815 | A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) | ||
Theorem | fvimacnv 6816 | The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 6431 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | funimass3 6817 | A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv 6816 would be the special case of 𝐴 being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵))) | ||
Theorem | funimass5 6818* | A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | funconstss 6819* | Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
Theorem | fvimacnvALT 6820 | Alternate proof of fvimacnv 6816, based on funimass3 6817. If funimass3 6817 is ever proved directly, as opposed to using funimacnv 6429 pointwise, then the proof of funimacnv 6429 should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | elpreima 6821 | Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) | ||
Theorem | elpreimad 6822 | Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶)) | ||
Theorem | fniniseg 6823 | Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.) |
⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) | ||
Theorem | fncnvima2 6824* | Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵}) | ||
Theorem | fniniseg2 6825* | Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵}) | ||
Theorem | unpreima 6826 | Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵))) | ||
Theorem | inpreima 6827 | Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵))) | ||
Theorem | difpreima 6828 | Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵))) | ||
Theorem | respreima 6829 | The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) | ||
Theorem | iinpreima 6830* | Preimage of an intersection. (Contributed by FL, 16-Apr-2012.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
Theorem | intpreima 6831* | Preimage of an intersection. (Contributed by FL, 28-Apr-2012.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝐴) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
Theorem | fimacnv 6832 | The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.) |
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) | ||
Theorem | fimacnvinrn 6833 | Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (Fun 𝐹 → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ ran 𝐹))) | ||
Theorem | fimacnvinrn2 6834 | Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → (◡𝐹 “ 𝐴) = (◡𝐹 “ (𝐴 ∩ 𝐵))) | ||
Theorem | fvn0ssdmfun 6835* | If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 6702. (Contributed by AV, 27-Jan-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (∀𝑎 ∈ 𝐷 (𝐹‘𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷))) | ||
Theorem | fnopfv 6836 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 〈𝐵, (𝐹‘𝐵)〉 ∈ 𝐹) | ||
Theorem | fvelrn 6837 | A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | nelrnfvne 6838 | A function value cannot be any element not contained in the range of the function. (Contributed by AV, 28-Jan-2020.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∉ ran 𝐹) → (𝐹‘𝑋) ≠ 𝑌) | ||
Theorem | fveqdmss 6839* | If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝐷 = dom 𝐵 ⇒ ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → 𝐷 ⊆ dom 𝐴) | ||
Theorem | fveqressseq 6840* | If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the class restricted to the domain of the function is the function itself. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝐷 = dom 𝐵 ⇒ ⊢ ((Fun 𝐵 ∧ ∅ ∉ ran 𝐵 ∧ ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) = (𝐵‘𝑥)) → (𝐴 ↾ 𝐷) = 𝐵) | ||
Theorem | fnfvelrn 6841 | A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | ffvelrn 6842 | A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelrni 6843 | A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelrnda 6844 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelrnd 6845 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | rexrn 6846* | 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 6847* | 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 6848* | 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 6849* | 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 6850* | 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 6851* | 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 6357 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 6357 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 6852* | 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 6853* | Version of ralrnmpt 6855 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexrnmptw 6854* | Version of rexrnmpt 6856 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrnmpt 6855* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexrnmpt 6856* | A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | f0cli 6857 | Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.) |
⊢ 𝐹:𝐴⟶𝐵 & ⊢ ∅ ∈ 𝐵 ⇒ ⊢ (𝐹‘𝐶) ∈ 𝐵 | ||
Theorem | dff2 6858 | Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵))) | ||
Theorem | dff3 6859* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) | ||
Theorem | dff4 6860* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) | ||
Theorem | dffo3 6861* | An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | dffo4 6862* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) | ||
Theorem | dffo5 6863* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) | ||
Theorem | exfo 6864* | 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 | foelrn 6865* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foco2 6866 | 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 6867* | Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | f1ompt 6868* | 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 6869* | Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 | ||
Theorem | fvmptelrn 6870* | The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
Theorem | fmptd 6871* | Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmpttd 6872* | Version of fmptd 6871 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 6873* | Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmptdf 6874* | A version of fmptd 6871 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | ffnfv 6875* | A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | ffnfvf 6876 | A function maps to a class to which all values belong. This version of ffnfv 6875 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | fnfvrnss 6877* | An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) | ||
Theorem | frnssb 6878* | 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 6879* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | fmpt2d 6880* | Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | ffvresb 6881* | A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵))) | ||
Theorem | f1oresrab 6882* | 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 6883* | 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 6884* | 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 6885* | Version of fmptco 6884 where 𝜑 needn't be distinct from 𝑥. (Contributed by NM, 27-Dec-2014.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) | ||
Theorem | fmptcos 6886* | Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆)) | ||
Theorem | cofmpt 6887* | Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.) |
⊢ (𝜑 → 𝐹:𝐶⟶𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) | ||
Theorem | fcompt 6888* | 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 6889 | Composition with a constant function. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) | ||
Theorem | fsn 6890 | 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 6891 | 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 6892 | 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 6893 | 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 6894 | The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) | ||
Theorem | xpprsng 6895 | The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} × {𝐶}) = {〈𝐴, 𝐶〉, 〈𝐵, 𝐶〉}) | ||
Theorem | xpsn 6896 | 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 6897 | 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 6898 | Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( I ↾ {𝐴, 𝐵}) = {〈𝐴, 𝐴〉, 〈𝐵, 𝐵〉}) | ||
Theorem | dfmpt 6899 | Alternate definition for the maps-to notation df-mpt 5139 (although it requires that 𝐵 be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} | ||
Theorem | fnasrn 6900 | 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 (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |