Home | Metamath
Proof Explorer Theorem List (p. 320 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssltex1 31901 | The first argument of surreal set less than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | ssltex2 31902 | The second argument of surreal set less than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | ssltss1 31903 | The first argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | ssltss2 31904 | The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | ssltsep 31905* | The separation property of surreal set less than. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | sssslt1 31906 | Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
Theorem | sssslt2 31907 | Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.) |
Theorem | nulsslt 31908 | The empty set is less than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | nulssgt 31909 | The empty set is greater than any set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | conway 31910* | Conway's Simplicity Theorem. Given preceeding , there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | scutval 31911* | The value of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | scutcut 31912 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | scutbday 31913* | The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | sslttr 31914 | Transitive law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
Theorem | ssltun1 31915 | Union law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
Theorem | ssltun2 31916 | Union law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
Theorem | scutun12 31917 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
Theorem | dmscut 31918 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
Theorem | scutf 31919 | Functionhood statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
Theorem | etasslt 31920* | A restatement of noeta 31868 using set less than. (Contributed by Scott Fenton, 10-Dec-2021.) |
Theorem | scutbdaybnd 31921 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
Theorem | scutbdaylt 31922 | If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021.) |
Theorem | slerec 31923* | A comparison law for surreals considered as cuts of sets of surreals. In Conway's treatment, this is the definition of less than or equal. (Contributed by Scott Fenton, 11-Dec-2021.) |
Theorem | sltrec 31924* | A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021.) |
Syntax | cmade 31925 | Declare the symbol for the made by function. |
M | ||
Syntax | cold 31926 | Declare the symbol for the older than function. |
O | ||
Syntax | cnew 31927 | Declare the symbol for the new on function. |
N | ||
Syntax | cleft 31928 | Declare the symbol for the left option function. |
L | ||
Syntax | cright 31929 | Declare the symbol for the right option function. |
R | ||
Definition | df-made 31930 | Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. (Contributed by Scott Fenton, 17-Dec-2021.) |
M recs | ||
Definition | df-old 31931 | Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. (Contributed by Scott Fenton, 17-Dec-2021.) |
O M | ||
Definition | df-new 31932 | Define the newer than function. This function carries an ordinal to all surreals made on that day. (Contributed by Scott Fenton, 17-Dec-2021.) |
N O M | ||
Definition | df-left 31933* | Define the left options of a surreal. This is the set of surreals that are "closest" on the left to the given surreal. (Contributed by Scott Fenton, 17-Dec-2021.) |
L O | ||
Definition | df-right 31934* | Define the left options of a surreal. This is the set of surreals that are "closest" on the right to the given surreal. (Contributed by Scott Fenton, 17-Dec-2021.) |
R O | ||
Theorem | madeval 31935 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
M M M | ||
Theorem | madeval2 31936* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
M M M | ||
Syntax | ctxp 31937 | Declare the syntax for tail Cartesian product. |
Syntax | cpprod 31938 | Declare the syntax for the parallel product. |
pprod | ||
Syntax | csset 31939 | Declare the subset relationship class. |
Syntax | ctrans 31940 | Declare the transitive set class. |
Syntax | cbigcup 31941 | Declare the set union relationship. |
Syntax | cfix 31942 | Declare the syntax for the fixpoints of a class. |
Syntax | climits 31943 | Declare the class of limit ordinals. |
Syntax | cfuns 31944 | Declare the syntax for the class of all function. |
Syntax | csingle 31945 | Declare the syntax for the singleton function. |
Singleton | ||
Syntax | csingles 31946 | Declare the syntax for the class of all singletons. |
Syntax | cimage 31947 | Declare the syntax for the image functor. |
Image | ||
Syntax | ccart 31948 | Declare the syntax for the cartesian function. |
Cart | ||
Syntax | cimg 31949 | Declare the syntax for the image function. |
Img | ||
Syntax | cdomain 31950 | Declare the syntax for the domain function. |
Domain | ||
Syntax | crange 31951 | Declare the syntax for the range function. |
Range | ||
Syntax | capply 31952 | Declare the syntax for the application function. |
Apply | ||
Syntax | ccup 31953 | Declare the syntax for the cup function. |
Cup | ||
Syntax | ccap 31954 | Declare the syntax for the cap function. |
Cap | ||
Syntax | csuccf 31955 | Declare the syntax for the successor function. |
Succ | ||
Syntax | cfunpart 31956 | Declare the syntax for the functional part functor. |
Funpart | ||
Syntax | cfullfn 31957 | Declare the syntax for the full function functor. |
FullFun | ||
Syntax | crestrict 31958 | Declare the syntax for the restriction function. |
Restrict | ||
Syntax | cub 31959 | Declare the syntax for the upper bound relationship functor. |
UB | ||
Syntax | clb 31960 | Declare the syntax for the lower bound relationship functor. |
LB | ||
Definition | df-txp 31961 | Define the tail cross of two classes. Membership in this class is defined by txpss3v 31985 and brtxp 31987. (Contributed by Scott Fenton, 31-Mar-2012.) |
Definition | df-pprod 31962 | Define the parallel product of two classes. Membership in this class is defined by pprodss4v 31991 and brpprod 31992. (Contributed by Scott Fenton, 11-Apr-2014.) |
pprod | ||
Definition | df-sset 31963 | Define the subset class. For the value, see brsset 31996. (Contributed by Scott Fenton, 31-Mar-2012.) |
Definition | df-trans 31964 | Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
Definition | df-bigcup 31965 | Define the Bigcup function, which, per fvbigcup 32009, carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012.) |
Definition | df-fix 31966 | Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
Definition | df-limits 31967 | Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
Definition | df-funs 31968 | Define the class of all functions. See elfuns 32022 for membership. (Contributed by Scott Fenton, 18-Feb-2013.) |
Definition | df-singleton 31969 | Define the singleton function. See brsingle 32024 for its value. (Contributed by Scott Fenton, 4-Apr-2014.) |
Singleton | ||
Definition | df-singles 31970 | Define the class of all singletons. See elsingles 32025 for membership. (Contributed by Scott Fenton, 19-Feb-2013.) |
Singleton | ||
Definition | df-image 31971 | Define the image functor. This function takes a set to a function , providing that the latter exists. See imageval 32037 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.) |
Image | ||
Definition | df-cart 31972 | Define the cartesian product function. See brcart 32039 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
Cart pprod | ||
Definition | df-img 31973 | Define the image function. See brimg 32044 for its value. (Contributed by Scott Fenton, 12-Apr-2014.) |
Img Image Cart | ||
Definition | df-domain 31974 | Define the domain function. See brdomain 32040 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
Domain Image | ||
Definition | df-range 31975 | Define the range function. See brrange 32041 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
Range Image | ||
Definition | df-cup 31976 | Define the little cup function. See brcup 32046 for its value. (Contributed by Scott Fenton, 14-Apr-2014.) |
Cup | ||
Definition | df-cap 31977 | Define the little cap function. See brcap 32047 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
Cap | ||
Definition | df-restrict 31978 | Define the restriction function. See brrestrict 32056 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
Restrict Cap Cart Range | ||
Definition | df-succf 31979 | Define the successor function. See brsuccf 32048 for its value. (Contributed by Scott Fenton, 14-Apr-2014.) |
Succ Cup Singleton | ||
Definition | df-apply 31980 | Define the application function. See brapply 32045 for its value. (Contributed by Scott Fenton, 12-Apr-2014.) |
Apply Singleton Img pprod Singleton | ||
Definition | df-funpart 31981 | Define the functional part of a class . This is the maximal part of that is a function. See funpartfun 32050 and funpartfv 32052 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.) |
Funpart Image Singleton | ||
Definition | df-fullfun 31982 | Define the full function over . This is a function with domain that always agrees with for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
FullFun Funpart Funpart | ||
Definition | df-ub 31983 | Define the upper bound relationship functor. See brub 32061 for value. (Contributed by Scott Fenton, 3-May-2018.) |
UB | ||
Definition | df-lb 31984 | Define the lower bound relationship functor. See brlb 32062 for value. (Contributed by Scott Fenton, 3-May-2018.) |
LB UB | ||
Theorem | txpss3v 31985 | A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | txprel 31986 | A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | brtxp 31987 | Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 31985, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | brtxp2 31988* | 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.) |
Theorem | dfpprod2 31989 | Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.) |
pprod | ||
Theorem | pprodcnveq 31990 | A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.) |
pprod pprod | ||
Theorem | pprodss4v 31991 | The parallel product is a subclass of . (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
pprod | ||
Theorem | brpprod 31992 | Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 31991, this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
pprod | ||
Theorem | brpprod3a 31993* | 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.) |
pprod | ||
Theorem | brpprod3b 31994* | Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014.) |
pprod | ||
Theorem | relsset 31995 | The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | brsset 31996 | For sets, the binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | idsset 31997 | is equal to the intersection of and its converse. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | eltrans 31998 | Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
Theorem | dfon3 31999 | A quantifier-free definition of . (Contributed by Scott Fenton, 5-Apr-2012.) |
Theorem | dfon4 32000 | Another quantifier-free definition of . (Contributed by Scott Fenton, 4-May-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |