P. 331 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33001-33100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	off2 33001*	The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈)
Theorem	ofresid 33002	Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f (𝑅 ↾ (𝐵 × 𝐵))𝐺))
Theorem	unipreima 33003*	Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.)
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥))
Theorem	opfv 33004	Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = ⟨((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)⟩)
Theorem	xppreima 33005	The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (◡𝐹 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍)))
Theorem	2ndimaxp 33006	Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)
Theorem	dmdju 33007*	Domain of a disjoint union of non-empty sets. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → dom ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = 𝐴)
Theorem	djussxp2 33008*	Stronger version of djussxp 5834. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵)
Theorem	2ndresdju 33009*	The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)
Theorem	2ndresdjuf1o 33010*	The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 8098. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴)
Theorem	xppreima2 33011*	The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍)))
Theorem	abfmpunirn 33012*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓))
Theorem	rabfmpunirn 33013*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑})    &   ⊢ 𝑊 ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓))
Theorem	abfmpeld 33014*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓})    &   ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V)    &   ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒)))
Theorem	abfmpel 33015*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓))
Theorem	fmptdf2 33016	Domain and codomain of the mapping operation; deduction form. This version of fmptd 7113 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmptcof2 33017*	Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) (Revised by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑦𝑇    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))    &   ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))
Theorem	fcomptf 33018*	Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 7133. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥))))
Theorem	acunirnmpt 33019*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵))
Theorem	acunirnmpt2 33020*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))
Theorem	acunirnmpt2f 33021*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑗𝐶    &   ⊢ Ⅎ𝑗𝐷    &   ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵    &   ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))
Theorem	aciunf1lem 33022*	Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥))
Theorem	aciunf1 33023*	Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘))
Theorem	ofoprabco 33024*	Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ Ⅎ𝑎𝑀    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))    &   ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀))
Theorem	ofpreima 33025*	Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶))    ⇒   ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
Theorem	ofpreima2 33026*	Express the preimage of a function operation as a union of preimages. This version of ofpreima 33025 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶))    ⇒   ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
Theorem	funcnv5mpt 33027*	Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶)))
Theorem	funcnv4mpt 33028*	Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)))
Theorem	preimane 33029	Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐹)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌}))
Theorem	fnpreimac 33030*	Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
Theorem	fgreu 33031*	Exactly one point of a function's graph has a given first element. (Contributed by Thierry Arnoux, 1-Apr-2018.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∃!𝑝 ∈ 𝐹 𝑋 = (1st ‘𝑝))
Theorem	fcnvgreu 33032*	If the converse of a relation 𝐴 is a function, exactly one point of its graph has a given second element (that is, function value). (Contributed by Thierry Arnoux, 1-Apr-2018.)
⊢ (((Rel 𝐴 ∧ Fun ◡𝐴) ∧ 𝑌 ∈ ran 𝐴) → ∃!𝑝 ∈ 𝐴 𝑌 = (2nd ‘𝑝))
Theorem	rnmposs 33033*	The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷)
Theorem	mptssALT 33034*	Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 6047. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	dfcnv2 33035*	Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.)
⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥})))
Theorem	partfun2 33036*	Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. See also partfun 6686 and ifmpt2v 7518. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ if(𝜑, 𝐵, 𝐶)) = ((𝑥 ∈ 𝐷 ↦ 𝐵) ∪ (𝑥 ∈ (𝐴 ∖ 𝐷) ↦ 𝐶))
Theorem	rnressnsn 33037	The range of a restriction to a singleton is a singleton. See dmressnsn 6025. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ran (𝐹 ↾ {𝐴}) = {(𝐹‘𝐴)})
21.3.4.3  Operations - misc additions
Theorem	mpomptxf 33038*	Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Thierry Arnoux, 31-Mar-2018.)
⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	of0r 33039	Function operation with the empty function. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ (𝐹 ∘f 𝑅∅) = ∅
21.3.4.4  The mapping operation
Theorem	elmaprd 33040	Deduction associated with elmapd 8839. Reverse direction of elmapdd 8840. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
21.3.4.5  Support of a function
Theorem	suppovss 33041*	A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))
Theorem	elsuppfnd 33042	Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝑋) ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐹 supp 𝑍))
Theorem	fisuppov1 33043*	Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 0 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐸)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ( 0 𝑂𝑦) = 𝑍)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ ((𝐹‘𝑥)𝑂𝐵)) finSupp 𝑍)
Theorem	suppun2 33044	The support of a union is the union of the supports. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) = ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍)))
Theorem	fdifsupp 33045	Express the support of a function 𝐹 outside of 𝐵 in two different ways. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) = ((𝐹 supp 𝑍) ∖ 𝐵))
Theorem	suppiniseg 33046	Relation between the support (𝐹 supp 𝑍) and the initial segment (◡𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍}))
Theorem	fsuppinisegfi 33047	The initial segment (◡𝐹 “ {𝑌}) of a nonzero 𝑌 is finite if 𝐹 has finite support. (Contributed by Thierry Arnoux, 21-Jun-2024.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ (V ∖ { 0 }))    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    ⇒   ⊢ (𝜑 → (◡𝐹 “ {𝑌}) ∈ Fin)
Theorem	fressupp 33048	The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍})))
Theorem	fdifsuppconst 33049	A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024.)
⊢ 𝐴 = (dom 𝐹 ∖ (𝐹 supp 𝑍))    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ 𝐴) = (𝐴 × {𝑍}))
Theorem	ressupprn 33050	The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 }))
Theorem	supppreima 33051	Express the support of a function as the preimage of its range except zero. (Contributed by Thierry Arnoux, 24-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (ran 𝐹 ∖ {𝑍})))
Theorem	fsupprnfi 33052	Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024.)
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin)
Theorem	mptiffisupp 33053*	Conditions for a mapping function defined with a conditional to have finite support. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝑍))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
21.3.4.6  Explicit Functions with one or two points as a domain
Theorem	cosnopne 33054	Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐷)    ⇒   ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐷⟩}) = ∅)
Theorem	cosnop 33055	Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐴⟩}) = {⟨𝐶, 𝐵⟩})
Theorem	cnvprop 33056	Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {⟨𝐵, 𝐴⟩, ⟨𝐷, 𝐶⟩})
Theorem	brprop 33057	Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷))))
Theorem	mptprop 33058*	Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷)))
Theorem	coprprop 33059	Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ≠ 𝐹)    ⇒   ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩})
Theorem	fmptunsnop 33060*	Two ways to express a function with a value replaced. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑥 = 𝑋, 𝑌, (𝐹‘𝑥))) = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, 𝑌⟩}))
21.3.4.7  Isomorphisms - misc. additions
Theorem	gtiso 33061	Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵)))
Theorem	isoun 33062*	Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥𝑅𝑦)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷) → 𝑧𝑆𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑥𝑅𝑦)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑧𝑆𝑤)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅)    ⇒   ⊢ (𝜑 → (𝐻 ∪ 𝐺) Isom 𝑅, 𝑆 ((𝐴 ∪ 𝐶), (𝐵 ∪ 𝐷)))
21.3.4.8  Disjointness (additional proof requiring functions)
Theorem	disjdsct 33063*	A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv 6609) (Contributed by Thierry Arnoux, 28-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅}))    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵))
21.3.4.9  First and second members of an ordered pair - misc additions
Theorem	df1stres 33064*	Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥)
Theorem	df2ndres 33065*	Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦)
Theorem	1stpreimas 33066	The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.)
⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋})))
Theorem	1stpreima 33067	The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶))
Theorem	2ndpreima 33068	The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴))
Theorem	curry2ima 33069*	The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)})
Theorem	preiman0 33070	The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ 𝐴) ≠ ∅)
Theorem	intimafv 33071*	The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ∩ (𝐹 “ 𝐴) = ∩ 𝑥 ∈ 𝐴 (𝐹‘𝑥))
21.3.4.10  Countable Sets
Theorem	snct 33072	A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω)
Theorem	prct 33073	An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω)
Theorem	mpocti 33074*	An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉    ⇒   ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	abrexct 33075*	An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω)
Theorem	mptctf 33076	A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω)
Theorem	abrexctf 33077*	An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω)
Theorem	padct 33078*	Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.) Avoid ax-rep 5241. (Revised by GG, 2-Apr-2026.)
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
Theorem	f1od2 33079*	Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))    &   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)
Theorem	fcobij 33080*	Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017.)
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑓 ∈ (𝑆 ↑m 𝑅) ↦ (𝐺 ∘ 𝑓)):(𝑆 ↑m 𝑅)–1-1-onto→(𝑇 ↑m 𝑅))
Theorem	fcobijfs 33081*	Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9370. (Contributed by Thierry Arnoux, 25-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑆)    &   ⊢ 𝑄 = (𝐺‘𝑂)    &   ⊢ 𝑋 = {𝑔 ∈ (𝑆 ↑m 𝑅) ∣ 𝑔 finSupp 𝑂}    &   ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑m 𝑅) ∣ ℎ finSupp 𝑄}    ⇒   ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝐺 ∘ 𝑓)):𝑋–1-1-onto→𝑌)
Theorem	fcobijfs2 33082*	Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also fcobijfs 33081 and mapfien 9370. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐺:𝑅–1-1-onto→𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑇)    &   ⊢ 𝑋 = {𝑔 ∈ (𝑇 ↑m 𝑆) ∣ 𝑔 finSupp 𝑂}    &   ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑m 𝑅) ∣ ℎ finSupp 𝑂}    ⇒   ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝑓 ∘ 𝐺)):𝑋–1-1-onto→𝑌)
Theorem	suppss3 33083*	Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑍) → 𝐵 = 𝑍)    ⇒   ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍))
Theorem	fsuppcurry1 33084*	Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.)
⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → 𝐺 finSupp 𝑍)
Theorem	fsuppcurry2 33085*	Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.)
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶))    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → 𝐺 finSupp 𝑍)
Theorem	offinsupp1 33086*	Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑇)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑌𝑅𝑥) = 𝑍)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) finSupp 𝑍)
Theorem	ffs2 33087	Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq 8173. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐶 = (𝐵 ∖ {𝑍})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 supp 𝑍) = (◡𝐹 “ 𝐶))
Theorem	ffsrn 33088	The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ Fin)
Theorem	cocnvf1o 33089	Composing with the inverse of a bijection. (Contributed by Thierry Arnoux, 15-Jan-2026.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → (𝐹 = (𝐺 ∘ 𝐻) ↔ 𝐺 = (𝐹 ∘ ◡𝐻)))
Theorem	resf1o 33090*	Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.)
⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶}    &   ⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶))    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑m 𝐶))
Theorem	maprnin 33091*	Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ∩ 𝐶) ↑m 𝐴) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ran 𝑓 ⊆ 𝐶}
Theorem	fpwrelmapffslem 33092*	Lemma for fpwrelmapffs 33094. For this theorem, the sets 𝐴 and 𝐵 could be infinite, but the relation 𝑅 itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵)    &   ⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))})    ⇒   ⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin)))
Theorem	fpwrelmap 33093*	Define a canonical mapping between functions from 𝐴 into subsets of 𝐵 and the relations with domain 𝐴 and range within 𝐵. Note that the same relation is used in axdc2lem 10442 and marypha2lem1 9397. (Contributed by Thierry Arnoux, 28-Aug-2017.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})    ⇒   ⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)
Theorem	fpwrelmapffs 33094*	Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})    &   ⊢ 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin}    ⇒   ⊢ (𝑀 ↾ 𝑆):𝑆–1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin)
21.3.5  Real and Complex Numbers
Theorem	sgnval2 33095	Value of the signum of a real number, expresssed using absolute value. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (sgn‘𝐴) = (𝐴 / (abs‘𝐴)))
21.3.5.1  Complex operations - misc. additions
Theorem	creq0 33096	The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 12221. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ (𝐴 + (i · 𝐵)) = 0))
Theorem	1nei 33097	The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ 1 ≠ i
Theorem	1neg1t1neg1 33098	An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020.)
⊢ (𝑁 ∈ {-1, 1} → (𝑁 · 𝑁) = 1)
Theorem	nnmulge 33099	Multiplying by a positive integer 𝑀 yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (𝑀 · 𝑁))
Theorem	submuladdd 33100	The product of a difference and a sum. Cf. addmulsub 11686. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐴 · 𝐷)) − ((𝐵 · 𝐶) + (𝐵 · 𝐷))))