 Home New Foundations ExplorerTheorem List (p. 59 of 64) < Previous  Next > Bad symbols? Try the GIF 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.)
A V       ImageA V

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

Theoremtxpcofun 5803 Composition distributes over tail cross product in the case of a function. (Contributed by SF, 18-Feb-2015.)
Fun F       ((RS) F) = ((R F) ⊗ (S F))

Theoremfntxp 5804 If F and G are functions, then their tail cross product is a function over the intersection of their domains. (Contributed by SF, 24-Feb-2015.)
((F Fn A G Fn B) → (FG) Fn (AB))

Theoremotsnelsi3 5805 Ordered triple membership in triple singleton image. (Contributed by SF, 12-Feb-2015.)
A V    &   B V    &   C V       ({A}, {B}, {C} SI3 RA, B, C R)

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

Theoremreleqel 5807* Lemma to turn a membership condition into an equality condition. (Contributed by SF, 9-Mar-2015.)
T V    &   ({y}, T Ry A)       (x, T ∼ (( Ins3 S Ins2 R) “ 1c) ↔ x = A)

Theoremreleqmpt 5808* Equality condition for a mapping. (Contributed by SF, 9-Mar-2015.)
({y}, x Ry V)       ((A × V) ∩ ∼ (( Ins3 S Ins2 R) “ 1c)) = (x A V)

Theoremreleqmpt2 5809* Equality condition for a mapping operation. (Contributed by SF, 13-Feb-2015.)
({z}, x, y Rz V)       (((A × B) × V) (( Ins2 S Ins3 R) “ 1c)) = (x A, y B V)

Theoremmptexlem 5810 Lemma for the existence of a mapping. (Contributed by SF, 9-Mar-2015.)
A V    &   R V       ((A × V) ∩ ∼ (( Ins3 S Ins2 R) “ 1c)) V

Theoremmpt2exlem 5811 Lemma for the existence of a double mapping. (Contributed by SF, 13-Feb-2015.)
A V    &   B V    &   R V       (((A × B) × V) (( Ins2 S Ins3 R) “ 1c)) V

Theoremcupvalg 5812 The value of the little cup function. (Contributed by SF, 11-Feb-2015.)
((A V B W) → (A Cup B) = (AB))

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 Fn V

Theorembrcupg 5814 Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
((A V B W) → (A, B Cup CC = (AB)))

Theorembrcup 5815 Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
A V    &   B V       (A, B Cup CC = (AB))

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

Theoremcomposevalg 5817 The value of the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
((A V B W) → (A Compose B) = (A B))

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

Theorembrcomposeg 5819 Binary relationship form of the compose function. (Contributed by Scott Fenton, 19-Apr-2021.)
((A V B W) → (A, B Compose C ↔ (A B) = C))

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

Theorembrdisjg 5821 The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
((A V B W) → (A Disj B ↔ (AB) = ))

Theorembrdisj 5822 The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
A V    &   B V       (A Disj B ↔ (AB) = )

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

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.)
A V    &   B V       (A, B AddC C ↔ (A +c B) = C)

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

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

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

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

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

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

Theorembrfns 5833 Binary relationship form of Fns relationship. (Contributed by SF, 23-Feb-2015.)
F V       (F Fns AF Fn A)

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

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

Theoremqrpprod 5836 A quadratic relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
(A, B PProd (R, S)C, D ↔ (ARC BSD))

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

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

Theorembrpprod 5839* Binary relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
(A PProd (R, S)Bxyzw(A = x, y B = z, w (xRz ySw)))

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

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

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

Theoremfnpprod 5843 Functionhood law for parallel product. (Contributed by SF, 24-Feb-2015.)
((F Fn A G Fn B) → PProd (F, G) Fn (A × B))

Theoremf1opprod 5844 The parallel product of two bijections is a bijection. (Contributed by SF, 24-Feb-2015.)
((F:A1-1-ontoC G:B1-1-ontoD) → PProd (F, G):(A × B)–1-1-onto→(C × D))

Theoremovcross 5845 The value of the cross product function. (Contributed by SF, 24-Feb-2015.)
((A V B W) → (A Cross B) = (A × B))

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

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

Theorembrcrossg 5848 Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
((A V B W) → (A, B Cross CC = (A × B)))

Theorembrcross 5849 Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
A V    &   B V       (A, B Cross CC = (A × B))

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

Theorempw1fnval 5851 The value of the unit power class function. (Contributed by SF, 25-Feb-2015.)
A V       ( Pw1Fn ‘{A}) = 1A

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

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

Theorembrpw1fn 5854 Binary relationship form of Pw1Fn (Contributed by SF, 25-Feb-2015.)
A V       ({A} Pw1Fn BB = 1A)

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

Theoremfnfullfunlem1 5856* Lemma for fnfullfun 5858. Binary relationship over part one of the full function definition. (Contributed by SF, 9-Mar-2015.)
(A(( I F) ( ∼ I F))B ↔ (AFB x(AFxx = B)))

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

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

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

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

Theoremfvfullfunlem1 5861* Lemma for fvfullfun 5864. Calculate the domain of part one of the full function definition. (Contributed by SF, 9-Mar-2015.)
dom (( I F) ( ∼ I F)) = {x ∃!y xFy}

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.)
(( I F) ( ∼ I F)) F

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.)
(A dom (( I F) ( ∼ I F)) → ((( I F) ( ∼ I F)) ‘A) = (FA))

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

Theorembrfullfung 5865 Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
(A V → (A FullFun FB ↔ (FA) = B))

Theorembrfullfun 5866 Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
A V       (A FullFun FB ↔ (FA) = B)

Theorembrfullfunop 5867 Binary relationship of the full function operation over an ordered pair. (Contributed by SF, 9-Mar-2015.)
A V    &   B V       (A, B FullFun FC ↔ (AFB) = C)

Theoremfvdomfn 5868 Calculate the value of the domain function. (Contributed by Scott Fenton, 9-Aug-2019.)
(A V → ( DomA) = dom A)

Theoremfvranfn 5869 Calculate the value of the range function. (Contributed by Scott Fenton, 9-Aug-2019.)
(A V → ( RanA) = ran A)

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

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

2.3.11  Closure operation

Syntaxcclos1 5872 Extend the definition of a class to include the closure operation.
class Clos1 (A, R)

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

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

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

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

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

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.)
C = Clos1 (S, R)       S C

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

Theoremclos1induct 5880* Inductive law for closure. If the base set is a subset of X, and X is closed under R, then the closure is a subset of X. Theorem IX.5.15 of [Rosser] p. 247. (Contributed by SF, 11-Feb-2015.)
S V    &   R V    &   C = Clos1 (S, R)       ((X V S X x C z((x X xRz) → z X)) → C X)

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.)
S V    &   R V    &   C = Clos1 (S, R)    &   {x φ} V    &   (x = y → (φψ))    &   (x = z → (φχ))    &   (x = A → (φθ))    &   (x Sφ)    &   ((y C yRz ψ) → χ)       (A Cθ)

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

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

Theoremclos1basesucg 5884* A member of a closure is either in the base set or connected to another member by R. Theorem IX.5.16 of [Rosser] p. 248. (Contributed by Scott Fenton, 31-Jul-2019.)
C = Clos1 (S, R)       ((S V R W) → (A C ↔ (A S x C xRA)))

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}, (x V (x +c 1c)))

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

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

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.
class Trans

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

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

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

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

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

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

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

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

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

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

Definitiondf-trans 5899* Define the set of all transitive relationships over a base set. (Contributed by SF, 19-Feb-2015.)
Trans = {r, a x a y a z a ((xry yrz) → xrz)}

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

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 >