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