HomeHome New Foundations Explorer
Theorem 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
 
Theoremaddcfnex 5824 The cardinal addition function exists. (Contributed by SF, 12-Feb-2015.)
AddC
 
Theoremaddcfn 5825 AddC is a function over the universe. (Contributed by SF, 2-Mar-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
AddC
 
Theorembraddcfn 5826 Binary relationship form of the AddC function. (Contributed by SF, 2-Mar-2015.)
   &       =>    AddC
 
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
    < Previous  Next >

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-6338
  Copyright terms: Public domain < Previous  Next >