P. 312 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31101-31200   *Has distinct variable group(s)

Type	Label	Description
Statement
21.8.26  Surreal Numbers: Full-Eta Property
Theorem	nofulllem1 31101*	Lemma for nofull (future) . The full statement of the axiom when 𝑅 is empty. (Contributed by Scott Fenton, 3-Aug-2011.)
⊢ (𝑅 = ∅ → (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∃𝑧 ∈ No (∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday ‘𝑧) ⊆ suc ∪ ( bday “ (𝐿 ∪ 𝑅)))))
Theorem	nofulllem2 31102*	Lemma for nofull (future) . The full statement of the axiom when 𝐿 is empty. (Contributed by Scott Fenton, 3-Aug-2011.)
⊢ (𝐿 = ∅ → (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∃𝑧 ∈ No (∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday ‘𝑧) ⊆ suc ∪ ( bday “ (𝐿 ∪ 𝑅)))))
Theorem	nofulllem3 31103	Lemma for nofull (future) . Restriction of surreal number to a superset of its birthday does not change anything. (Contributed by Scott Fenton, 25-Apr-2017.)
⊢ ((𝐴 ⊆ No ∧ 𝑋 ∈ 𝐴 ∧ 𝐴 ⊆ 𝑆) → (𝑋 ↾ ∪ ( bday “ 𝑆)) = 𝑋)
Theorem	nofulllem4 31104*	Lemma for nofull (future) . Show a particular abstraction is an ordinal. (Contributed by Scott Fenton, 25-Apr-2017.)
⊢ 𝑀 = ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}    ⇒   ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On)
Theorem	nofulllem5 31105*	Lemma for nofull (future) . Here, we introduce a new surreal number 𝑋. Eventually, we will show that either 𝑋 or a related surreal number has the required properties for the final theorem. We begin by calculating the domain of 𝑋. (Contributed by Scott Fenton, 1-May-2017.)
⊢ 𝑀 = ∩ {𝑎 ∈ On ∣ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 (𝑥 ↾ 𝑎) ≠ (𝑦 ↾ 𝑎)}    &   ⊢ 𝑆 = {𝑓 ∣ ∃𝑔 ∈ 𝐿 ∃ℎ ∈ 𝑅 ∃𝑎 ∈ 𝑀 ((𝑔 ↾ 𝑎) = 𝑓 ∧ (ℎ ↾ 𝑎) = 𝑓)}    &   ⊢ 𝑋 = ∪ 𝑆    ⇒   ⊢ (((𝐿 ⊆ No ∧ 𝐿 ∈ 𝑉) ∧ (𝑅 ⊆ No ∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → dom 𝑋 = ∪ 𝑀)
21.8.27  Quantifier-free definitions
Syntax	ctxp 31106	Declare the syntax for tail Cartesian product.
class (𝐴 ⊗ 𝐵)
Syntax	cpprod 31107	Declare the syntax for the parallel product.
class pprod(𝑅, 𝑆)
Syntax	csset 31108	Declare the subset relationship class.
class SSet
Syntax	ctrans 31109	Declare the transitive set class.
class Trans
Syntax	cbigcup 31110	Declare the set union relationship.
class Bigcup
Syntax	cfix 31111	Declare the syntax for the fixpoints of a class.
class Fix 𝐴
Syntax	climits 31112	Declare the class of limit ordinals.
class Limits
Syntax	cfuns 31113	Declare the syntax for the class of all function.
class Funs
Syntax	csingle 31114	Declare the syntax for the singleton function.
class Singleton
Syntax	csingles 31115	Declare the syntax for the class of all singletons.
class Singletons
Syntax	cimage 31116	Declare the syntax for the image functor.
class Image𝐴
Syntax	ccart 31117	Declare the syntax for the cartesian function.
class Cart
Syntax	cimg 31118	Declare the syntax for the image function.
class Img
Syntax	cdomain 31119	Declare the syntax for the domain function.
class Domain
Syntax	crange 31120	Declare the syntax for the range function.
class Range
Syntax	capply 31121	Declare the syntax for the application function.
class Apply
Syntax	ccup 31122	Declare the syntax for the cup function.
class Cup
Syntax	ccap 31123	Declare the syntax for the cap function.
class Cap
Syntax	csuccf 31124	Declare the syntax for the successor function.
class Succ
Syntax	cfunpart 31125	Declare the syntax for the functional part functor.
class Funpart𝐹
Syntax	cfullfn 31126	Declare the syntax for the full function functor.
class FullFun𝐹
Syntax	crestrict 31127	Declare the syntax for the restriction function.
class Restrict
Syntax	cub 31128	Declare the syntax for the upper bound relationship functor.
class UB𝑅
Syntax	clb 31129	Declare the syntax for the lower bound relationship functor.
class LB𝑅
Definition	df-txp 31130	Define the tail cross of two classes. Membership in this class is defined by txpss3v 31155 and brtxp 31157. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Definition	df-pprod 31131	Define the parallel product of two classes. Membership in this class is defined by pprodss4v 31161 and brpprod 31162. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Definition	df-sset 31132	Define the subset class. For the value, see brsset 31166. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
Definition	df-trans 31133	Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Definition	df-bigcup 31134	Define the Bigcup function, which, per fvbigcup 31179, 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 31135	Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Fix 𝐴 = dom (𝐴 ∩ I )
Definition	df-limits 31136	Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
Definition	df-funs 31137	Define the class of all functions. See elfuns 31192 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
Definition	df-singleton 31138	Define the singleton function. See brsingle 31194 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V)))
Definition	df-singles 31139	Define the class of all singletons. See elsingles 31195 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ Singletons = ran Singleton
Definition	df-image 31140	Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 31207 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)))
Definition	df-cart 31141	Define the cartesian product function. See brcart 31209 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
Definition	df-img 31142	Define the image function. See brimg 31214 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Definition	df-domain 31143	Define the domain function. See brdomain 31210 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Domain = Image(1st ↾ (V × V))
Definition	df-range 31144	Define the range function. See brrange 31211 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Range = Image(2nd ↾ (V × V))
Definition	df-cup 31145	Define the little cup function. See brcup 31216 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 31146	Define the little cap function. See brcap 31217 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 31147	Define the restriction function. See brrestrict 31226 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
Definition	df-succf 31148	Define the successor function. See brsuccf 31218 for its value. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ Succ = (Cup ∘ ( I ⊗ Singleton))
Definition	df-apply 31149	Define the application function. See brapply 31215 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 31150	Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 31220 and funpartfv 31222 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
Definition	df-fullfun 31151	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 31152	Define the upper bound relationship functor. See brub 31231 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))
Definition	df-lb 31153	Define the lower bound relationship functor. See brlb 31232 for value. (Contributed by Scott Fenton, 3-May-2018.)
⊢ LB𝑅 = UB◡𝑅
Theorem	brv 31154	The binary relationship over V always holds. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴V𝐵
Theorem	txpss3v 31155	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 31156	A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel (𝐴 ⊗ 𝐵)
Theorem	brtxp 31157	Characterize a trinary relationship over a tail Cartesian product. Together with txpss3v 31155, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ (𝑋(𝐴 ⊗ 𝐵)⟨𝑌, 𝑍⟩ ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍))
Theorem	brtxp2 31158*	The binary relationship 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 31159	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 31160	A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.)
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆)
Theorem	pprodss4v 31161	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.)
⊢ pprod(𝐴, 𝐵) ⊆ ((V × V) × (V × V))
Theorem	brpprod 31162	Characterize a quatary relationship over a tail Cartesian product. Together with pprodss4v 31161, 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 31163*	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 31164*	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 31165	The subset class is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Rel SSet
Theorem	brsset 31166	For sets, the SSet binary relationship is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵)
Theorem	idsset 31167	I is equal to SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ I = ( SSet ∩ ◡ SSet )
Theorem	eltrans 31168	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴)
Theorem	dfon3 31169	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E )))
Theorem	dfon4 31170	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans ))
Theorem	brtxpsd 31171*	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 31172*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴))
Theorem	brtxpsd3 31173*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    &   ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴)    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋)
Theorem	relbigcup 31174	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel Bigcup
Theorem	brbigcup 31175	Binary relationship over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵)
Theorem	dfbigcup2 31176	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥)
Theorem	fobigcup 31177	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup :V–onto→V
Theorem	fnbigcup 31178	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup Fn V
Theorem	fvbigcup 31179	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴
Theorem	elfix 31180	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	elfix2 31181	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	dffix2 31182	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = ran (𝐴 ∩ I )
Theorem	fixssdm 31183	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ dom 𝐴
Theorem	fixssrn 31184	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ ran 𝐴
Theorem	fixcnv 31185	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = Fix ◡𝐴
Theorem	fixun 31186	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵)
Theorem	ellimits 31187	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴)
Theorem	limitssson 31188	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 31189	A quantifier-free definition of ω that does not depend on ax-inf 8418. (Note: label was changed from dfom5 8430 to dfom5b 31189 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ ω = (On ∩ ∩ Limits )
Theorem	sscoid 31190	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵))
Theorem	dffun10 31191	Another potential definition of functionhood. 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 31192	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)
Theorem	elfunsg 31193	Closed form of elfuns 31192. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 31194	The binary relationship form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Singleton𝐵 ↔ 𝐵 = {𝐴})
Theorem	elsingles 31195*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 31196	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 31197	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 31198*	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 31199	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ Singletons
Theorem	dfiota3 31200	A definiton of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons )