P. 354 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35301-35400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-trans 35301	Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Definition	df-bigcup 35302	Define the Bigcup function, which, per fvbigcup 35346, 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 35303	Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Fix 𝐴 = dom (𝐴 ∩ I )
Definition	df-limits 35304	Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
Definition	df-funs 35305	Define the class of all functions. See elfuns 35359 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
Definition	df-singleton 35306	Define the singleton function. See brsingle 35361 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V)))
Definition	df-singles 35307	Define the class of all singletons. See elsingles 35362 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ Singletons = ran Singleton
Definition	df-image 35308	Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 35374 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)))
Definition	df-cart 35309	Define the cartesian product function. See brcart 35376 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
Definition	df-img 35310	Define the image function. See brimg 35381 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Definition	df-domain 35311	Define the domain function. See brdomain 35377 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Domain = Image(1st ↾ (V × V))
Definition	df-range 35312	Define the range function. See brrange 35378 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Range = Image(2nd ↾ (V × V))
Definition	df-cup 35313	Define the little cup function. See brcup 35383 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 35314	Define the little cap function. See brcap 35384 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 35315	Define the restriction function. See brrestrict 35393 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
Definition	df-succf 35316	Define the successor function. See brsuccf 35385 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Succ = (Cup ∘ ( I ⊗ Singleton))
Definition	df-apply 35317	Define the application function. See brapply 35382 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 35318	Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 35387 and funpartfv 35389 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
Definition	df-fullfun 35319	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 35320	Define the upper bound relationship functor. See brub 35398 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))
Definition	df-lb 35321	Define the lower bound relationship functor. See brlb 35399 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ LB𝑅 = UB◡𝑅
Theorem	txpss3v 35322	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 35323	A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⊗ 𝐵)
Theorem	brtxp 35324	Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 35322, 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 35325*	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 35326	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 35327	A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆)
Theorem	pprodss4v 35328	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 35329	Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 35328, 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 35330*	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 35331*	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 35332	The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel SSet
Theorem	brsset 35333	For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	idsset 35334	I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ I = ( SSet ∩ ◡ SSet )
Theorem	eltrans 35335	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴)
Theorem	dfon3 35336	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E )))
Theorem	dfon4 35337	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans ))
Theorem	brtxpsd 35338*	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 35339*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴))
Theorem	brtxpsd3 35340*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    &   ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴)    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋)
Theorem	relbigcup 35341	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel Bigcup
Theorem	brbigcup 35342	Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵)
Theorem	dfbigcup2 35343	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥)
Theorem	fobigcup 35344	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup :V–onto→V
Theorem	fnbigcup 35345	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup Fn V
Theorem	fvbigcup 35346	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴
Theorem	elfix 35347	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	elfix2 35348	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	dffix2 35349	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = ran (𝐴 ∩ I )
Theorem	fixssdm 35350	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ dom 𝐴
Theorem	fixssrn 35351	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ ran 𝐴
Theorem	fixcnv 35352	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = Fix ◡𝐴
Theorem	fixun 35353	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵)
Theorem	ellimits 35354	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴)
Theorem	limitssson 35355	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 35356	A quantifier-free definition of ω that does not depend on ax-inf 9639. (Note: label was changed from dfom5 9651 to dfom5b 35356 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ ω = (On ∩ ∩ Limits )
Theorem	sscoid 35357	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵))
Theorem	dffun10 35358	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 35359	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)
Theorem	elfunsg 35360	Closed form of elfuns 35359. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 35361	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 35362*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 35363	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 35364	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 35365*	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 35366	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ Singletons
Theorem	dfiota3 35367	A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons )
Theorem	dffv5 35368	Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons )
Theorem	unisnif 35369	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 35370	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 35371	Closed form of brimage 35370. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)))
Theorem	funimage 35372	Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Image𝐴
Theorem	fnimage 35373*	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 35374*	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 35375	Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴))
Theorem	brcart 35376	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 35377	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 35378	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 35379	Closed form of brdomain 35377. (Contributed by Scott Fenton, 2-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴))
Theorem	brrangeg 35380	Closed form of brrange 35378. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴))
Theorem	brimg 35381	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 35382	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 35383	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 35384	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	brsuccf 35385	Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴)
Theorem	funpartlem 35386*	Lemma for funpartfun 35387. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Theorem	funpartfun 35387	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 35388	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 35389	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𝐹‘𝐴) = (𝐹‘𝐴)
Theorem	fullfunfnv 35390	The full functional part of 𝐹 is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ FullFun𝐹 Fn V
Theorem	fullfunfv 35391	The function value of the full function of 𝐹 agrees with 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (FullFun𝐹‘𝐴) = (𝐹‘𝐴)
Theorem	brfullfun 35392	A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴FullFun𝐹𝐵 ↔ 𝐵 = (𝐹‘𝐴))
Theorem	brrestrict 35393	Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))
Theorem	dfrecs2 35394	A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.)
⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))
Theorem	dfrdg4 35395	A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))
Theorem	dfint3 35396	Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴))
Theorem	imagesset 35397	The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.)
⊢ Image◡ SSet ⊆ SSet
Theorem	brub 35398*	Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴)
Theorem	brlb 35399*	Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥)
21.10.17  Alternate ordered pairs
Syntax	caltop 35400	Declare the syntax for an alternate ordered pair.
class ⟪𝐴, 𝐵⟫