P. 80 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfopab2 7901*	A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∈ (V × V) ∣ [(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑}
Theorem	dfoprab3s 7902*	A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ [(1st ‘𝑤) / 𝑥][(2nd ‘𝑤) / 𝑦]𝜑)}
Theorem	dfoprab3 7903*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.)
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (V × V) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
Theorem	dfoprab4 7904*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}
Theorem	dfoprab4f 7905*	Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝜑)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}
Theorem	opabex2 7906*	Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑦 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ∈ V)
Theorem	opabn1stprc 7907*	An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020.)
⊢ (∃𝑦𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∉ V)
Theorem	opiota 7908*	The property of a uniquely specified ordered pair. The proof uses properties of the ℩ description binder. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ 𝐼 = (℩𝑧∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))    &   ⊢ 𝑋 = (1st ‘𝐼)    &   ⊢ 𝑌 = (2nd ‘𝐼)    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐷 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃!𝑧∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝜒) ↔ (𝐶 = 𝑋 ∧ 𝐷 = 𝑌)))
Theorem	cnvoprab 7909*	The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof shortened by Thierry Arnoux, 20-Feb-2022.)
⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜑))    &   ⊢ (𝜓 → 𝑎 ∈ (V × V))    ⇒   ⊢ ◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑧, 𝑎⟩ ∣ 𝜓}
Theorem	dfxp3 7910*	Define the Cartesian product of three classes. Compare df-xp 5596. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.)
⊢ ((𝐴 × 𝐵) × 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)}
Theorem	elopabi 7911*	A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = (1st ‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = (2nd ‘𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝜒)
Theorem	eloprabi 7912*	A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = (1st ‘(1st ‘𝐴)) → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = (2nd ‘(1st ‘𝐴)) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = (2nd ‘𝐴) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝐴 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → 𝜃)
Theorem	mpomptsx 7913*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶)
Theorem	mpompts 7914*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶)
Theorem	dmmpossx 7915*	The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
Theorem	fmpox 7916*	Functionality, domain and codomain of a class given by the maps-to notation, where 𝐵(𝑥) is not constant but depends on 𝑥. (Contributed by NM, 29-Dec-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷)
Theorem	fmpo 7917*	Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
Theorem	fnmpo 7918*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn (𝐴 × 𝐵))
Theorem	fnmpoi 7919*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ 𝐹 Fn (𝐴 × 𝐵)
Theorem	dmmpo 7920*	Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ dom 𝐹 = (𝐴 × 𝐵)
Theorem	ovmpoelrn 7921*	An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) ∈ 𝑀)
Theorem	dmmpoga 7922*	Domain of an operation given by the maps-to notation, closed form of dmmpo 7920. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵))
Theorem	dmmpogaOLD 7923*	Obsolete version of dmmpoga 7922 as of 29-May-2024. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵))
Theorem	dmmpog 7924*	Domain of an operation given by the maps-to notation, closed form of dmmpo 7920. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵))
Theorem	mpoexxg 7925*	Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	mpoexg 7926*	Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	mpoexga 7927*	If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
Theorem	mpoexw 7928*	Weak version of mpoex 7929 that holds without ax-rep 5210. If the domain and codomain of an operation given by maps-to notation are sets, the operation is a set. (Contributed by Rohan Ridenour, 14-Aug-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V
Theorem	mpoex 7929*	If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V
Theorem	mptmpoopabbrd 7930*	The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) Add disjoint variable condition on 𝐷, 𝑓, ℎ to remove hypotheses. (Revised by SN, 13-Dec-2024.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺))    &   ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃))    &   ⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏))    &   ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}))    ⇒   ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)})
Theorem	mptmpoopabovd 7931*	The operation value of a function value of a collection of ordered pairs of related elements. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) Add disjoint variable condition on 𝐷, 𝑓, ℎ to remove hypotheses. (Revised by SN, 13-Dec-2024.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺))    &   ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝑓(𝑎(𝐶‘𝑔)𝑏)ℎ ∧ 𝑓(𝐷‘𝑔)ℎ)}))    ⇒   ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝑓(𝑋(𝐶‘𝐺)𝑌)ℎ ∧ 𝑓(𝐷‘𝐺)ℎ)})
Theorem	mptmpoopabbrdOLD 7932*	Obsolete version of mptmpoopabbrd 7930 as of 13-Dec-2024. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺))    &   ⊢ (𝜑 → {⟨𝑓, ℎ⟩ ∣ 𝜓} ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓)    &   ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃))    &   ⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏))    &   ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}))    ⇒   ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)})
Theorem	mptmpoopabovdOLD 7933*	Obsolete version of mptmpoopabovd 7931 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺))    &   ⊢ (𝜑 → {⟨𝑓, ℎ⟩ ∣ 𝜓} ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑓(𝐷‘𝐺)ℎ) → 𝜓)    &   ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝑓(𝑎(𝐶‘𝑔)𝑏)ℎ ∧ 𝑓(𝐷‘𝑔)ℎ)}))    ⇒   ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝑓(𝑋(𝐶‘𝐺)𝑌)ℎ ∧ 𝑓(𝐷‘𝐺)ℎ)})
Theorem	el2mpocsbcl 7934*	If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.)
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐸))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ ⦋𝑋 / 𝑥⦌⦋𝑌 / 𝑦⦌𝐶 ∧ 𝑇 ∈ ⦋𝑋 / 𝑥⦌⦋𝑌 / 𝑦⦌𝐷))))
Theorem	el2mpocl 7935*	If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. Using implicit substitution. (Contributed by AV, 21-May-2021.)
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑠 ∈ 𝐶, 𝑡 ∈ 𝐷 ↦ 𝐸))    &   ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝐶 = 𝐹 ∧ 𝐷 = 𝐺))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑆 ∈ 𝐹 ∧ 𝑇 ∈ 𝐺))))
Theorem	fnmpoovd 7936*	A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) (Revised by AV, 3-Jul-2022.)
⊢ (𝜑 → 𝑀 Fn (𝐴 × 𝐵))    &   ⊢ ((𝑖 = 𝑎 ∧ 𝑗 = 𝑏) → 𝐷 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) → 𝐷 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐵 (𝑖𝑀𝑗) = 𝐷))
Theorem	offval22 7937*	The function operation expressed as a mapping, variation of offval2 7562. (Contributed by SO, 15-Jul-2018.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷)))
Theorem	brovpreldm 7938	If a binary relation holds for the result of an operation, the operands are in the domain of the operation. (Contributed by AV, 31-Dec-2020.)
⊢ (𝐷(𝐵𝐴𝐶)𝐸 → ⟨𝐵, 𝐶⟩ ∈ dom 𝐴)
Theorem	bropopvvv 7939*	If a binary relation holds for the result of an operation which is a result of an operation, the involved classes are sets. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Proof shortened by AV, 3-Jan-2021.)
⊢ 𝑂 = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ 𝜑}))    &   ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜑 ↔ 𝜓))    &   ⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉𝑂𝐸)𝐵) = {⟨𝑓, 𝑝⟩ ∣ 𝜃})    ⇒   ⊢ (𝐹(𝐴(𝑉𝑂𝐸)𝐵)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)))
Theorem	bropfvvvvlem 7940*	Lemma for bropfvvvv 7941. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))    &   ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})    ⇒   ⊢ ((⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))
Theorem	bropfvvvv 7941*	If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))    &   ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})    &   ⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆)    &   ⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇)    &   ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))
Theorem	ovmptss 7942*	If all the values of the mapping are subsets of a class 𝑋, then so is any evaluation of the mapping. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ⊆ 𝑋 → (𝐸𝐹𝐺) ⊆ 𝑋)
Theorem	relmpoopab 7943*	Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨𝑧, 𝑤⟩ ∣ 𝜑})    ⇒   ⊢ Rel (𝐶𝐹𝐷)
Theorem	fmpoco 7944*	Composition of two functions. Variation of fmptco 7010 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆))    &   ⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇))
Theorem	oprabco 7945*	Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 26-Sep-2015.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐷)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐻‘𝐶))    ⇒   ⊢ (𝐻 Fn 𝐷 → 𝐺 = (𝐻 ∘ 𝐹))
Theorem	oprab2co 7946*	Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑅)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨𝐶, 𝐷⟩)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑀𝐷))    ⇒   ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹))
Theorem	df1st2 7947*	An alternate possible definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑥} = (1st ↾ (V × V))
Theorem	df2nd2 7948*	An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑧 = 𝑦} = (2nd ↾ (V × V))
Theorem	1stconst 7949	The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐵 ∈ 𝑉 → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–1-1-onto→𝐴)
Theorem	2ndconst 7950	The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ∈ 𝑉 → (2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–1-1-onto→𝐵)
Theorem	dfmpo 7951*	Alternate definition for the maps-to notation df-mpo 7289 (although it requires that 𝐶 be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 {⟨⟨𝑥, 𝑦⟩, 𝐶⟩}
Theorem	mposn 7952*	An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019.)
⊢ 𝐹 = (𝑥 ∈ {𝐴}, 𝑦 ∈ {𝐵} ↦ 𝐶)    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑦 = 𝐵 → 𝐷 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈) → 𝐹 = {⟨⟨𝐴, 𝐵⟩, 𝐸⟩})
Theorem	curry1 7953*	Composition with ◡(2nd ↾ ({𝐶} × V)) turns any binary operation 𝐹 with a constant first operand into a function 𝐺 of the second operand only. This transformation is called "currying". (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.)
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)))
Theorem	curry1val 7954	The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴) → (𝐺‘𝐷) = (𝐶𝐹𝐷))
Theorem	curry1f 7955	Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))    ⇒   ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐴) → 𝐺:𝐵⟶𝐷)
Theorem	curry2 7956*	Composition with ◡(1st ↾ (V × {𝐶})) turns any binary operation 𝐹 with a constant second operand into a function 𝐺 of the first operand only. This transformation is called "currying". (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)))
Theorem	curry2f 7957	Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐵) → 𝐺:𝐴⟶𝐷)
Theorem	curry2val 7958	The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝐺‘𝐷) = (𝐷𝐹𝐶))
Theorem	cnvf1olem 7959	Lemma for cnvf1o 7960. (Contributed by Mario Carneiro, 27-Apr-2014.)
⊢ ((Rel 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (𝐶 ∈ ◡𝐴 ∧ 𝐵 = ∪ ◡{𝐶}))
Theorem	cnvf1o 7960*	Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.)
⊢ (Rel 𝐴 → (𝑥 ∈ 𝐴 ↦ ∪ ◡{𝑥}):𝐴–1-1-onto→◡𝐴)
Theorem	fparlem1 7961	Lemma for fpar 7965. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (◡(1st ↾ (V × V)) “ {𝑥}) = ({𝑥} × V)
Theorem	fparlem2 7962	Lemma for fpar 7965. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦})
Theorem	fparlem3 7963*	Lemma for fpar 7965. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) = ∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)))
Theorem	fparlem4 7964*	Lemma for fpar 7965. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))
Theorem	fpar 7965*	Merge two functions in parallel. Use as the second argument of a composition with a binary operation to build compound functions such as (𝑥 ∈ (0[,)+∞), 𝑦 ∈ ℝ ↦ ((√‘𝑥) + (sin‘𝑦))), see also ex-fpar 28835. (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩))
Theorem	fsplit 7966	A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar 7965 in order to build compound functions such as (𝑥 ∈ (0[,)+∞) ↦ ((√‘𝑥) + (sin‘𝑥))). (Contributed by NM, 17-Sep-2007.) Replace use of dfid2 5492 with df-id 5490. (Revised by BJ, 31-Dec-2023.)
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
Theorem	fsplitOLD 7967	Obsolete proof of fsplit 7966 as of 31-Dec-2023. (Contributed by NM, 17-Sep-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
Theorem	fsplitfpar 7968*	Merge two functions with a common argument in parallel. Combination of fsplit 7966 and fpar 7965. (Contributed by AV, 3-Jan-2024.)
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))    &   ⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐻 ∘ 𝑆) = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩))
Theorem	offsplitfpar 7969	Express the function operation map ∘f by the functions defined in fsplit 7966 and fpar 7965. (Contributed by AV, 4-Jan-2024.)
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))    &   ⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴)    ⇒   ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) ∧ ( + Fn 𝐶 ∧ (ran 𝐹 × ran 𝐺) ⊆ 𝐶)) → ( + ∘ (𝐻 ∘ 𝑆)) = (𝐹 ∘f + 𝐺))
Theorem	f2ndf 7970	The 2nd (second component of an ordered pair) function restricted to a function 𝐹 is a function from 𝐹 into the codomain of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶𝐵)
Theorem	fo2ndf 7971	The 2nd (second component of an ordered pair) function restricted to a function 𝐹 is a function from 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹–onto→ran 𝐹)
Theorem	f1o2ndf1 7972	The 2nd (second component of an ordered pair) function restricted to a one-to-one function 𝐹 is a one-to-one function from 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
⊢ (𝐹:𝐴–1-1→𝐵 → (2nd ↾ 𝐹):𝐹–1-1-onto→ran 𝐹)
Theorem	opco1 7973	Value of an operation precomposed with the projection on the first component. (Contributed by Mario Carneiro, 28-May-2014.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴(𝐹 ∘ 1st )𝐵) = (𝐹‘𝐴))
Theorem	opco2 7974	Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴(𝐹 ∘ 2nd )𝐵) = (𝐹‘𝐵))
Theorem	opco1i 7975	Inference form of opco1 7973. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵(𝐹 ∘ 1st )𝐶) = (𝐹‘𝐵)
Theorem	frxp 7976*	A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
Theorem	xporderlem 7977*	Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
Theorem	poxp 7978*	A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))
Theorem	soxp 7979*	A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵))
Theorem	wexp 7980*	A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑆 We 𝐵) → 𝑇 We (𝐴 × 𝐵))
Theorem	fnwelem 7981*	Lemma for fnwe 7982. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 We 𝐵)    &   ⊢ (𝜑 → 𝑆 We 𝐴)    &   ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V)    &   ⊢ 𝑄 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))))}    &   ⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ ⟨(𝐹‘𝑧), 𝑧⟩)    ⇒   ⊢ (𝜑 → 𝑇 We 𝐴)
Theorem	fnwe 7982*	A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 We 𝐵)    &   ⊢ (𝜑 → 𝑆 We 𝐴)    &   ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V)    ⇒   ⊢ (𝜑 → 𝑇 We 𝐴)
Theorem	fnse 7983*	Condition for the well-order in fnwe 7982 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 Se 𝐵)    &   ⊢ (𝜑 → (◡𝐹 “ 𝑤) ∈ V)    ⇒   ⊢ (𝜑 → 𝑇 Se 𝐴)
Theorem	fvproj 7984*	Value of a function on ordered pairs with values expressed as ordered pairs. Note that 𝐹 and 𝐺 are the projections of 𝐻 to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.)
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻‘⟨𝑋, 𝑌⟩) = ⟨(𝐹‘𝑋), (𝐺‘𝑌)⟩)
Theorem	fimaproj 7985*	Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that 𝐹 and 𝐺 are the projections of 𝐻 to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.)
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
2.4.9  The support of functions In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 7988) are based on the Axiom of Union (usage of dmexg 7759), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (◡𝑅 “ (V ∖ {𝑍})) (see suppimacnv 7999). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now).
Syntax	csupp 7986	Extend class definition to include the support of functions.
class supp
Definition	df-supp 7987*	Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects." The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.)
⊢ supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}})
Theorem	suppval 7988*	The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋 “ {𝑖}) ≠ {𝑍}})
Theorem	supp0prc 7989	The support of a class is empty if either the class or the "zero" is a proper class. (Contributed by AV, 28-May-2019.)
⊢ (¬ (𝑋 ∈ V ∧ 𝑍 ∈ V) → (𝑋 supp 𝑍) = ∅)
Theorem	suppvalbr 7990*	The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑦 𝑥𝑅𝑦 ∧ ∃𝑦(𝑥𝑅𝑦 ↔ 𝑦 ≠ 𝑍))})
Theorem	supp0 7991	The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.)
⊢ (𝑍 ∈ 𝑊 → (∅ supp 𝑍) = ∅)
Theorem	suppval1 7992*	The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.)
⊢ ((Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋‘𝑖) ≠ 𝑍})
Theorem	suppvalfng 7993*	The value of the operation constructing the support of a function with a given domain. This version of suppvalfn 7994 assumes 𝐹 is a set rather than its domain 𝑋, avoiding ax-rep 5210. (Contributed by SN, 5-Aug-2024.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑖 ∈ 𝑋 ∣ (𝐹‘𝑖) ≠ 𝑍})
Theorem	suppvalfn 7994*	The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by AV, 22-Apr-2019.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑖 ∈ 𝑋 ∣ (𝐹‘𝑖) ≠ 𝑍})
Theorem	elsuppfng 7995	An element of the support of a function with a given domain. This version of elsuppfn 7996 assumes 𝐹 is a set rather than its domain 𝑋, avoiding ax-rep 5210. (Contributed by SN, 5-Aug-2024.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍)))
Theorem	elsuppfn 7996	An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍)))
Theorem	cnvimadfsn 7997*	The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}
Theorem	suppimacnvss 7998	The support of functions "defined" by inverse images is a subset of the support defined by df-supp 7987. (Contributed by AV, 7-Apr-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
Theorem	suppimacnv 7999	Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍})))
Theorem	frnsuppeq 8000	Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.)
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 supp 𝑍) = (◡𝐹 “ (𝑆 ∖ {𝑍}))))