Home | Metamath
Proof Explorer Theorem List (p. 72 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | resiexd 7101 | The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( I ↾ 𝐵) ∈ V) | ||
Theorem | fnex 7102 | 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 7100. See fnexALT 7802 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | fnexd 7103 | 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 7104 | 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 7102. (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 7105* | Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | mptexg 7106* | 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 7107 | 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 7108* | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7106. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | mptexd 7109* | If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 7106. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptrabex 7110* | 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 7111 | If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | ||
Theorem | fexd 7112 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | mptfvmpt 7113* | A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022.) |
⊢ (𝑦 = 𝑌 → 𝑀 = (𝑥 ∈ 𝑉 ↦ 𝐴)) & ⊢ 𝐺 = (𝑦 ∈ 𝑊 ↦ 𝑀) & ⊢ 𝑉 = (𝐹‘𝑋) ⇒ ⊢ (𝑌 ∈ 𝑊 → (𝐺‘𝑌) = (𝑥 ∈ 𝑉 ↦ 𝐴)) | ||
Theorem | eufnfv 7114* | A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵) | ||
Theorem | funfvima 7115 | A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2 7116 | A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2d 7117 | 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 7118 | 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 7119 | A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐶)) | ||
Theorem | resfvresima 7120 | 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 7121 | 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 7122* | Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ralima 7123* | Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | fvclss 7124* | Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995.) |
⊢ {𝑦 ∣ ∃𝑥 𝑦 = (𝐹‘𝑥)} ⊆ (ran 𝐹 ∪ {∅}) | ||
Theorem | elabrex 7125* | Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | abrexco 7126* | Composition of two image maps 𝐶(𝑦) and 𝐵(𝑤). (Contributed by NM, 27-May-2013.) |
⊢ 𝐵 ∈ V & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} | ||
Theorem | imaiun 7127* | The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶) | ||
Theorem | imauni 7128* | 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 7129* | 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 7130* |
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 7131* | The indexed union of a function's values is the union of its image under the index class. This version of funiunfv 7130 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 7132* | Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐵 ∈ ∪ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn 7133* | Membership in the union of the range of a function. See elunirnALT 7134 for a shorter proof which uses ax-pow 5289. (Contributed by NM, 24-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirnALT 7134* | Alternate proof of elunirn 7133. It is shorter but requires ax-pow 5289 (through eluniima 7132, funiunfv 7130, ndmfv 6813). (Contributed by NM, 24-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn2 7135 | Condition for the membership in the union of the range of a function. (Contributed by Thierry Arnoux, 13-Nov-2016.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (𝐹‘𝐴)) → 𝐵 ∈ ∪ ran 𝐹) | ||
Theorem | fnunirn 7136* | Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐹 Fn 𝐼 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝐼 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | dff13 7137* | 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 7138* | 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 7139 | 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 7140 | 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 7141 | Alternate proof of f1cofveqaeq 7140, 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 7142 | 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 7143* | Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦))) | ||
Theorem | f1fveq 7144 | Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1elima 7145 | Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌)) | ||
Theorem | f1imass 7146 | Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊆ (𝐹 “ 𝐷) ↔ 𝐶 ⊆ 𝐷)) | ||
Theorem | f1imaeq 7147 | Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) = (𝐹 “ 𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1imapss 7148 | Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊊ (𝐹 “ 𝐷) ↔ 𝐶 ⊊ 𝐷)) | ||
Theorem | fpropnf1 7149 | 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 7150 | 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 7151* | The range 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 7152* | 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 7153* | 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 7154 | 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 7155 | 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 7156* | A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1ocnvfv1 7157 | The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv2 7158 | The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv 7159 | 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 7160 | 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 7161 | An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | nvocnv 7162* | The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019.) |
⊢ ((𝐹:𝐴⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥) → ◡𝐹 = 𝐹) | ||
Theorem | f1cdmsn 7163* | 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 7164* | Relate a function with a singleton as domain and one variable. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 𝜓)) | ||
Theorem | f1prex 7165* | 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 7166 | 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 7167 | 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 7168 | 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 7169 | 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 7170* | 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 7171* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) |
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | cocan1 7172 | An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐻:𝐴⟶𝐵 ∧ 𝐾:𝐴⟶𝐵) → ((𝐹 ∘ 𝐻) = (𝐹 ∘ 𝐾) ↔ 𝐻 = 𝐾)) | ||
Theorem | cocan2 7173 | A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐻 Fn 𝐵 ∧ 𝐾 Fn 𝐵) → ((𝐻 ∘ 𝐹) = (𝐾 ∘ 𝐹) ↔ 𝐻 = 𝐾)) | ||
Theorem | fcof1oinvd 7174 | Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o 7177. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | fcof1od 7175 | A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 7168 and fcofo 7169. Formerly part of proof of fcof1o 7177. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | 2fcoidinvd 7176 | 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 7177 | 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 7178* | 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 7179* | A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | 2fvidinvd 7180* | 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.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | foeqcnvco 7181 | Condition for function equality in terms of vanishing of the composition with the converse. EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) | ||
Theorem | f1eqcocnv 7182 | Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Proof shortened by Wolf Lammen, 29-May-2024.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴))) | ||
Theorem | f1eqcocnvOLD 7183 | Obsolete version of f1eqcocnv 7182 as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴))) | ||
Theorem | fveqf1o 7184 | Given a bijection 𝐹, produce another bijection 𝐺 which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐺 = (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝐶, (◡𝐹‘𝐷)})) ∪ {〈𝐶, (◡𝐹‘𝐷)〉, 〈(◡𝐹‘𝐷), 𝐶〉})) ⇒ ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐺:𝐴–1-1-onto→𝐵 ∧ (𝐺‘𝐶) = 𝐷)) | ||
Theorem | nf1const 7185 | A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1→𝐶) | ||
Theorem | nf1oconst 7186 | A constant function from at least two elements is not bijective. (Contributed by AV, 30-Mar-2024.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1-onto→𝐶) | ||
Theorem | f1ofvswap 7187 | Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵) | ||
Theorem | fliftrel 7188* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆)) | ||
Theorem | fliftel 7189* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵))) | ||
Theorem | fliftel1 7190* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵) | ||
Theorem | fliftcnv 7191* | Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ◡𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐵, 𝐴〉)) | ||
Theorem | fliftfun 7192* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷))) | ||
Theorem | fliftfund 7193* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶)) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | fliftfuns 7194* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) | ||
Theorem | fliftf 7195* | The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆)) | ||
Theorem | fliftval 7196* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷) | ||
Theorem | isoeq1 7197 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) | ||
Theorem | isoeq2 7198 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵))) | ||
Theorem | isoeq3 7199 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵))) | ||
Theorem | isoeq4 7200 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |