Home New Foundations ExplorerTheorem List (p. 59 of 64) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 5801-5900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremimageex 5801 The image function of a set is a set. (Contributed by SF, 11-Feb-2015.)
Image

Theoremdmtxp 5802 The domain of a tail cross product is the intersection of the domains of its arguments. (Contributed by SF, 18-Feb-2015.)

Theoremtxpcofun 5803 Composition distributes over tail cross product in the case of a function. (Contributed by SF, 18-Feb-2015.)

Theoremfntxp 5804 If and are functions, then their tail cross product is a function over the intersection of their domains. (Contributed by SF, 24-Feb-2015.)

Theoremotsnelsi3 5805 Ordered triple membership in triple singleton image. (Contributed by SF, 12-Feb-2015.)
SI3

Theoremsi3ex 5806 SI3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
SI3

Theoremreleqel 5807* Lemma to turn a membership condition into an equality condition. (Contributed by SF, 9-Mar-2015.)
Ins3 S Ins2 1c

Theoremreleqmpt 5808* Equality condition for a mapping. (Contributed by SF, 9-Mar-2015.)
Ins3 S Ins2 1c

Theoremreleqmpt2 5809* Equality condition for a mapping operation. (Contributed by SF, 13-Feb-2015.)
Ins2 S Ins3 1c

Theoremmptexlem 5810 Lemma for the existence of a mapping. (Contributed by SF, 9-Mar-2015.)
Ins3 S Ins2 1c

Theoremmpt2exlem 5811 Lemma for the existence of a double mapping. (Contributed by SF, 13-Feb-2015.)
Ins2 S Ins3 1c

Theoremcupvalg 5812 The value of the little cup function. (Contributed by SF, 11-Feb-2015.)
Cup

Theoremfncup 5813 The cup function is a function over the universe. (Contributed by SF, 11-Feb-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
Cup

Theorembrcupg 5814 Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
Cup

Theorembrcup 5815 Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
Cup

Theoremcupex 5816 The little cup function is a set. (Contributed by SF, 11-Feb-2015.)
Cup

Theoremcomposevalg 5817 The value of the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
Compose

Theoremcomposefn 5818 The compose function is a function over the universe. (Contributed by Scott Fenton, 19-Apr-2021.)
Compose

Theorembrcomposeg 5819 Binary relationship form of the compose function. (Contributed by Scott Fenton, 19-Apr-2021.)
Compose

Theoremcomposeex 5820 The compose function is a set. (Contributed by Scott Fenton, 19-Apr-2021.)
Compose

Theorembrdisjg 5821 The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
Disj

Theorembrdisj 5822 The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
Disj

Theoremdisjex 5823 The disjointedness relationship is a set. (Contributed by SF, 11-Feb-2015.)
Disj

Theoremaddcfn 5825 AddC is a function over the universe. (Contributed by SF, 2-Mar-2015.) (Revised by Scott Fenton, 19-Apr-2021.)

Theorembraddcfn 5826 Binary relationship form of the AddC function. (Contributed by SF, 2-Mar-2015.)

Theoremepprc 5827 The membership relationship is a proper class. This theorem together with vvex 4109 demonstrates the basic idea behind New Foundations: since is not a stratified relationship, then it does not have a realization as a set of ordered pairs, but since is stratified, then it does have a realization as a set. (Contributed by SF, 20-Feb-2015.)

Theoremfunsex 5828 The class of all functions forms a set. (Contributed by SF, 18-Feb-2015.)
Funs

Theoremelfuns 5829 Membership in the set of all functions. (Contributed by SF, 23-Feb-2015.)
Funs

Theoremelfunsg 5830 Membership in the set of all functions. (Contributed by Scott Fenton, 31-Jul-2019.)
Funs

Theoremelfunsi 5831 Membership in the set of all functions implies functionhood. (Contributed by Scott Fenton, 31-Jul-2019.)
Funs

Theoremfnsex 5832 The function with domain relationship exists. (Contributed by SF, 23-Feb-2015.)
Fns

Theorembrfns 5833 Binary relationship form of Fns relationship. (Contributed by SF, 23-Feb-2015.)
Fns

Theorempprodeq1 5834 Equality theorem for parallel product. (Contributed by Scott Fenton, 31-Jul-2019.)
PProd PProd

Theorempprodeq2 5835 Equality theorem for parallel product. (Contributed by Scott Fenton, 31-Jul-2019.)
PProd PProd

Theoremqrpprod 5836 A quadratic relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
PProd

Theorempprodexg 5837 The parallel product of two sets is a set. (Contributed by SF, 24-Feb-2015.)
PProd

Theorempprodex 5838 The parallel product of two sets is a set. (Contributed by SF, 24-Feb-2015.)
PProd

Theorembrpprod 5839* Binary relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
PProd

Theoremdmpprod 5840 The domain of a parallel product. (Contributed by SF, 24-Feb-2015.)
PProd

Theoremcnvpprod 5841 The converse of a parallel product. (Contributed by SF, 24-Feb-2015.)
PProd PProd

Theoremrnpprod 5842 The range of a parallel product. (Contributed by SF, 24-Feb-2015.)
PProd

Theoremfnpprod 5843 Functionhood law for parallel product. (Contributed by SF, 24-Feb-2015.)
PProd

Theoremf1opprod 5844 The parallel product of two bijections is a bijection. (Contributed by SF, 24-Feb-2015.)
PProd

Theoremovcross 5845 The value of the cross product function. (Contributed by SF, 24-Feb-2015.)
Cross

Theoremfncross 5846 The cross product function is a function over (Contributed by SF, 24-Feb-2015.)
Cross

Theoremdmcross 5847 The domain of the cross product function. (Contributed by SF, 24-Feb-2015.)
Cross

Theorembrcrossg 5848 Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
Cross

Theorembrcross 5849 Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
Cross

Theoremcrossex 5850 The function mapping and to their cross product is a set. (Contributed by SF, 11-Feb-2015.)
Cross

Theorempw1fnval 5851 The value of the unit power class function. (Contributed by SF, 25-Feb-2015.)
Pw1Fn 1

Theorempw1fnex 5852 The unit power class function is a set. (Contributed by SF, 25-Feb-2015.)
Pw1Fn

Theoremfnpw1fn 5853 Functionhood statement for Pw1Fn (Contributed by SF, 25-Feb-2015.)
Pw1Fn 1c

Theorembrpw1fn 5854 Binary relationship form of Pw1Fn (Contributed by SF, 25-Feb-2015.)
Pw1Fn 1

Theorempw1fnf1o 5855 Pw1Fn is a one-to-one function with domain 1c and range 1c. (Contributed by SF, 26-Feb-2015.)
Pw1Fn 1c1c

Theoremfnfullfunlem1 5856* Lemma for fnfullfun 5858. Binary relationship over part one of the full function definition. (Contributed by SF, 9-Mar-2015.)

Theoremfnfullfunlem2 5857 Lemma for fnfullfun 5858. Part one of the full function operator yields a function. (Contributed by SF, 9-Mar-2015.)

Theoremfnfullfun 5858 The full function operator yields a function over . (Contributed by SF, 9-Mar-2015.)
FullFun

Theoremfullfunexg 5859 The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
FullFun

Theoremfullfunex 5860 The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
FullFun

Theoremfvfullfunlem1 5861* Lemma for fvfullfun 5864. Calculate the domain of part one of the full function definition. (Contributed by SF, 9-Mar-2015.)

Theoremfvfullfunlem2 5862 Lemma for fvfullfun 5864. Part one of the full function definition is a subset of the function. (Contributed by SF, 9-Mar-2015.)

Theoremfvfullfunlem3 5863 Lemma for fvfullfun 5864. Part one of the full function definition agrees with the set itself over its domain. (Contributed by SF, 9-Mar-2015.)

Theoremfvfullfun 5864 The value of the full function definition agrees with the function value everywhere. (Contributed by SF, 9-Mar-2015.)
FullFun

Theorembrfullfung 5865 Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
FullFun

Theorembrfullfun 5866 Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
FullFun

Theorembrfullfunop 5867 Binary relationship of the full function operation over an ordered pair. (Contributed by SF, 9-Mar-2015.)
FullFun

Theoremfvdomfn 5868 Calculate the value of the domain function. (Contributed by Scott Fenton, 9-Aug-2019.)
Dom

Theoremfvranfn 5869 Calculate the value of the range function. (Contributed by Scott Fenton, 9-Aug-2019.)
Ran

Theoremdomfnex 5870 The domain function is stratified. (Contributed by Scott Fenton, 9-Aug-2019.)
Dom

Theoremranfnex 5871 The range function is stratified. (Contributed by Scott Fenton, 9-Aug-2019.)
Ran

2.3.11  Closure operation

Syntaxcclos1 5872 Extend the definition of a class to include the closure operation.
Clos1

Definitiondf-clos1 5873* Define the closure operation. A modified version of the definition from [Rosser] p. 245. (Contributed by SF, 11-Feb-2015.)
Clos1

Theoremclos1eq1 5874 Equality law for closure. (Contributed by SF, 11-Feb-2015.)
Clos1 Clos1

Theoremclos1eq2 5875 Equality law for closure. (Contributed by SF, 11-Feb-2015.)
Clos1 Clos1

Theoremclos1ex 5876 The closure of a set under a set is a set. (Contributed by SF, 11-Feb-2015.)
Clos1

Theoremclos1exg 5877 The closure of a set under a set is a set. (Contributed by SF, 11-Feb-2015.)
Clos1

Theoremclos1base 5878 The initial set of a closure is a subset of the closure. Theorem IX.5.13 of [Rosser] p. 246. (Contributed by SF, 13-Feb-2015.)
Clos1

Theoremclos1conn 5879 If a class is connected to an element of a closure via , then it is a member of the closure. Theorem IX.5.14 of [Rosser] p. 246. (Contributed by SF, 13-Feb-2015.)
Clos1

Theoremclos1induct 5880* Inductive law for closure. If the base set is a subset of , and is closed under , then the closure is a subset of . Theorem IX.5.15 of [Rosser] p. 247. (Contributed by SF, 11-Feb-2015.)
Clos1

Theoremclos1is 5881* Induction scheme for closures. Hypotheses one through three set up existence properties, hypothesis four sets up stratification, hypotheses five through seven set up implicit substitution, and hypotheses eight and nine set up the base and induction steps. (Contributed by SF, 13-Feb-2015.)
Clos1

Theoremclos1basesuc 5882* A member of a closure is either in the base set or connected to another member by . Theorem IX.5.16 of [Rosser] p. 248. (Contributed by SF, 13-Feb-2015.)
Clos1

Theoremclos1baseima 5883 A closure is equal to the base set together with the image of the closure under . Theorem X.4.37 of [Rosser] p. 303. (Contributed by SF, 10-Mar-2015.)
Clos1

Theoremclos1basesucg 5884* A member of a closure is either in the base set or connected to another member by . Theorem IX.5.16 of [Rosser] p. 248. (Contributed by Scott Fenton, 31-Jul-2019.)
Clos1

Theoremdfnnc3 5885 The finite cardinals as expressed via the closure operation. Theorem X.1.3 of [Rosser] p. 276. (Contributed by SF, 12-Feb-2015.)
Nn Clos1 0c 1c

Theoremclos1nrel 5886 The value of a closure when the base set is not related to anything in . (Contributed by SF, 13-Mar-2015.)
Clos1

Theoremclos10 5887 The value of a closure over an empty base set. (Contributed by Scott Fenton, 31-Jul-2019.)
Clos1

2.4  Orderings

2.4.1  Basic ordering relationships

Syntaxctrans 5888 Extend the definition of a class to include the set of all transitive relationships.
Trans

Syntaxcref 5889 Extend the definition of a class to include the set of all reflexive relationships.
Ref

Syntaxcantisym 5890 Extend the definition of a class to include the set of all antisymmetric relationships.
Antisym

Syntaxcpartial 5891 Extend the definition of a class to include the set of all partial orderings.
Po

Syntaxcconnex 5892 Extend the definition of a class to include the set of all connected relationships.
Connex

Syntaxcstrict 5893 Extend the definition of a class to include the set of all strict linear orderings.
Or

Syntaxcfound 5894 Extend the definition of a class to include the set of all founded relationships.
Fr

Syntaxcwe 5895 Extend the definition of a class to include the set of all well-ordered relationships.
We

Syntaxcext 5896 Extend the definition of a class to include the set of all extensional relationships.
Ext

Syntaxcsym 5897 Extend the definition of a class to include the symmetric relationships.
Sym

Syntaxcer 5898 Extend the definition of a class to include the equivalence relationships.
Er

Definitiondf-trans 5899* Define the set of all transitive relationships over a base set. (Contributed by SF, 19-Feb-2015.)
Trans

Definitiondf-ref 5900* Define the set of all reflexive relationships over a base set. (Contributed by SF, 19-Feb-2015.)
Ref

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >