![]() |
Metamath
Proof Explorer Theorem List (p. 71 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 | fvmptd2f 7001* | Alternate deduction version of fvmpt 6985, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) (Proof shortened by AV, 19-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
Theorem | fvmptdv 7002* | Alternate deduction version of fvmpt 6985, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝐴) = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → 𝜓)) | ||
Theorem | fvmptdv2 7003* | Alternate deduction version of fvmpt 6985, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶)) | ||
Theorem | mpteqb 7004* | Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv 7019. (Contributed by Mario Carneiro, 14-Nov-2014.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)) | ||
Theorem | fvmptt 7005* | Closed theorem form of fvmpt 6985. (Contributed by Scott Fenton, 21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptf 7006* | Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6983 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptnf 7007* | The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 7009 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐴) = ∅) | ||
Theorem | fvmptd3 7008* | Deduction version of fvmpt 6985. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | fvmptn 7009* | This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class 𝐶 it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 6983. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.) |
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (¬ 𝐶 ∈ V → (𝐹‘𝐷) = ∅) | ||
Theorem | fvmptss2 7010* | A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.) |
⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐹‘𝐷) ⊆ 𝐶 | ||
Theorem | elfvmptrab1w 7011* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Version of elfvmptrab1 7012 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Alexander van der Vekens, 15-Jul-2018.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | elfvmptrab1 7012* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker elfvmptrab1w 7011 when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) | ||
Theorem | elfvmptrab 7013* | Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → 𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀)) | ||
Theorem | fvopab4ndm 7014* | Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008.) |
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⇒ ⊢ (¬ 𝐵 ∈ 𝐴 → (𝐹‘𝐵) = ∅) | ||
Theorem | fvmptndm 7015* | Value of a function given by the maps-to notation, outside of its domain. (Contributed by AV, 31-Dec-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (¬ 𝑋 ∈ 𝐴 → (𝐹‘𝑋) = ∅) | ||
Theorem | fvmptrabfv 7016* | Value of a function mapping a set to a class abstraction restricting the value of another function. (Contributed by AV, 18-Feb-2022.) |
⊢ 𝐹 = (𝑥 ∈ V ↦ {𝑦 ∈ (𝐺‘𝑥) ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑋) ∣ 𝜓} | ||
Theorem | fvopab5 7017* | The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹‘𝐴) = (℩𝑦𝜓)) | ||
Theorem | fvopab6 7018* | Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝑦 = 𝐵)} & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | eqfnfv 7019* | Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | eqfnfv2 7020* | Equality of functions is determined by their values. Exercise 4 of [TakeutiZaring] p. 28. (Contributed by NM, 3-Aug-1994.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))) | ||
Theorem | eqfnfv3 7021* | Derive equality of functions from equality of their values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥))))) | ||
Theorem | eqfnfvd 7022* | Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | eqfnfv2f 7023* | Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). This version of eqfnfv 7019 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐺 ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | eqfunfv 7024* | Equality of functions is determined by their values. (Contributed by Scott Fenton, 19-Jun-2011.) |
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥)))) | ||
Theorem | fvreseq0 7025* | Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐶) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐶)) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fvreseq1 7026* | Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = 𝐺 ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) | ||
Theorem | fvreseq 7027* | 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 7028* | A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019.) |
⊢ (𝜑 → 𝑀 Fn 𝐴) & ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷)) | ||
Theorem | fndmdif 7029* | Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)}) | ||
Theorem | fndmdifcom 7030 | The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹)) | ||
Theorem | fndmdifeq0 7031 | 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 7032* | Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)}) | ||
Theorem | fneqeql 7033 | Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴)) | ||
Theorem | fneqeql2 7034 | Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) | ||
Theorem | fnreseql 7035 | 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 7036* | 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 7037 | 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 7038 | Two ways to say that 𝐴 is in the domain of 𝐹. (Contributed by Mario Carneiro, 1-May-2014.) |
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴))) | ||
Theorem | fvimacnvi 7039 | A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) | ||
Theorem | fvimacnv 7040 | 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 6621 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | funimass3 7041 | 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 7040 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 7042* | A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | funconstss 7043* | Two ways of specifying that a function is constant on a subdomain. (Contributed by NM, 8-Mar-2007.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
Theorem | fvimacnvALT 7044 | Alternate proof of fvimacnv 7040, based on funimass3 7041. If funimass3 7041 is ever proved directly, as opposed to using funimacnv 6619 pointwise, then the proof of funimacnv 6619 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 7045 | Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) | ||
Theorem | elpreimad 7046 | Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → (𝐹‘𝐵) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ∈ (◡𝐹 “ 𝐶)) | ||
Theorem | fniniseg 7047 | 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 7048* | Inverse images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵}) | ||
Theorem | fniniseg2 7049* | Inverse point images under functions expressed as abstractions. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵}) | ||
Theorem | unpreima 7050 | Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵))) | ||
Theorem | inpreima 7051 | Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jun-2016.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵))) | ||
Theorem | difpreima 7052 | Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵))) | ||
Theorem | respreima 7053 | The preimage of a restricted function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) | ||
Theorem | cnvimainrn 7054 | The preimage of the intersection of the range of a class and a class 𝐴 is the preimage of the class 𝐴. (Contributed by AV, 17-Sep-2024.) |
⊢ (Fun 𝐹 → (◡𝐹 “ (ran 𝐹 ∩ 𝐴)) = (◡𝐹 “ 𝐴)) | ||
Theorem | sspreima 7055 | The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ 𝐵) → (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ 𝐵)) | ||
Theorem | iinpreima 7056* | Preimage of an intersection. (Contributed by FL, 16-Apr-2012.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
Theorem | intpreima 7057* | Preimage of an intersection. (Contributed by FL, 28-Apr-2012.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ ∩ 𝐴) = ∩ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
Theorem | fimacnvOLD 7058 | Obsolete version of fimacnv 6727 as of 20-Sep-2024. (Contributed by FL, 25-Jan-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) | ||
Theorem | fimacnvinrn 7059 | 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 7060 | 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 | rescnvimafod 7061 | The restriction of a function to a preimage of a class is a function onto the intersection of this class and the range of the function. (Contributed by AV, 13-Sep-2024.) (Revised by AV, 29-Sep-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐸 = (ran 𝐹 ∩ 𝐵)) & ⊢ (𝜑 → 𝐷 = (◡𝐹 “ 𝐵)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–onto→𝐸) | ||
Theorem | fvn0ssdmfun 7062* | 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 6922. (Contributed by AV, 27-Jan-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (∀𝑎 ∈ 𝐷 (𝐹‘𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷))) | ||
Theorem | fnopfv 7063 | Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41. (Contributed by NM, 30-Sep-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 〈𝐵, (𝐹‘𝐵)〉 ∈ 𝐹) | ||
Theorem | fvelrn 7064 | A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | nelrnfvne 7065 | 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 7066* | 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 7067* | 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 7068 | A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | ffvelcdm 7069 | A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | fnfvelrnd 7070 | A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | ffvelcdmi 7071 | A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelcdmda 7072 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | ffvelcdmd 7073 | A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵) | ||
Theorem | rexrn 7074* | 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 7075* | 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 7076* | 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 7077* | 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 7078* | 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 7079* | 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 6541 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 6541 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 7080* | 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 7081* | A restricted quantifier over an image set. Version of ralrnmpt 7083 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexrnmptw 7082* | A restricted quantifier over an image set. Version of rexrnmpt 7084 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 20-Aug-2015.) Avoid ax-13 2371. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrnmpt 7083* | A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker ralrnmptw 7081 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexrnmpt 7084* | A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker rexrnmptw 7082 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | f0cli 7085 | Unconditional closure of a function when the codomain includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013.) |
⊢ 𝐹:𝐴⟶𝐵 & ⊢ ∅ ∈ 𝐵 ⇒ ⊢ (𝐹‘𝐶) ∈ 𝐵 | ||
Theorem | dff2 7086 | Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵))) | ||
Theorem | dff3 7087* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) | ||
Theorem | dff4 7088* | Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) | ||
Theorem | dffo3 7089* | An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
Theorem | dffo4 7090* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) | ||
Theorem | dffo5 7091* | Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007.) |
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) | ||
Theorem | exfo 7092* | 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 7093* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foco2 7094 | 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 7095* | Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | f1ompt 7096* | 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 7097* | Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 | ||
Theorem | fvmptelcdm 7098* | The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
Theorem | fmptd 7099* | Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmpttd 7100* | Version of fmptd 7099 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.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |