P. 83 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	suppsnop 8201	The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐹 = {⟨𝑋, 𝑌⟩}    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋}))
Theorem	snopsuppss 8202	The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019.)
⊢ ({⟨𝑋, 𝑌⟩} supp 𝑍) ⊆ {𝑋}
Theorem	fvn0elsupp 8203	If the function value for a given argument is not empty, the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 2-Jul-2019.) (Revised by AV, 4-Apr-2020.)
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ (𝐺 Fn 𝐵 ∧ (𝐺‘𝑋) ≠ ∅)) → 𝑋 ∈ (𝐺 supp ∅))
Theorem	fvn0elsuppb 8204	The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵) → ((𝐺‘𝑋) ≠ ∅ ↔ 𝑋 ∈ (𝐺 supp ∅)))
Theorem	rexsupp 8205*	Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∃𝑥 ∈ (𝐹 supp 𝑍)𝜑 ↔ ∃𝑥 ∈ 𝑋 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑)))
Theorem	ressuppss 8206	The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐹 ↾ 𝐵) supp 𝑍) ⊆ (𝐹 supp 𝑍))
Theorem	suppun 8207	The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019.)
⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍))
Theorem	ressuppssdif 8208	The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) ⊆ (((𝐹 ↾ 𝐵) supp 𝑍) ∪ (dom 𝐹 ∖ 𝐵)))
Theorem	mptsuppdifd 8209*	The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})})
Theorem	mptsuppd 8210*	The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍})
Theorem	extmptsuppeq 8211*	The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 30-Jun-2019.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐵 ∖ 𝐴)) → 𝑋 = 𝑍)    ⇒   ⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍))
Theorem	suppfnss 8212*	The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 6-Jun-2022.)
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)))
Theorem	funsssuppss 8213	The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.)
⊢ ((Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))
Theorem	fnsuppres 8214	Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.)
⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ (𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 supp 𝑍) ⊆ 𝐴 ↔ (𝐹 ↾ 𝐵) = (𝐵 × {𝑍})))
Theorem	fnsuppeq0 8215	The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 28-May-2019.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) → ((𝐹 supp 𝑍) = ∅ ↔ 𝐹 = (𝐴 × {𝑍})))
Theorem	fczsupp0 8216	The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.)
⊢ ((𝐵 × {𝑍}) supp 𝑍) = ∅
Theorem	suppss 8217*	Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) (Proof shortened by SN, 5-Aug-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)
Theorem	suppssr 8218	A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍)
Theorem	suppssrg 8219	A function is zero outside its support. Version of suppssr 8218 avoiding ax-rep 5284 by assuming 𝐹 is a set rather than its domain 𝐴. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍)
Theorem	suppssov1 8220*	Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) (Proof shortened by SN, 11-Apr-2025.)
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)
Theorem	suppssov2 8221*	Formula building theorem for support restrictions: operator with right annihilator. (Contributed by SN, 11-Apr-2025.)
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐵) supp 𝑌) ⊆ 𝐿)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑣𝑂𝑌) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)
Theorem	suppssof1 8222*	Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.)
⊢ (𝜑 → (𝐴 supp 𝑌) ⊆ 𝐿)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ⊢ (𝜑 → 𝐴:𝐷⟶𝑉)    &   ⊢ (𝜑 → 𝐵:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 ∘f 𝑂𝐵) supp 𝑍) ⊆ 𝐿)
Theorem	suppss2 8223*	Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.)
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)
Theorem	suppsssn 8224*	Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊) → 𝐵 = 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ {𝑊})
Theorem	suppssfv 8225*	Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.)
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿)    &   ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿)
Theorem	suppofssd 8226	Condition for the support of a function operation to be a subset of the union of the supports of the left and right function terms. (Contributed by Steven Nguyen, 28-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝑍𝑋𝑍) = 𝑍)    ⇒   ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍)))
Theorem	suppofss1d 8227*	Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑍𝑋𝑥) = 𝑍)    ⇒   ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍))
Theorem	suppofss2d 8228*	Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥𝑋𝑍) = 𝑍)    ⇒   ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑍))
Theorem	suppco 8229	The support of the composition of two functions is the inverse image by the inner function of the support of the outer function. (Contributed by AV, 30-May-2019.) Extract this statement from the proof of supp0cosupp0 8231. (Revised by SN, 15-Sep-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍)))
Theorem	suppcoss 8230	The support of the composition of two functions is a subset of the support of the inner function if the outer function preserves zero. Compare suppssfv 8225, which has a sethood condition on 𝐴 instead of 𝐵. (Contributed by SN, 25-May-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍)    ⇒   ⊢ (𝜑 → ((𝐹 ∘ 𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑌))
Theorem	supp0cosupp0 8231	The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 supp 𝑍) = ∅ → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅))
Theorem	imacosupp 8232	The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍)))
2.4.13  Special maps-to operations The following theorems are about maps-to operations (see df-mpo 7435) where the domain of the second argument depends on the domain of the first argument, especially when the first argument is a pair and the base set of the second argument is the first component of the first argument, in short "x-maps-to operations". For labels, the abbreviations "mpox" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpox 7525, ovmpox 7585 and fmpox 8090). If the first argument is an ordered pair, as in the following, the abbreviation is extended to "mpoxop", and the maps-to operations are called "x-op maps-to operations" for short.
Theorem	opeliunxp2f 8233*	Membership in a union of Cartesian products, using bound-variable hypothesis for 𝐸 instead of distinct variable conditions as in opeliunxp2 5851. (Contributed by AV, 25-Oct-2020.)
⊢ Ⅎ𝑥𝐸    &   ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸)    ⇒   ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))
Theorem	mpoxeldm 8234*	If there is an element of the value of an operation given by a maps-to rule, then the first argument is an element of the first component of the domain and the second argument is an element of the second component of the domain depending on the first argument. (Contributed by AV, 25-Oct-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐷))
Theorem	mpoxneldm 8235*	If the first argument of an operation given by a maps-to rule is not an element of the first component of the domain or the second argument is not an element of the second component of the domain depending on the first argument, then the value of the operation is the empty set. (Contributed by AV, 25-Oct-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)    ⇒   ⊢ ((𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋𝑋 / 𝑥⦌𝐷) → (𝑋𝐹𝑌) = ∅)
Theorem	mpoxopn0yelv 8236*	If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊⟩𝐹𝐾) → 𝐾 ∈ 𝑉))
Theorem	mpoxopynvov0g 8237*	If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∉ 𝑉) → (⟨𝑉, 𝑊⟩𝐹𝐾) = ∅)
Theorem	mpoxopxnop0 8238*	If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ (¬ 𝑉 ∈ (V × V) → (𝑉𝐹𝐾) = ∅)
Theorem	mpoxopx0ov0 8239*	If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ (∅𝐹𝐾) = ∅
Theorem	mpoxopxprcov0 8240*	If the components of the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ (¬ (𝑉 ∈ V ∧ 𝑊 ∈ V) → (⟨𝑉, 𝑊⟩𝐹𝐾) = ∅)
Theorem	mpoxopynvov0 8241*	If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ (𝐾 ∉ 𝑉 → (⟨𝑉, 𝑊⟩𝐹𝐾) = ∅)
Theorem	mpoxopoveq 8242*	Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑})    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∈ 𝑉) → (⟨𝑉, 𝑊⟩𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑})
Theorem	mpoxopovel 8243*	Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑})    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊⟩𝐹𝐾) ↔ (𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦][𝑁 / 𝑛]𝜑)))
Theorem	mpoxopoveqd 8244*	Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑})    &   ⊢ (𝜓 → (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌))    &   ⊢ ((𝜓 ∧ ¬ 𝐾 ∈ 𝑉) → {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑} = ∅)    ⇒   ⊢ (𝜓 → (⟨𝑉, 𝑊⟩𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑})
Theorem	brovex 8245*	A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.)
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶)    &   ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Rel (𝑉𝑂𝐸))    ⇒   ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
Theorem	brovmpoex 8246*	A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.)
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑧, 𝑤⟩ ∣ 𝜑})    ⇒   ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
Theorem	sprmpod 8247*	The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 20-Jun-2019.)
⊢ 𝑀 = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑣𝑅𝑒)𝑦 ∧ 𝜒)})    &   ⊢ ((𝜑 ∧ 𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → (𝑉 ∈ V ∧ 𝐸 ∈ V))    &   ⊢ (𝜑 → ∀𝑥∀𝑦(𝑥(𝑉𝑅𝐸)𝑦 → 𝜃))    &   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜃} ∈ V)    ⇒   ⊢ (𝜑 → (𝑉𝑀𝐸) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑉𝑅𝐸)𝑦 ∧ 𝜓)})
2.4.14  Function transposition
Syntax	ctpos 8248	The transposition of a function.
class tpos 𝐹
Definition	df-tpos 8249*	Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
Theorem	tposss 8250	Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺)
Theorem	tposeq 8251	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺)
Theorem	tposeqd 8252	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺)
Theorem	tposssxp 8253	The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹)
Theorem	reltpos 8254	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Rel tpos 𝐹
Theorem	brtpos2 8255	Value of the transposition at an ordered pair ⟨𝐴, 𝐵⟩. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵)))
Theorem	brtpos0 8256	The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows to eliminate sethood hypotheses on 𝐴, 𝐵 in brtpos 8258. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴))
Theorem	reldmtpos 8257	Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹)
Theorem	brtpos 8258	The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐶 ∈ 𝑉 → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶))
Theorem	ottpos 8259	The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ (𝐶 ∈ 𝑉 → (⟨𝐴, 𝐵, 𝐶⟩ ∈ tpos 𝐹 ↔ ⟨𝐵, 𝐴, 𝐶⟩ ∈ 𝐹))
Theorem	relbrtpos 8260	The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015.)
⊢ (Rel 𝐹 → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶))
Theorem	dmtpos 8261	The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹)
Theorem	rntpos 8262	The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Theorem	tposexg 8263	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V)
Theorem	ovtpos 8264	The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from (1...𝑚) × (1...𝑛) to ℝ or some ring, tpos 𝐹 is the transposition of 𝐹, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐴tpos 𝐹𝐵) = (𝐵𝐹𝐴)
Theorem	tposfun 8265	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Fun 𝐹 → Fun tpos 𝐹)
Theorem	dftpos2 8266*	Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})))
Theorem	dftpos3 8267*	Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 5696. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨𝑦, 𝑥⟩𝐹𝑧})
Theorem	dftpos4 8268*	Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
Theorem	tpostpos 8269	Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V))
Theorem	tpostpos2 8270	Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹)
Theorem	tposfn2 8271	The domain of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴))
Theorem	tposfo2 8272	Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵))
Theorem	tposf2 8273	The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵))
Theorem	tposf12 8274	Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵))
Theorem	tposf1o2 8275	Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 → tpos 𝐹:◡𝐴–1-1-onto→𝐵))
Theorem	tposfo 8276	The domain and codomain/range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–onto→𝐶)
Theorem	tposf 8277	The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → tpos 𝐹:(𝐵 × 𝐴)⟶𝐶)
Theorem	tposfn 8278	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → tpos 𝐹 Fn (𝐵 × 𝐴))
Theorem	tpos0 8279	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
⊢ tpos ∅ = ∅
Theorem	tposco 8280	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺)
Theorem	tpossym 8281*	Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (𝐴 × 𝐴) → (tpos 𝐹 = 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝐹𝑦) = (𝑦𝐹𝑥)))
Theorem	tposeqi 8282	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ tpos 𝐹 = tpos 𝐺
Theorem	tposex 8283	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 ∈ V    ⇒   ⊢ tpos 𝐹 ∈ V
Theorem	nftpos 8284	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥tpos 𝐹
Theorem	tposoprab 8285*	Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ tpos 𝐹 = {⟨⟨𝑦, 𝑥⟩, 𝑧⟩ ∣ 𝜑}
Theorem	tposmpo 8286*	Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ tpos 𝐹 = (𝑦 ∈ 𝐵, 𝑥 ∈ 𝐴 ↦ 𝐶)
Theorem	tposconst 8287	The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018.)
⊢ tpos ((𝐴 × 𝐵) × {𝐶}) = ((𝐵 × 𝐴) × {𝐶})
2.4.15  Curry and uncurry
Syntax	ccur 8288	Extend class notation to include the currying function.
class curry 𝐴
Syntax	cunc 8289	Extend class notation to include the uncurrying function.
class uncurry 𝐴
Definition	df-cur 8290*	Define the currying of 𝐹, which splits a function of two arguments into a function of the first argument, producing a function over the second argument. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧})
Definition	df-unc 8291*	Define the uncurrying of 𝐹, which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧}
Theorem	mpocurryd 8292*	The currying of an operation given in maps-to notation, splitting the operation (function of two arguments) into a function of the first argument, producing a function over the second argument. (Contributed by AV, 27-Oct-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    ⇒   ⊢ (𝜑 → curry 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)))
Theorem	mpocurryvald 8293*	The value of a curried operation given in maps-to notation is a function over the second argument of the original operation. (Contributed by AV, 27-Oct-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ≠ ∅)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (curry 𝐹‘𝐴) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	fvmpocurryd 8294*	The value of the value of a curried operation given in maps-to notation is the operation value of the original operation. (Contributed by AV, 27-Oct-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵))
2.4.16  Undefined values
Syntax	cund 8295	Extend class notation with undefined value function.
class Undef
Definition	df-undef 8296	Define the undefined value function, whose value at set 𝑠 is guaranteed not to be a member of 𝑠 (see pwuninel 8298). (Contributed by NM, 15-Sep-2011.)
⊢ Undef = (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠)
Theorem	pwuninel2 8297	Proof of pwuninel 8298 under the assumption that the union of the given class is a set, avoiding ax-pr 5437 and ax-un 7753. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴)
Theorem	pwuninel 8298	The powerclass of the union of a class does not belong to that class. This theorem provides a way of constructing a new set that does not belong to a given set. See also pwuninel2 8297. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ ¬ 𝒫 ∪ 𝐴 ∈ 𝐴
Theorem	undefval 8299	Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 8301 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) = 𝒫 ∪ 𝑆)
Theorem	undefnel2 8300	The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.)
⊢ (𝑆 ∈ 𝑉 → ¬ (Undef‘𝑆) ∈ 𝑆)