P. 327 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32601-32700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ac6mapd 32601*	Axiom of choice equivalent, deduction form. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝑦 = (𝑓‘𝑥) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (𝐵 ↑m 𝐴)∀𝑥 ∈ 𝐴 𝜒)
Theorem	fnresin 32602	Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐵) Fn (𝐴 ∩ 𝐵))
Theorem	f1o3d 32603*	Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷)))
Theorem	eldmne0 32604	A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ (𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅)
Theorem	f1rnen 32605	Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉) → ran 𝐹 ≈ 𝐴)
Theorem	f1oeq3dd 32606	Equality deduction for one-to-one onto functions. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵)
Theorem	rinvf1o 32607	Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ Fun 𝐹    &   ⊢ ◡𝐹 = 𝐹    &   ⊢ (𝐹 “ 𝐴) ⊆ 𝐵    &   ⊢ (𝐹 “ 𝐵) ⊆ 𝐴    &   ⊢ 𝐴 ⊆ dom 𝐹    &   ⊢ 𝐵 ⊆ dom 𝐹    ⇒   ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→𝐵
Theorem	fresf1o 32608	Conditions for a restriction to be a one-to-one onto function. (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun (◡𝐹 ↾ 𝐶)) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–1-1-onto→𝐶)
Theorem	nfpconfp 32609	The set of fixed points of 𝐹 is the complement of the set of points moved by 𝐹. (Contributed by Thierry Arnoux, 17-Nov-2023.)
⊢ (𝐹 Fn 𝐴 → (𝐴 ∖ dom (𝐹 ∖ I )) = dom (𝐹 ∩ I ))
Theorem	fmptco1f1o 32610*	The action of composing (to the right) with a bijection is itself a bijection of functions. (Contributed by Thierry Arnoux, 3-Jan-2021.)
⊢ 𝐴 = (𝑅 ↑m 𝐸)    &   ⊢ 𝐵 = (𝑅 ↑m 𝐷)    &   ⊢ 𝐹 = (𝑓 ∈ 𝐴 ↦ (𝑓 ∘ 𝑇))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑇:𝐷–1-1-onto→𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	cofmpt2 32611*	Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023.)
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝐶) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝐷))
Theorem	f1mptrn 32612*	Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃!𝑥 ∈ 𝐴 𝑦 = 𝐵)    ⇒   ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfimafnf 32613*	Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
Theorem	funimass4f 32614	Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	suppss2f 32615*	Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017.) (Revised by AV, 1-Sep-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝑊    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)
Theorem	ofrn 32616	The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ 𝐶)
Theorem	ofrn2 32617	The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺)))
Theorem	off2 32618*	The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈)
Theorem	ofresid 32619	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 32620*	Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.)
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥))
Theorem	opfv 32621	Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = ⟨((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)⟩)
Theorem	xppreima 32622	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 32623	Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)
Theorem	dmdju 32624*	Domain of a disjoint union of non-empty sets. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → dom ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = 𝐴)
Theorem	djussxp2 32625*	Stronger version of djussxp 5785. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵)
Theorem	2ndresdju 32626*	The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴)
Theorem	2ndresdjuf1o 32627*	The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 8031. (Contributed by Thierry Arnoux, 23-Jun-2024.)
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶)    &   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴)    ⇒   ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴)
Theorem	xppreima2 32628*	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 32629*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓))
Theorem	rabfmpunirn 32630*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑})    &   ⊢ 𝑊 ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓))
Theorem	abfmpeld 32631*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓})    &   ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V)    &   ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒)))
Theorem	abfmpel 32632*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓))
Theorem	fmptdF 32633	Domain and codomain of the mapping operation; deduction form. This version of fmptd 7047 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fmptcof2 32634*	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 32635*	Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 7066. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥))))
Theorem	acunirnmpt 32636*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵))
Theorem	acunirnmpt2 32637*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))
Theorem	acunirnmpt2f 32638*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑗𝐶    &   ⊢ Ⅎ𝑗𝐷    &   ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵    &   ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))
Theorem	aciunf1lem 32639*	Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥))
Theorem	aciunf1 32640*	Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘))
Theorem	ofoprabco 32641*	Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ Ⅎ𝑎𝑀    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))    &   ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀))
Theorem	ofpreima 32642*	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 32643*	Express the preimage of a function operation as a union of preimages. This version of ofpreima 32642 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶))    ⇒   ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
Theorem	funcnvmpt 32644*	Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵))
Theorem	funcnv5mpt 32645*	Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶)))
Theorem	funcnv4mpt 32646*	Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)))
Theorem	preimane 32647	Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐹)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌}))
Theorem	fnpreimac 32648*	Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
Theorem	fgreu 32649*	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 32650*	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 32651*	The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷)
Theorem	mptssALT 32652*	Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 5991. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	dfcnv2 32653*	Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.)
⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥})))
21.3.4.3  Operations - misc additions
Theorem	mpomptxf 32654*	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 32655	Function operation with the empty function. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ (𝐹 ∘f 𝑅∅) = ∅
21.3.4.4  The mapping operation
Theorem	elmaprd 32656	Deduction associated with elmapd 8764. Reverse direction of elmapdd 8765. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
21.3.4.5  Support of a function
Theorem	suppovss 32657*	A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍)))
Theorem	elsuppfnd 32658	Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝐹‘𝑋) ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐹 supp 𝑍))
Theorem	fisuppov1 32659*	Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 0 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐸)    &   ⊢ (𝜑 → 𝐹 finSupp 0 )    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ( 0 𝑂𝑦) = 𝑍)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ ((𝐹‘𝑥)𝑂𝐵)) finSupp 𝑍)
Theorem	suppun2 32660	The support of a union is the union of the supports. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) = ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍)))
Theorem	fdifsupp 32661	Express the support of a function 𝐹 outside of 𝐵 in two different ways. (Contributed by Thierry Arnoux, 5-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∖ 𝐵)) supp 𝑍) = ((𝐹 supp 𝑍) ∖ 𝐵))
Theorem	suppiniseg 32662	Relation between the support (𝐹 supp 𝑍) and the initial segment (◡𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍}))
Theorem	fsuppinisegfi 32663	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 32664	The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍})))
Theorem	fdifsuppconst 32665	A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024.)
⊢ 𝐴 = (dom 𝐹 ∖ (𝐹 supp 𝑍))    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ 𝐴) = (𝐴 × {𝑍}))
Theorem	ressupprn 32666	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 32667	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 32668	Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024.)
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin)
Theorem	mptiffisupp 32669*	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 32670	Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐷)    ⇒   ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐷⟩}) = ∅)
Theorem	cosnop 32671	Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐶, 𝐴⟩}) = {⟨𝐶, 𝐵⟩})
Theorem	cnvprop 32672	Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {⟨𝐵, 𝐴⟩, ⟨𝐷, 𝐶⟩})
Theorem	brprop 32673	Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷))))
Theorem	mptprop 32674*	Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷)))
Theorem	coprprop 32675	Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ≠ 𝐹)    ⇒   ⊢ (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩})
Theorem	fmptunsnop 32676*	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 32677	Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵)))
Theorem	isoun 32678*	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 32679*	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 6550) (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 32680*	Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥)
Theorem	df2ndres 32681*	Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦)
Theorem	1stpreimas 32682	The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.)
⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋})))
Theorem	1stpreima 32683	The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶))
Theorem	2ndpreima 32684	The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴))
Theorem	curry2ima 32685*	The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)})
Theorem	preiman0 32686	The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ 𝐴) ≠ ∅)
Theorem	intimafv 32687*	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  Finite Sets
Theorem	imafi2 32688	The image by a finite set is finite. See also imafi 9199. (Contributed by Thierry Arnoux, 25-Apr-2020.)
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin)
Theorem	unifi3 32689	If a union is finite, then all its elements are finite. See unifi 9228. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin)
21.3.4.11  Countable Sets
Theorem	snct 32690	A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω)
Theorem	prct 32691	An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω)
Theorem	mpocti 32692*	An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉    ⇒   ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	abrexct 32693*	An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω)
Theorem	mptctf 32694	A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω)
Theorem	abrexctf 32695*	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 32696*	Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
Theorem	f1od2 32697*	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 32698*	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 32699*	Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9292. (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 32700*	Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also fcobijfs 32699 and mapfien 9292. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐺:𝑅–1-1-onto→𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑇)    &   ⊢ 𝑋 = {𝑔 ∈ (𝑇 ↑m 𝑆) ∣ 𝑔 finSupp 𝑂}    &   ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑m 𝑅) ∣ ℎ finSupp 𝑂}    ⇒   ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝑓 ∘ 𝐺)):𝑋–1-1-onto→𝑌)