P. 289 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28801-28900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brelg 28801	Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017.)
⊢ ((𝑅 ⊆ (𝐶 × 𝐷) ∧ 𝐴𝑅𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
Theorem	br8d 28802*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by Thierry Arnoux, 21-Mar-2019.)
⊢ (𝑎 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑏 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑐 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑑 = 𝐷 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑒 = 𝐸 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑓 = 𝐹 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑔 = 𝐺 → (𝜎 ↔ 𝜌))    &   ⊢ (ℎ = 𝐻 → (𝜌 ↔ 𝜇))    &   ⊢ (𝜑 → 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)})    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜇))
Theorem	opabdm 28803*	Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → dom 𝑅 = {𝑥 ∣ ∃𝑦𝜑})
Theorem	opabrn 28804*	Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → ran 𝑅 = {𝑦 ∣ ∃𝑥𝜑})
Theorem	ssrelf 28805*	A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Thierry Arnoux, 6-Nov-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Theorem	eqrelrd2 28806*	A version of eqrelrdv2 5142 with explicit non-free declarations. (Contributed by Thierry Arnoux, 28-Aug-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	erbr3b 28807	Biconditional for equivalent elements. (Contributed by Thierry Arnoux, 6-Jan-2020.)
⊢ ((𝑅 Er 𝑋 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
Theorem	iunsnima 28808	Image of a singleton by an indexed union involving that singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑥}) = 𝐵)
21.3.4.2  Functions - misc additions
Theorem	mptexgf 28809	If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.) (Revised by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V)
Theorem	ac6sf2 28810*	Alternate version of ac6 9185 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008.) (Revised by Thierry Arnoux, 17-May-2020.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	idssxp 28811	A diagonal set as a subset of a Cartesian product. (Contributed by Thierry Arnoux, 29-Dec-2019.)
⊢ ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)
Theorem	fnresin 28812	Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐵) Fn (𝐴 ∩ 𝐵))
Theorem	f1o3d 28813*	Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷)))
Theorem	rinvf1o 28814	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 28815	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	f1mptrn 28816*	Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃!𝑥 ∈ 𝐴 𝑦 = 𝐵)    ⇒   ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵))
Theorem	dfimafnf 28817*	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 28818	Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	suppss2f 28819*	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	fovcld 28820	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Revised by Thierry Arnoux, 17-Feb-2017.)
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
Theorem	ofrn 28821	The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ 𝐶)
Theorem	ofrn2 28822	The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺)))
Theorem	off2 28823*	The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺):𝐶⟶𝑈)
Theorem	ofresid 28824	Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝐹 ∘𝑓 (𝑅 ↾ (𝐵 × 𝐵))𝐺))
Theorem	fimarab 28825*	Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝐹 “ 𝑋) = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑦})
Theorem	unipreima 28826*	Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.)
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥))
Theorem	sspreima 28827	The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ 𝐵) → (◡𝐹 “ 𝐴) ⊆ (◡𝐹 “ 𝐵))
Theorem	opfv 28828	Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.)
⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = ⟨((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)⟩)
Theorem	xppreima 28829	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	xppreima2 28830*	The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍)))
Theorem	elunirn2 28831	Condition for the membership in the union of the range of a function. (Contributed by Thierry Arnoux, 13-Nov-2016.)
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (𝐹‘𝐴)) → 𝐵 ∈ ∪ ran 𝐹)
Theorem	abfmpunirn 28832*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓))
Theorem	rabfmpunirn 28833*	Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑})    &   ⊢ 𝑊 ∈ V    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓))
Theorem	abfmpeld 28834*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓})    &   ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V)    &   ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒)))
Theorem	abfmpel 28835*	Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑})    &   ⊢ {𝑦 ∣ 𝜑} ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓))
Theorem	fmptdF 28836	Domain and co-domain of the mapping operation; deduction form. This version of fmptd 6292 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	mpteq12df 28837	An equality theorem for the maps to notation. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
Theorem	resmptf 28838	Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	fmptcof2 28839*	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 28840*	Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 6306. (Contributed by Thierry Arnoux, 30-Jun-2017.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥))))
Theorem	acunirnmpt 28841*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵))
Theorem	acunirnmpt2 28842*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))
Theorem	acunirnmpt2f 28843*	Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑗𝐶    &   ⊢ Ⅎ𝑗𝐷    &   ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵    &   ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))
Theorem	aciunf1lem 28844*	Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥))
Theorem	aciunf1 28845*	Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘))
Theorem	cofmpt 28846*	Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
⊢ (𝜑 → 𝐹:𝐶⟶𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)))
Theorem	ofoprabco 28847*	Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ Ⅎ𝑎𝑀    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ ⟨(𝐹‘𝑎), (𝐺‘𝑎)⟩))    &   ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑁 ∘ 𝑀))
Theorem	ofpreima 28848*	Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶))    ⇒   ⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
Theorem	ofpreima2 28849*	Express the preimage of a function operation as a union of preimages. This version of ofpreima 28848 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶))    ⇒   ⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
Theorem	funcnvmptOLD 28850*	Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)))
Theorem	funcnvmpt 28851*	Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵))
Theorem	funcnv5mpt 28852*	Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶)))
Theorem	funcnv4mpt 28853*	Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵)))
Theorem	fgreu 28854*	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 28855*	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	rnmpt2ss 28856*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷)
Theorem	mptssALT 28857*	Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 5373. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	partfun 28858	Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. (Contributed by Thierry Arnoux, 30-Mar-2017.)
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷))
Theorem	dfcnv2 28859*	Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.)
⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥})))
21.3.4.3  Operations - misc additions
Theorem	mpt2mptxf 28860*	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.)
⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
21.3.4.4  Isomorphisms - misc. add.
Theorem	gtiso 28861	Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵)))
Theorem	isoun 28862*	Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017.)
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥𝑅𝑦)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷) → 𝑧𝑆𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑥𝑅𝑦)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑧𝑆𝑤)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅)    ⇒   ⊢ (𝜑 → (𝐻 ∪ 𝐺) Isom 𝑅, 𝑆 ((𝐴 ∪ 𝐶), (𝐵 ∪ 𝐷)))
21.3.4.5  Disjointness (additional proof requiring functions)
Theorem	disjdsct 28863*	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 5872) (Contributed by Thierry Arnoux, 28-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅}))    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵))
21.3.4.6  First and second members of an ordered pair - misc additions
Theorem	df1stres 28864*	Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥)
Theorem	df2ndres 28865*	Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦)
Theorem	1stpreimas 28866	The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.)
⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋})))
Theorem	1stpreima 28867	The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶))
Theorem	2ndpreima 28868	The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴))
Theorem	curry2ima 28869*	The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶})))    ⇒   ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)})
21.3.4.7  Supremum - misc additions
Theorem	supssd 28870*	Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅))
Theorem	infssd 28871*	Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ¬ inf(𝐶, 𝐴, 𝑅)𝑅inf(𝐵, 𝐴, 𝑅))
21.3.4.8  Finite Sets
Theorem	imafi2 28872	The image by a finite set is finite. See also imafi 8142. (Contributed by Thierry Arnoux, 25-Apr-2020.)
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin)
Theorem	unifi3 28873	If a union is finite, then all its elements are finite. See unifi 8138. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin)
21.3.4.9  Countable Sets
Theorem	snct 28874	A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω)
Theorem	prct 28875	An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω)
Theorem	fnct 28876	If the domain of a function is countable, the function is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹 ≼ ω)
Theorem	dmct 28877	The domain of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → dom 𝐴 ≼ ω)
Theorem	cnvct 28878	If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω)
Theorem	rnct 28879	The range of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → ran 𝐴 ≼ ω)
Theorem	mptct 28880*	A countable mapping set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω)
Theorem	mpt2cti 28881*	An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉    ⇒   ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	abrexct 28882*	An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω)
Theorem	mptctf 28883	A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω)
Theorem	abrexctf 28884*	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 28885*	Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))
Theorem	cnvoprab 28886*	The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜑))    &   ⊢ (𝜓 → 𝑎 ∈ (V × V))    ⇒   ⊢ ◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑧, 𝑎⟩ ∣ 𝜓}
Theorem	f1od2 28887*	Describe an implicit one-to-one onto function of two variables. (Contributed by Thierry Arnoux, 17-Aug-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))    &   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)
Theorem	fcobij 28888*	Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017.)
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑓 ∈ (𝑆 ↑𝑚 𝑅) ↦ (𝐺 ∘ 𝑓)):(𝑆 ↑𝑚 𝑅)–1-1-onto→(𝑇 ↑𝑚 𝑅))
Theorem	fcobijfs 28889*	Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 8196. (Contributed by Thierry Arnoux, 25-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑆)    &   ⊢ 𝑄 = (𝐺‘𝑂)    &   ⊢ 𝑋 = {𝑔 ∈ (𝑆 ↑𝑚 𝑅) ∣ 𝑔 finSupp 𝑂}    &   ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑𝑚 𝑅) ∣ ℎ finSupp 𝑄}    ⇒   ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝐺 ∘ 𝑓)):𝑋–1-1-onto→𝑌)
Theorem	suppss3 28890*	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	ffs2 28891	Rewrite a function's support based with its range rather than the universal class. See also frnsuppeq 7194. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐶 = (𝐵 ∖ {𝑍})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 supp 𝑍) = (◡𝐹 “ 𝐶))
Theorem	ffsrn 28892	The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ Fin)
Theorem	resf1o 28893*	Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.)
⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶}    &   ⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶))    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑𝑚 𝐶))
Theorem	maprnin 28894*	Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ∩ 𝐶) ↑𝑚 𝐴) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ ran 𝑓 ⊆ 𝐶}
Theorem	fpwrelmapffslem 28895*	Lemma for fpwrelmapffs 28897. 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 28896*	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 9153 and marypha2lem1 8224. (Contributed by Thierry Arnoux, 28-Aug-2017.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})    ⇒   ⊢ 𝑀:(𝒫 𝐵 ↑𝑚 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)
Theorem	fpwrelmapffs 28897*	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    &   ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})    &   ⊢ 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑𝑚 𝐴) ∣ (𝑓 supp ∅) ∈ Fin}    ⇒   ⊢ (𝑀 ↾ 𝑆):𝑆–1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin)
21.3.5  Real and Complex Numbers
21.3.5.1  Complex operations - misc. additions
Theorem	addeq0 28898	Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) = 0 ↔ 𝐴 = -𝐵))
Theorem	subeqxfrd 28899	Transfer two terms of a subtraction in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐷))
Theorem	znsqcld 28900	Squaring of nonzero relative numbers. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑁↑2) ∈ ℕ)