P. 82 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	curry1 8101*	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 8102	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 8103	Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(2nd ↾ ({𝐶} × V)))    ⇒   ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐴) → 𝐺:𝐵⟶𝐷)
Theorem	curry2 8104*	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 8105	Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐷 ∧ 𝐶 ∈ 𝐵) → 𝐺:𝐴⟶𝐷)
Theorem	curry2val 8106	The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝐺‘𝐷) = (𝐷𝐹𝐶))
Theorem	cnvf1olem 8107	Lemma for cnvf1o 8108. (Contributed by Mario Carneiro, 27-Apr-2014.)
⊢ ((Rel 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (𝐶 ∈ ◡𝐴 ∧ 𝐵 = ∪ ◡{𝐶}))
Theorem	cnvf1o 8108*	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 8109	Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (◡(1st ↾ (V × V)) “ {𝑥}) = ({𝑥} × V)
Theorem	fparlem2 8110	Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (◡(2nd ↾ (V × V)) “ {𝑦}) = (V × {𝑦})
Theorem	fparlem3 8111*	Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) = ∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)))
Theorem	fparlem4 8112*	Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))) = ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))
Theorem	fpar 8113*	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 30389. (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 8114	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 8113 in order to build compound functions such as (𝑥 ∈ (0[,)+∞) ↦ ((√‘𝑥) + (sin‘𝑥))). (Contributed by NM, 17-Sep-2007.) Replace use of dfid2 5550 with df-id 5548. (Revised by BJ, 31-Dec-2023.)
⊢ ◡(1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
Theorem	fsplitfpar 8115*	Merge two functions with a common argument in parallel. Combination of fsplit 8114 and fpar 8113. (Contributed by AV, 3-Jan-2024.)
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))    &   ⊢ 𝑆 = (◡(1st ↾ I ) ↾ 𝐴)    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐻 ∘ 𝑆) = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩))
Theorem	offsplitfpar 8116	Express the function operation map ∘f by the functions defined in fsplit 8114 and fpar 8113. (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 8117	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 8118	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 8119	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 8120	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 8121	Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴(𝐹 ∘ 2nd )𝐵) = (𝐹‘𝐵))
Theorem	opco1i 8122	Inference form of opco1 8120. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐵(𝐹 ∘ 1st )𝐶) = (𝐹‘𝐵)
Theorem	frxp 8123*	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 8124*	Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}    ⇒   ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
Theorem	poxp 8125*	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 8126*	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 8127*	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 8128*	Lemma for fnwe 8129. (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 8129*	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 8130*	Condition for the well-order in fnwe 8129 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 Se 𝐵)    &   ⊢ (𝜑 → (◡𝐹 “ 𝑤) ∈ V)    ⇒   ⊢ (𝜑 → 𝑇 Se 𝐴)
Theorem	fvproj 8131*	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 8132*	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 8133*	A version of ralxp 5821 with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ (∀𝑥 ∈ (𝐴 × 𝐵)[(1st ‘𝑥) / 𝑦][(2nd ‘𝑥) / 𝑧]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜑)
Theorem	ralxp3f 8134*	Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨𝑦, 𝑧, 𝑤⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜓)
Theorem	ralxp3 8135*	Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 2-Feb-2025.)
⊢ (𝑥 = ⟨𝑦, 𝑧, 𝑤⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜓)
Theorem	ralxp3es 8136*	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 8137*	Special case of founded partial induction over a Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧∀𝑤(⟨𝑧, 𝑤⟩ ∈ Pred(𝑅, (𝐴 × 𝐵), ⟨𝑥, 𝑦⟩) → 𝜒) → 𝜑))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑦 = 𝑌 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → 𝜏)
Theorem	frpoins3xp3g 8138*	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 8139*	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 8140*	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 8141*	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 8142*	Calculate the predecessor class in frxp2 8141. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
Theorem	sexp2 8143*	Condition for the relation in frxp2 8141 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑆 Se 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 Se (𝐴 × 𝐵))
Theorem	xpord2indlem 8144*	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 8145*	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 8146*	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 8147*	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 8148*	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 8149*	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 8150*	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 8151*	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 8152*	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 8153*	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 8154*	Lemma for poseq 8155 and soseq 8156. The function value of a sequence is either in 𝐴 or null. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}    ⇒   ⊢ (𝐺 ∈ 𝐹 → (𝐺‘𝑋) ∈ (𝐴 ∪ {∅}))
Theorem	poseq 8155*	A partial ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝑅 Po (𝐴 ∪ {∅})    &   ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}    &   ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}    ⇒   ⊢ 𝑆 Po 𝐹
Theorem	soseq 8156*	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 8159) are based on the Axiom of Union (usage of dmexg 7895), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (◡𝑅 “ (V ∖ {𝑍})) (see suppimacnv 8171). 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 8157	Extend class definition to include the support of functions.
class supp
Definition	df-supp 8158*	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 8159*	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 8160	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 8161*	The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑦 𝑥𝑅𝑦 ∧ ∃𝑦(𝑥𝑅𝑦 ↔ 𝑦 ≠ 𝑍))})
Theorem	supp0 8162	The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.)
⊢ (𝑍 ∈ 𝑊 → (∅ supp 𝑍) = ∅)
Theorem	suppval1 8163*	The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.)
⊢ ((Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋‘𝑖) ≠ 𝑍})
Theorem	suppvalfng 8164*	The value of the operation constructing the support of a function with a given domain. This version of suppvalfn 8165 assumes 𝐹 is a set rather than its domain 𝑋, avoiding ax-rep 5249. (Contributed by SN, 5-Aug-2024.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑖 ∈ 𝑋 ∣ (𝐹‘𝑖) ≠ 𝑍})
Theorem	suppvalfn 8165*	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 8166	An element of the support of a function with a given domain. This version of elsuppfn 8167 assumes 𝐹 is a set rather than its domain 𝑋, avoiding ax-rep 5249. (Contributed by SN, 5-Aug-2024.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍)))
Theorem	elsuppfn 8167	An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍)))
Theorem	fvdifsupp 8168	Function value is zero outside of its support. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∖ (𝐹 supp 𝑍)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) = 𝑍)
Theorem	cnvimadfsn 8169*	The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}
Theorem	suppimacnvss 8170	The support of functions "defined" by inverse images is a subset of the support defined by df-supp 8158. (Contributed by AV, 7-Apr-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
Theorem	suppimacnv 8171	Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍})))
Theorem	fsuppeq 8172	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 𝑍) = (◡𝐹 “ (𝑆 ∖ {𝑍}))))
Theorem	fsuppeqg 8173	Version of fsuppeq 8172 avoiding ax-rep 5249 by assuming 𝐹 is a set rather than its domain 𝐼. (Contributed by SN, 30-Jul-2024.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 supp 𝑍) = (◡𝐹 “ (𝑆 ∖ {𝑍}))))
Theorem	suppssdm 8174	The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.)
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹
Theorem	suppsnop 8175	The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.)
⊢ 𝐹 = {⟨𝑋, 𝑌⟩}    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋}))
Theorem	snopsuppss 8176	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 8177	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 8178	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 8179*	Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.)
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∃𝑥 ∈ (𝐹 supp 𝑍)𝜑 ↔ ∃𝑥 ∈ 𝑋 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑)))
Theorem	ressuppss 8180	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 8181	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 8182	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 8183*	The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})})
Theorem	mptsuppd 8184*	The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍})
Theorem	extmptsuppeq 8185*	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 8186*	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 8187	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 8188	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 8189	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 8190	The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.)
⊢ ((𝐵 × {𝑍}) supp 𝑍) = ∅
Theorem	suppss 8191*	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 8192	A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍)
Theorem	suppssrg 8193	A function is zero outside its support. Version of suppssr 8192 avoiding ax-rep 5249 by assuming 𝐹 is a set rather than its domain 𝐴. (Contributed by SN, 5-May-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍)
Theorem	suppssov1 8194*	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 8195*	Formula building theorem for support restrictions: operator with right annihilator. (Contributed by SN, 11-Apr-2025.)
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐵) supp 𝑌) ⊆ 𝐿)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑣𝑂𝑌) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿)
Theorem	suppssof1 8196*	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 8197*	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 8198*	Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊) → 𝐵 = 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ {𝑊})
Theorem	suppssfv 8199*	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 8200	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 𝑍)))