![]() |
Metamath
Proof Explorer Theorem List (p. 73 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fvtp1g 7201 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷) | ||
Theorem | fvtp2g 7202 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸) | ||
Theorem | fvtp3g 7203 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹) | ||
Theorem | tpres 7204 | 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 7205 | The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2g 7206 | A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007.) |
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))) | ||
Theorem | fvconst2 7207 | The value of a constant function. (Contributed by NM, 16-Apr-2005.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2 7208 | A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | fconst5 7209 | Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅) → (𝐹 = (𝐴 × {𝐵}) ↔ ran 𝐹 = {𝐵})) | ||
Theorem | rnmptc 7210* | 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 7211* | Obsolete version of rnmptc 7210 as of 17-Apr-2024. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ran 𝐹 = {𝐵}) | ||
Theorem | fnprb 7212 | 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 7213 | 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 7214 | 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 7215 | A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹:{𝐴, 𝐵}⟶𝐶 ↔ ((𝐹‘𝐴) ∈ 𝐶 ∧ (𝐹‘𝐵) ∈ 𝐶 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}))) | ||
Theorem | fconstfv 7216* | A constant function expressed in terms of its functionality, domain, and value. See also fconst2 7208. (Contributed by NM, 27-Aug-2004.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) | ||
Theorem | fconst3 7217 | Two ways to express a constant function. (Contributed by NM, 15-Mar-2007.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) | ||
Theorem | fconst4 7218 | Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.) |
⊢ (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴)) | ||
Theorem | resfunexg 7219 | The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.) |
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) | ||
Theorem | resiexd 7220 | The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V) | ||
Theorem | fnex 7221 | If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 7219. See fnexALT 7941 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | fnexd 7222 | If the domain of a function is a set, the function is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | funex 7223 | If the domain of a function exists, so does the function. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex 7221. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.) (Contributed by NM, 11-Nov-1995.) |
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | opabex 7224* | Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | mptexg 7225* | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptexgf 7226 | If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) (Revised by Thierry Arnoux, 17-May-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptex 7227* | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7225. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | mptexd 7228* | If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7225. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptrabex 7229* | If the domain of a function given by maps-to notation is a class abstraction based on a set, the function is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↦ 𝐵) ∈ V | ||
Theorem | fex 7230 | If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | ||
Theorem | fexd 7231 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | mptfvmpt 7232* | A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022.) |
⊢ (𝑦 = 𝑌 → 𝑀 = (𝑥 ∈ 𝑉 ↦ 𝐴)) & ⊢ 𝐺 = (𝑦 ∈ 𝑊 ↦ 𝑀) & ⊢ 𝑉 = (𝐹‘𝑋) ⇒ ⊢ (𝑌 ∈ 𝑊 → (𝐺‘𝑌) = (𝑥 ∈ 𝑉 ↦ 𝐴)) | ||
Theorem | eufnfv 7233* | A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵) | ||
Theorem | funfvima 7234 | A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2 7235 | A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2d 7236 | A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.) (Revised by AV, 23-Mar-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ (𝐹 “ 𝐴)) | ||
Theorem | fnfvima 7237 | The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)) | ||
Theorem | fnfvimad 7238 | A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐶)) | ||
Theorem | resfvresima 7239 | The value of the function value of a restriction for a function restricted to the image of the restricting subset. (Contributed by AV, 6-Mar-2021.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑆 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐻 ↾ (𝐹 “ 𝑆))‘((𝐹 ↾ 𝑆)‘𝑋)) = (𝐻‘(𝐹‘𝑋))) | ||
Theorem | funfvima3 7240 | A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ 𝐺) → (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) ∈ (𝐺 “ {𝐴}))) | ||
Theorem | rexima 7241* | Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ralima 7242* | Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | fvclss 7243* | Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.) |
⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ⊆ (ran 𝐹 ∪ {∅}) | ||
Theorem | elabrex 7244* | Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | elabrexg 7245* | Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | abrexco 7246* | Composition of two image maps 𝐶(𝑦) and 𝐵(𝑤). (Contributed by NM, 27-May-2013.) |
⊢ 𝐵 ∈ V & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} | ||
Theorem | imaiun 7247* | The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶) | ||
Theorem | imauni 7248* | The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (Contributed by NM, 9-Aug-2004.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝑥) | ||
Theorem | fniunfv 7249* | The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹) | ||
Theorem | funiunfv 7250* |
The indexed union of a function's values is the union of its image under
the index class.
Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to 𝐹 Fn 𝐴, the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) | ||
Theorem | funiunfvf 7251* | The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 7250 uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006.) (Revised by David Abernethy, 15-Apr-2013.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) | ||
Theorem | eluniima 7252* | Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐵 ∈ ∪ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn 7253* | Membership in the union of the range of a function. See elunirnALT 7254 for a shorter proof which uses ax-pow 5363. See elfvunirn 6923 for a more general version of the reverse direction. (Contributed by NM, 24-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirnALT 7254* | Alternate proof of elunirn 7253. It is shorter but requires ax-pow 5363 (through eluniima 7252, funiunfv 7250, ndmfv 6926). (Contributed by NM, 24-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn2OLD 7255 | Obsolete version of elfvunirn 6923 as of 12-Jan-2025. (Contributed by Thierry Arnoux, 13-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (𝐹‘𝐴)) → 𝐵 ∈ ∪ ran 𝐹) | ||
Theorem | fnunirn 7256* | Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐹 Fn 𝐼 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝐼 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | dff13 7257* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | dff13f 7258* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 31-Jul-2003.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐹 ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1veqaeq 7259 | If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
Theorem | f1cofveqaeq 7260 | If the values of a composition of one-to-one functions for two arguments are equal, the arguments themselves must be equal. (Contributed by AV, 3-Feb-2021.) |
⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐹‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑌)) → 𝑋 = 𝑌)) | ||
Theorem | f1cofveqaeqALT 7261 | Alternate proof of f1cofveqaeq 7260, 1 essential step shorter, but having more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐹‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑌)) → 𝑋 = 𝑌)) | ||
Theorem | 2f1fvneq 7262 | If two one-to-one functions are applied on different arguments, also the values are different. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌)) | ||
Theorem | f1mpt 7263* | Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦))) | ||
Theorem | f1fveq 7264 | Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1elima 7265 | Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌)) | ||
Theorem | f1imass 7266 | Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊆ (𝐹 “ 𝐷) ↔ 𝐶 ⊆ 𝐷)) | ||
Theorem | f1imaeq 7267 | Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) = (𝐹 “ 𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1imapss 7268 | Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊊ (𝐹 “ 𝐷) ↔ 𝐶 ⊊ 𝐷)) | ||
Theorem | fpropnf1 7269 | A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) |
⊢ 𝐹 = {⟨𝑋, 𝑍⟩, ⟨𝑌, 𝑍⟩} ⇒ ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑋 ≠ 𝑌) → (Fun 𝐹 ∧ ¬ Fun ◡𝐹)) | ||
Theorem | f1dom3fv3dif 7270 | The function values for a 1-1 function from a set with three different elements are different. (Contributed by AV, 20-Mar-2019.) |
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ (𝐹‘𝐶) ∧ (𝐹‘𝐵) ≠ (𝐹‘𝐶))) | ||
Theorem | f1dom3el3dif 7271* | The codomain of a 1-1 function from a set with three different elements has (at least) three different elements. (Contributed by AV, 20-Mar-2019.) |
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 ∃𝑧 ∈ 𝑅 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧)) | ||
Theorem | dff14a 7272* | A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → (𝐹‘𝑥) ≠ (𝐹‘𝑦)))) | ||
Theorem | dff14b 7273* | A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))) | ||
Theorem | f12dfv 7274 | A one-to-one function with a domain with at least two different elements in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ 𝐴 = {𝑋, 𝑌} ⇒ ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))) | ||
Theorem | f13dfv 7275 | A one-to-one function with a domain with at least three different elements in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018.) |
⊢ 𝐴 = {𝑋, 𝑌, 𝑍} ⇒ ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))) | ||
Theorem | dff1o6 7276* | A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1ocnvfv1 7277 | The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv2 7278 | The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv 7279 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶)) | ||
Theorem | f1ocnvfvb 7280 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐹‘𝐶) = 𝐷 ↔ (◡𝐹‘𝐷) = 𝐶)) | ||
Theorem | nvof1o 7281 | An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | nvocnv 7282* | The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019.) |
⊢ ((𝐹:𝐴⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥) → ◡𝐹 = 𝐹) | ||
Theorem | f1cdmsn 7283* | If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024.) |
⊢ ((𝐹:𝐴–1-1→{𝐵} ∧ 𝐴 ≠ ∅) → ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | fsnex 7284* | Relate a function with a singleton as domain and one variable. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 𝜓)) | ||
Theorem | f1prex 7285* | Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))) | ||
Theorem | f1ocnvdm 7286 | The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) | ||
Theorem | f1ocnvfvrneq 7287 | If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹)) → ((◡𝐹‘𝐶) = (◡𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
Theorem | fcof1 7288 | An application is injective if a retraction exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 11-Nov-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑅 ∘ 𝐹) = ( I ↾ 𝐴)) → 𝐹:𝐴–1-1→𝐵) | ||
Theorem | fcofo 7289 | An application is surjective if a section exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 17-Nov-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆:𝐵⟶𝐴 ∧ (𝐹 ∘ 𝑆) = ( I ↾ 𝐵)) → 𝐹:𝐴–onto→𝐵) | ||
Theorem | cbvfo 7290* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | cbvexfo 7291* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) |
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | cocan1 7292 | An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐻:𝐴⟶𝐵 ∧ 𝐾:𝐴⟶𝐵) → ((𝐹 ∘ 𝐻) = (𝐹 ∘ 𝐾) ↔ 𝐻 = 𝐾)) | ||
Theorem | cocan2 7293 | A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐻 Fn 𝐵 ∧ 𝐾 Fn 𝐵) → ((𝐻 ∘ 𝐹) = (𝐾 ∘ 𝐹) ↔ 𝐻 = 𝐾)) | ||
Theorem | fcof1oinvd 7294 | Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o 7297. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | fcof1od 7295 | A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 7288 and fcofo 7289. Formerly part of proof of fcof1o 7297. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | 2fcoidinvd 7296 | Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | fcof1o 7297 | Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by AV, 15-Dec-2019.) |
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ 𝐵) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = 𝐺)) | ||
Theorem | 2fvcoidd 7298* | Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) | ||
Theorem | 2fvidf1od 7299* | A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | 2fvidinvd 7300* | Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |