P. 363 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36201-36300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	csuccf 36201	Declare the syntax for the successor function.
class Succ
Syntax	cfunpart 36202	Declare the syntax for the functional part functor.
class Funpart𝐹
Syntax	cfullfn 36203	Declare the syntax for the full function functor.
class FullFun𝐹
Syntax	crestrict 36204	Declare the syntax for the restriction function.
class Restrict
Syntax	cub 36205	Declare the syntax for the upper bound relationship functor.
class UB𝑅
Syntax	clb 36206	Declare the syntax for the lower bound relationship functor.
class LB𝑅
Definition	df-txp 36207	Define the tail cross of two classes. Membership in this class is defined by txpss3v 36231 and brtxp 36233. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Definition	df-pprod 36208	Define the parallel product of two classes. Membership in this class is defined by pprodss4v 36237 and brpprod 36238. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Definition	df-sset 36209	Define the subset class. For the value, see brsset 36242. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
Definition	df-trans 36210	Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Definition	df-bigcup 36211	Define the Bigcup function, which, per fvbigcup 36255, carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ E ) ⊗ V)))
Definition	df-fix 36212	Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Fix 𝐴 = dom (𝐴 ∩ I )
Definition	df-limits 36213	Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
Definition	df-funs 36214	Define the class of all functions. See elfuns 36268 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
Definition	df-singleton 36215	Define the singleton function. See brsingle 36270 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V)))
Definition	df-singles 36216	Define the class of all singletons. See elsingles 36271 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ Singletons = ran Singleton
Definition	df-image 36217	Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 36283 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)))
Definition	df-cart 36218	Define the cartesian product function. See brcart 36285 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
Definition	df-img 36219	Define the image function. See brimg 36290 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Definition	df-domain 36220	Define the domain function. See brdomain 36286 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Domain = Image(1st ↾ (V × V))
Definition	df-range 36221	Define the range function. See brrange 36287 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Range = Image(2nd ↾ (V × V))
Definition	df-cup 36222	Define the little cup function. See brcup 36292 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Cup = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∪ (◡2nd ∘ E )) ⊗ V)))
Definition	df-cap 36223	Define the little cap function. See brcap 36293 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Cap = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∩ (◡2nd ∘ E )) ⊗ V)))
Definition	df-restrict 36224	Define the restriction function. See brrestrict 36304 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
Definition	df-succf 36225	Define the successor function. See its alternate version dfsuccf2 36296. See brsuccf 36295 for its value. Cf. the equivalent df-sucmap 38966 family. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Succ = (Cup ∘ ( I ⊗ Singleton))
Definition	df-apply 36226	Define the application function. See brapply 36291 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Apply = (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
Definition	df-funpart 36227	Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 36298 and funpartfv 36300 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
Definition	df-fullfun 36228	Define the full function over 𝐹. This is a function with domain V that always agrees with 𝐹 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ FullFun𝐹 = (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅}))
Definition	df-ub 36229	Define the upper bound relationship functor. See brub 36309 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))
Definition	df-lb 36230	Define the lower bound relationship functor. See brlb 36310 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ LB𝑅 = UB◡𝑅
Theorem	txpss3v 36231	A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) ⊆ (V × (V × V))
Theorem	txprel 36232	A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⊗ 𝐵)
Theorem	brtxp 36233	Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 36231, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋(𝐴 ⊗ 𝐵)⟨𝑌, 𝑍⟩ ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍))
Theorem	brtxp2 36234*	The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴(𝑅 ⊗ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = ⟨𝑥, 𝑦⟩ ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦))
Theorem	dfpprod2 36235	Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝐴, 𝐵) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V)))))
Theorem	pprodcnveq 36236	A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆)
Theorem	pprodss4v 36237	The parallel product is a subclass of ((V × V) × (V × V)). (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ pprod(𝐴, 𝐵) ⊆ ((V × V) × (V × V))
Theorem	brpprod 36238	Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 36237, this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    &   ⊢ 𝑊 ∈ V    ⇒   ⊢ (⟨𝑋, 𝑌⟩pprod(𝐴, 𝐵)⟨𝑍, 𝑊⟩ ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊))
Theorem	brpprod3a 36239*	Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (⟨𝑋, 𝑌⟩pprod(𝑅, 𝑆)𝑍 ↔ ∃𝑧∃𝑤(𝑍 = ⟨𝑧, 𝑤⟩ ∧ 𝑋𝑅𝑧 ∧ 𝑌𝑆𝑤))
Theorem	brpprod3b 36240*	Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋pprod(𝑅, 𝑆)⟨𝑌, 𝑍⟩ ↔ ∃𝑧∃𝑤(𝑋 = ⟨𝑧, 𝑤⟩ ∧ 𝑧𝑅𝑌 ∧ 𝑤𝑆𝑍))
Theorem	relsset 36241	The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel SSet
Theorem	brsset 36242	For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	idsset 36243	I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ I = ( SSet ∩ ◡ SSet )
Theorem	eltrans 36244	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴)
Theorem	dfon3 36245	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E )))
Theorem	dfon4 36246	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans ))
Theorem	brtxpsd 36247*	Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (¬ 𝐴ran ((V ⊗ E ) △ (𝑅 ⊗ V))𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑅𝐴))
Theorem	brtxpsd2 36248*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴))
Theorem	brtxpsd3 36249*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    &   ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴)    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋)
Theorem	relbigcup 36250	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel Bigcup
Theorem	brbigcup 36251	Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵)
Theorem	dfbigcup2 36252	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥)
Theorem	fobigcup 36253	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup :V–onto→V
Theorem	fnbigcup 36254	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup Fn V
Theorem	fvbigcup 36255	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴
Theorem	elfix 36256	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	elfix2 36257	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	dffix2 36258	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = ran (𝐴 ∩ I )
Theorem	fixssdm 36259	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ dom 𝐴
Theorem	fixssrn 36260	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ ran 𝐴
Theorem	fixcnv 36261	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = Fix ◡𝐴
Theorem	fixun 36262	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵)
Theorem	ellimits 36263	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴)
Theorem	limitssson 36264	The class of all limit ordinals is a subclass of the class of all ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits ⊆ On
Theorem	dfom5b 36265	A quantifier-free definition of ω that does not depend on ax-inf 9591. (Note: label was changed from dfom5 9603 to dfom5b 36265 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ ω = (On ∩ ∩ Limits )
Theorem	sscoid 36266	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵))
Theorem	dffun10 36267	Another potential definition of functionality. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.)
⊢ (Fun 𝐹 ↔ 𝐹 ⊆ ( I ∘ (V ∖ ((V ∖ I ) ∘ 𝐹))))
Theorem	elfuns 36268	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)
Theorem	elfunsg 36269	Closed form of elfuns 36268. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 36270	The binary relation form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Singleton𝐵 ↔ 𝐵 = {𝐴})
Theorem	elsingles 36271*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 36272	The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Singleton Fn V
Theorem	fvsingle 36273	The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Revised by Scott Fenton, 13-Apr-2018.)
⊢ (Singleton‘𝐴) = {𝐴}
Theorem	dfsingles2 36274*	Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Singletons = {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}}
Theorem	snelsingles 36275	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ Singletons
Theorem	dfiota3 36276	A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons )
Theorem	dffv5 36277	Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons )
Theorem	unisnif 36278	Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
Theorem	brimage 36279	Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))
Theorem	brimageg 36280	Closed form of brimage 36279. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)))
Theorem	funimage 36281	Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Image𝐴
Theorem	fnimage 36282*	Image𝑅 is a function over the set-like portion of 𝑅. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}
Theorem	imageval 36283*	The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥))
Theorem	fvimage 36284	Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴))
Theorem	brcart 36285	Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cart𝐶 ↔ 𝐶 = (𝐴 × 𝐵))
Theorem	brdomain 36286	Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)
Theorem	brrange 36287	Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)
Theorem	brdomaing 36288	Closed form of brdomain 36286. (Contributed by Scott Fenton, 2-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴))
Theorem	brrangeg 36289	Closed form of brrange 36287. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴))
Theorem	brimg 36290	Binary relation form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Img𝐶 ↔ 𝐶 = (𝐴 “ 𝐵))
Theorem	brapply 36291	Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵))
Theorem	brcup 36292	Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cup𝐶 ↔ 𝐶 = (𝐴 ∪ 𝐵))
Theorem	brcap 36293	Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵))
Theorem	lemsuccf 36294*	Lemma for unfolding different forms of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ 𝐵 = suc 𝐴)
Theorem	brsuccf 36295	Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴)
Theorem	dfsuccf2 36296*	Alternate definition of Scott Fenton's version of Succ, cf. df-sucmap 38966. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ Succ = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	funpartlem 36297*	Lemma for funpartfun 36298. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Theorem	funpartfun 36298	The functional part of 𝐹 is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ Fun Funpart𝐹
Theorem	funpartss 36299	The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Funpart𝐹 ⊆ 𝐹
Theorem	funpartfv 36300	The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (Funpart𝐹‘𝐴) = (𝐹‘𝐴)