P. 81 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opiota 8001*	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 8002*	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 8003*	Define the Cartesian product of three classes. Compare df-xp 5629. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.)
⊢ ((𝐴 × 𝐵) × 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)}
Theorem	elopabi 8004*	A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.)
⊢ (𝑥 = (1st ‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = (2nd ‘𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} → 𝜒)
Theorem	eloprabi 8005*	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 8006*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶)
Theorem	mpompts 8007*	Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd ‘𝑧) / 𝑦⦌𝐶)
Theorem	dmmpossx 8008*	The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
Theorem	fmpox 8009*	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 8010*	Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
Theorem	fnmpo 8011*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn (𝐴 × 𝐵))
Theorem	fnmpoi 8012*	Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ 𝐹 Fn (𝐴 × 𝐵)
Theorem	dmmpo 8013*	Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ dom 𝐹 = (𝐴 × 𝐵)
Theorem	ovmpoelrn 8014*	An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑂 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝑂𝑌) ∈ 𝑀)
Theorem	dmmpoga 8015*	Domain of an operation given by the maps-to notation, closed form of dmmpo 8013. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = (𝐴 × 𝐵))
Theorem	dmmpog 8016*	Domain of an operation given by the maps-to notation, closed form of dmmpo 8013. 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 8017*	Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	mpoexg 8018*	Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 𝐹 ∈ V)
Theorem	mpoexga 8019*	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 8020*	Weak version of mpoex 8021 that holds without ax-rep 5221. 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 8021*	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 8022*	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; avoid ax-rep 5221. (Revised by SN, 7-Apr-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺))    &   ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃))    &   ⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏))    &   ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}))    ⇒   ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)})
Theorem	mptmpoopabbrdOLD 8023*	Obsolete version of mptmpoopabbrd 8022 as of 7-Apr-2025. (Contributed by Alexander van Vekens, 8-Nov-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵‘𝐺))    &   ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → (𝜏 ↔ 𝜃))    &   ⊢ (𝑔 = 𝐺 → (𝜒 ↔ 𝜏))    &   ⊢ 𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴‘𝑔), 𝑏 ∈ (𝐵‘𝑔) ↦ {⟨𝑓, ℎ⟩ ∣ (𝜒 ∧ 𝑓(𝐷‘𝑔)ℎ)}))    ⇒   ⊢ (𝜑 → (𝑋(𝑀‘𝐺)𝑌) = {⟨𝑓, ℎ⟩ ∣ (𝜃 ∧ 𝑓(𝐷‘𝐺)ℎ)})
Theorem	mptmpoopabovd 8024*	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	el2mpocsbcl 8025*	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 8026*	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 8027*	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 8028*	The function operation expressed as a mapping, variation of offval2 7637. (Contributed by SO, 15-Jul-2018.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷)))
Theorem	brovpreldm 8029	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 8030*	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 8031*	Lemma for bropfvvvv 8032. (Contributed by AV, 31-Dec-2020.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {⟨𝑑, 𝑒⟩ ∣ 𝜑}))    &   ⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {⟨𝑑, 𝑒⟩ ∣ 𝜃})    ⇒   ⊢ ((⟨𝐵, 𝐶⟩ ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))
Theorem	bropfvvvv 8032*	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 8033*	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 8034*	Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 9-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨𝑧, 𝑤⟩ ∣ 𝜑})    ⇒   ⊢ Rel (𝐶𝐹𝐷)
Theorem	fmpoco 8035*	Composition of two functions. Variation of fmptco 7067 when the second function has two arguments. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆))    &   ⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇))
Theorem	oprabco 8036*	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 8037*	Composition of operator abstractions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by David Abernethy, 23-Apr-2013.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑅)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨𝐶, 𝐷⟩)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑀𝐷))    ⇒   ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹))
Theorem	df1st2 8038*	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 8039*	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 8040	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 8041	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 8042*	Alternate definition for the maps-to notation df-mpo 7358 (although it requires that 𝐶 be a set). (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐶 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 {⟨⟨𝑥, 𝑦⟩, 𝐶⟩}
Theorem	mposn 8043*	An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019.)
⊢ 𝐹 = (𝑥 ∈ {𝐴}, 𝑦 ∈ {𝐵} ↦ 𝐶)    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑦 = 𝐵 → 𝐷 = 𝐸)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈) → 𝐹 = {⟨⟨𝐴, 𝐵⟩, 𝐸⟩})
Theorem	curry1 8044*	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 8045	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 8046	Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))    ⇒   ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐴) → 𝐺:𝐵⟶𝐷)
Theorem	curry2 8047*	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 8048	Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐵) → 𝐺:𝐴⟶𝐷)
Theorem	curry2val 8049	The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝐺‘𝐷) = (𝐷𝐹𝐶))
Theorem	cnvf1olem 8050	Lemma for cnvf1o 8051. (Contributed by Mario Carneiro, 27-Apr-2014.)
⊢ ((Rel 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (𝐶 ∈ ◡𝐴 ∧ 𝐵 = ∪ ◡{𝐶}))
Theorem	cnvf1o 8051*	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 8052	Lemma for fpar 8056. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (◡(1st ↾ (V × V)) “ {𝑥}) = ({𝑥} × V)
Theorem	fparlem2 8053	Lemma for fpar 8056. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦})
Theorem	fparlem3 8054*	Lemma for fpar 8056. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) = ∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)))
Theorem	fparlem4 8055*	Lemma for fpar 8056. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))
Theorem	fpar 8056*	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 30424. (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 8057	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 8056 in order to build compound functions such as (𝑥 ∈ (0[,)+∞) ↦ ((√‘𝑥) + (sin‘𝑥))). (Contributed by NM, 17-Sep-2007.) Replace use of dfid2 5520 with df-id 5518. (Revised by BJ, 31-Dec-2023.)
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
Theorem	fsplitfpar 8058*	Merge two functions with a common argument in parallel. Combination of fsplit 8057 and fpar 8056. (Contributed by AV, 3-Jan-2024.)
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))    &   ⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐻 ∘ 𝑆) = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩))
Theorem	offsplitfpar 8059	Express the function operation map ∘f by the functions defined in fsplit 8057 and fpar 8056. (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 8060	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 8061	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 8062	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 8063	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 8064	Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴(𝐹 ∘ 2nd )𝐵) = (𝐹‘𝐵))
Theorem	opco1i 8065	Inference form of opco1 8063. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵(𝐹 ∘ 1st )𝐶) = (𝐹‘𝐵)
Theorem	frxp 8066*	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 8067*	Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
Theorem	poxp 8068*	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 8069*	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 8070*	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 8071*	Lemma for fnwe 8072. (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 8072*	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 8073*	Condition for the well-order in fnwe 8072 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 Se 𝐵)    &   ⊢ (𝜑 → (◡𝐹 “ 𝑤) ∈ V)    ⇒   ⊢ (𝜑 → 𝑇 Se 𝐴)
Theorem	fvproj 8074*	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 8075*	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 𝐵)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
Theorem	ralxpes 8076*	A version of ralxp 5788 with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ (∀𝑥 ∈ (𝐴 × 𝐵)[(1st ‘𝑥) / 𝑦][(2nd ‘𝑥) / 𝑧]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜑)
Theorem	ralxp3f 8077*	Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧, 𝑤⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜓)
Theorem	ralxp3 8078*	Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝑥 = ⟨𝑦, 𝑧, 𝑤⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜓)
Theorem	ralxp3es 8079*	Restricted for-all over a triple Cartesian product with explicit substitution. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st ‘𝑥)) / 𝑦][(2nd ‘(1st ‘𝑥)) / 𝑧][(2nd ‘𝑥) / 𝑤]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜑)
2.4.9  Induction on Cartesian products
Theorem	frpoins3xpg 8080*	Special case of founded partial induction over a Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧∀𝑤(⟨𝑧, 𝑤⟩ ∈ Pred(𝑅, (𝐴 × 𝐵), ⟨𝑥, 𝑦⟩) → 𝜒) → 𝜑))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑦 = 𝑌 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → 𝜏)
Theorem	frpoins3xp3g 8081*	Special case of founded partial recursion over a triple Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) → 𝜑))    &   ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁)
2.4.10  Ordering on Cartesian products
Theorem	xpord2lem 8082*	Lemma for Cartesian product ordering. Calculate the value of the Cartesian product relation. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ ((𝑎𝑅𝑐 ∨ 𝑎 = 𝑐) ∧ (𝑏𝑆𝑑 ∨ 𝑏 = 𝑑) ∧ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))))
Theorem	poxp2 8083*	Another way of partially ordering a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Po 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))
Theorem	frxp2 8084*	Another way of giving a well-founded order to a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Fr 𝐴)    &   ⊢ (𝜑 → 𝑆 Fr 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 Fr (𝐴 × 𝐵))
Theorem	xpord2pred 8085*	Calculate the predecessor class in frxp2 8084. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
Theorem	sexp2 8086*	Condition for the relation in frxp2 8084 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑆 Se 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 Se (𝐴 × 𝐵))
Theorem	xpord2indlem 8087*	Induction over the Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ 𝑅 Fr 𝐴    &   ⊢ 𝑅 Po 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ 𝑆 Fr 𝐵    &   ⊢ 𝑆 Po 𝐵    &   ⊢ 𝑆 Se 𝐵    &   ⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) → 𝜑))    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝜂)
Theorem	xpord2ind 8088*	Induction over the Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ 𝑅 Fr 𝐴    &   ⊢ 𝑅 Po 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ 𝑆 Fr 𝐵    &   ⊢ 𝑆 Po 𝐵    &   ⊢ 𝑆 Se 𝐵    &   ⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) → 𝜑))    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝜂)
Theorem	xpord3lem 8089*	Lemma for triple ordering. Calculate the value of the relation. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
Theorem	poxp3 8090*	Triple Cartesian product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Po 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑇 Po 𝐶)    ⇒   ⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))
Theorem	frxp3 8091*	Give well-foundedness over a triple Cartesian product. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Fr 𝐴)    &   ⊢ (𝜑 → 𝑆 Fr 𝐵)    &   ⊢ (𝜑 → 𝑇 Fr 𝐶)    ⇒   ⊢ (𝜑 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
Theorem	xpord3pred 8092*	Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025.)
⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
Theorem	sexp3 8093*	Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑆 Se 𝐵)    &   ⊢ (𝜑 → 𝑇 Se 𝐶)    ⇒   ⊢ (𝜑 → 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
Theorem	xpord3inddlem 8094*	Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜅 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜅 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜅 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜅 → 𝑅 Fr 𝐴)    &   ⊢ (𝜅 → 𝑅 Po 𝐴)    &   ⊢ (𝜅 → 𝑅 Se 𝐴)    &   ⊢ (𝜅 → 𝑆 Fr 𝐵)    &   ⊢ (𝜅 → 𝑆 Po 𝐵)    &   ⊢ (𝜅 → 𝑆 Se 𝐵)    &   ⊢ (𝜅 → 𝑇 Fr 𝐶)    &   ⊢ (𝜅 → 𝑇 Po 𝐶)    &   ⊢ (𝜅 → 𝑇 Se 𝐶)    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))    &   ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))    &   ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))    &   ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))    &   ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))    &   ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))    ⇒   ⊢ (𝜅 → 𝜆)
Theorem	xpord3indd 8095*	Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝜅 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜅 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜅 → 𝑍 ∈ 𝐶)    &   ⊢ (𝜅 → 𝑅 Fr 𝐴)    &   ⊢ (𝜅 → 𝑅 Po 𝐴)    &   ⊢ (𝜅 → 𝑅 Se 𝐴)    &   ⊢ (𝜅 → 𝑆 Fr 𝐵)    &   ⊢ (𝜅 → 𝑆 Po 𝐵)    &   ⊢ (𝜅 → 𝑆 Se 𝐵)    &   ⊢ (𝜅 → 𝑇 Fr 𝐶)    &   ⊢ (𝜅 → 𝑇 Po 𝐶)    &   ⊢ (𝜅 → 𝑇 Se 𝐶)    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))    &   ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))    &   ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))    &   ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))    &   ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))    &   ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))    ⇒   ⊢ (𝜅 → 𝜆)
Theorem	xpord3ind 8096*	Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024.)
⊢ 𝑅 Fr 𝐴    &   ⊢ 𝑅 Po 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ 𝑆 Fr 𝐵    &   ⊢ 𝑆 Po 𝐵    &   ⊢ 𝑆 Se 𝐵    &   ⊢ 𝑇 Fr 𝐶    &   ⊢ 𝑇 Po 𝐶    &   ⊢ 𝑇 Se 𝐶    &   ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))    &   ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))    &   ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))    &   ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))    &   ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))    &   ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → 𝜆)
2.4.11  Ordering Ordinal Sequences
Theorem	orderseqlem 8097*	Lemma for poseq 8098 and soseq 8099. The function value of a sequence is either in 𝐴 or null. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}    ⇒   ⊢ (𝐺 ∈ 𝐹 → (𝐺‘𝑋) ∈ (𝐴 ∪ {∅}))
Theorem	poseq 8098*	A partial ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝑅 Po (𝐴 ∪ {∅})    &   ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}    &   ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}    ⇒   ⊢ 𝑆 Po 𝐹
Theorem	soseq 8099*	A linear ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝑅 Or (𝐴 ∪ {∅})    &   ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}    &   ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}    &   ⊢ ¬ ∅ ∈ 𝐴    ⇒   ⊢ 𝑆 Or 𝐹
2.4.12  The support of functions In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 8102) are based on the Axiom of Union (usage of dmexg 7841), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (◡𝑅 “ (V ∖ {𝑍})) (see suppimacnv 8114). 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 8100	Extend class definition to include the support of functions.
class supp