P. 59 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	imageex 5801	The image function of a set is a set. (Contributed by SF, 11-Feb-2015.)
|- A e. _V   =>   |- ImageA e. _V
Theorem	dmtxp 5802	The domain of a tail cross product is the intersection of the domains of its arguments. (Contributed by SF, 18-Feb-2015.)
|- dom (R (x) S) = (dom R i^i dom S)
Theorem	txpcofun 5803	Composition distributes over tail cross product in the case of a function. (Contributed by SF, 18-Feb-2015.)
|- Fun F   =>   |- ((R (x) S) o. F) = ((R o. F) (x) (S o. F))
Theorem	fntxp 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) -> (F (x) G) Fn (A i^i B))
Theorem	otsnelsi3 5805	Ordered triple membership in triple singleton image. (Contributed by SF, 12-Feb-2015.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- (<.{A}, <.{B}, {C}>.>. e. SI3 R <-> <.A, <.B, C>.>. e. R)
Theorem	si3ex 5806	SI3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
|- A e. _V   =>   |- SI3 A e. _V
Theorem	releqel 5807*	Lemma to turn a membership condition into an equality condition. (Contributed by SF, 9-Mar-2015.)
|- T e. _V   &   |- (<.{y}, T>. e. R <-> y e. A)   =>   |- (<.x, T>. e. ∼ (( Ins3 S (+) Ins2 R)"1c) <-> x = A)
Theorem	releqmpt 5808*	Equality condition for a mapping. (Contributed by SF, 9-Mar-2015.)
|- (<.{y}, x>. e. R <-> y e. V)   =>   |- ((A X. _V) i^i `' ∼ (( Ins3 S (+) Ins2 R)"1c)) = (x e. A |-> V)
Theorem	releqmpt2 5809*	Equality condition for a mapping operation. (Contributed by SF, 13-Feb-2015.)
|- (<.{z}, <.x, y>.>. e. R <-> z e. V)   =>   |- (((A X. B) X. _V) \ (( Ins2 S (+) Ins3 R)"1c)) = (x e. A, y e. B |-> V)
Theorem	mptexlem 5810	Lemma for the existence of a mapping. (Contributed by SF, 9-Mar-2015.)
|- A e. _V   &   |- R e. _V   =>   |- ((A X. _V) i^i `' ∼ (( Ins3 S (+) Ins2 R)"1c)) e. _V
Theorem	mpt2exlem 5811	Lemma for the existence of a double mapping. (Contributed by SF, 13-Feb-2015.)
|- A e. _V   &   |- B e. _V   &   |- R e. _V   =>   |- (((A X. B) X. _V) \ (( Ins2 S (+) Ins3 R)"1c)) e. _V
Theorem	cupvalg 5812	The value of the little cup function. (Contributed by SF, 11-Feb-2015.)
|- ((A e. V /\ B e. W) -> (A Cup B) = (A u. B))
Theorem	fncup 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
Theorem	brcupg 5814	Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
|- ((A e. V /\ B e. W) -> (<.A, B>. Cup C <-> C = (A u. B)))
Theorem	brcup 5815	Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>. Cup C <-> C = (A u. B))
Theorem	cupex 5816	The little cup function is a set. (Contributed by SF, 11-Feb-2015.)
|- Cup e. _V
Theorem	composevalg 5817	The value of the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
|- ((A e. V /\ B e. W) -> (A Compose B) = (A o. B))
Theorem	composefn 5818	The compose function is a function over the universe. (Contributed by Scott Fenton, 19-Apr-2021.)
|- Compose Fn _V
Theorem	brcomposeg 5819	Binary relationship form of the compose function. (Contributed by Scott Fenton, 19-Apr-2021.)
|- ((A e. V /\ B e. W) -> (<.A, B>. Compose C <-> (A o. B) = C))
Theorem	composeex 5820	The compose function is a set. (Contributed by Scott Fenton, 19-Apr-2021.)
|- Compose e. _V
Theorem	brdisjg 5821	The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
|- ((A e. V /\ B e. W) -> (A Disj B <-> (A i^i B) = (/)))
Theorem	brdisj 5822	The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A Disj B <-> (A i^i B) = (/))
Theorem	disjex 5823	The disjointedness relationship is a set. (Contributed by SF, 11-Feb-2015.)
|- Disj e. _V
Theorem	addcfnex 5824	The cardinal addition function exists. (Contributed by SF, 12-Feb-2015.)
|- AddC e. _V
Theorem	addcfn 5825	AddC is a function over the universe. (Contributed by SF, 2-Mar-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
|- AddC Fn _V
Theorem	braddcfn 5826	Binary relationship form of the AddC function. (Contributed by SF, 2-Mar-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>. AddC C <-> (A +o B) = C)
Theorem	epprc 5827	The membership relationship is a proper class. This theorem together with vvex 4109 demonstrates the basic idea behind New Foundations: since x e. 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 e. _V
Theorem	funsex 5828	The class of all functions forms a set. (Contributed by SF, 18-Feb-2015.)
|- Funs e. _V
Theorem	elfuns 5829	Membership in the set of all functions. (Contributed by SF, 23-Feb-2015.)
|- F e. _V   =>   |- (F e. Funs <-> Fun F)
Theorem	elfunsg 5830	Membership in the set of all functions. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (F e. V -> (F e. Funs <-> Fun F))
Theorem	elfunsi 5831	Membership in the set of all functions implies functionhood. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (F e. Funs -> Fun F)
Theorem	fnsex 5832	The function with domain relationship exists. (Contributed by SF, 23-Feb-2015.)
|- Fns e. _V
Theorem	brfns 5833	Binary relationship form of Fns relationship. (Contributed by SF, 23-Feb-2015.)
|- F e. _V   =>   |- (F Fns A <-> F Fn A)
Theorem	pprodeq1 5834	Equality theorem for parallel product. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (A = B -> PProd (A, C) = PProd (B, C))
Theorem	pprodeq2 5835	Equality theorem for parallel product. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (A = B -> PProd (C, A) = PProd (C, B))
Theorem	qrpprod 5836	A quadratic relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
|- (<.A, B>. PProd (R, S)<.C, D>. <-> (ARC /\ BSD))
Theorem	pprodexg 5837	The parallel product of two sets is a set. (Contributed by SF, 24-Feb-2015.)
|- ((A e. V /\ B e. W) -> PProd (A, B) e. _V)
Theorem	pprodex 5838	The parallel product of two sets is a set. (Contributed by SF, 24-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- PProd (A, B) e. _V
Theorem	brpprod 5839*	Binary relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
|- (A PProd (R, S)B <-> E.xE.yE.zE.w(A = <.x, y>. /\ B = <.z, w>. /\ (xRz /\ ySw)))
Theorem	dmpprod 5840	The domain of a parallel product. (Contributed by SF, 24-Feb-2015.)
|- dom PProd (A, B) = (dom A X. dom B)
Theorem	cnvpprod 5841	The converse of a parallel product. (Contributed by SF, 24-Feb-2015.)
|- `' PProd (A, B) = PProd (`'A, `'B)
Theorem	rnpprod 5842	The range of a parallel product. (Contributed by SF, 24-Feb-2015.)
|- ran PProd (A, B) = (ran A X. ran B)
Theorem	fnpprod 5843	Functionhood law for parallel product. (Contributed by SF, 24-Feb-2015.)
|- ((F Fn A /\ G Fn B) -> PProd (F, G) Fn (A X. B))
Theorem	f1opprod 5844	The parallel product of two bijections is a bijection. (Contributed by SF, 24-Feb-2015.)
|- ((F:A-1-1-onto->C /\ G:B-1-1-onto->D) -> PProd (F, G):(A X. B)-1-1-onto->(C X. D))
Theorem	ovcross 5845	The value of the cross product function. (Contributed by SF, 24-Feb-2015.)
|- ((A e. V /\ B e. W) -> (A Cross B) = (A X. B))
Theorem	fncross 5846	The cross product function is a function over (_V X. _V) (Contributed by SF, 24-Feb-2015.)
|- Cross Fn _V
Theorem	dmcross 5847	The domain of the cross product function. (Contributed by SF, 24-Feb-2015.)
|- dom Cross = _V
Theorem	brcrossg 5848	Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
|- ((A e. V /\ B e. W) -> (<.A, B>. Cross C <-> C = (A X. B)))
Theorem	brcross 5849	Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>. Cross C <-> C = (A X. B))
Theorem	crossex 5850	The function mapping x and y to their cross product is a set. (Contributed by SF, 11-Feb-2015.)
|- Cross e. _V
Theorem	pw1fnval 5851	The value of the unit power class function. (Contributed by SF, 25-Feb-2015.)
|- A e. _V   =>   |- ( Pw1Fn ` {A}) = ~P1 A
Theorem	pw1fnex 5852	The unit power class function is a set. (Contributed by SF, 25-Feb-2015.)
|- Pw1Fn e. _V
Theorem	fnpw1fn 5853	Functionhood statement for Pw1Fn. (Contributed by SF, 25-Feb-2015.)
|- Pw1Fn Fn 1c
Theorem	brpw1fn 5854	Binary relationship form of Pw1Fn. (Contributed by SF, 25-Feb-2015.)
|- A e. _V   =>   |- ({A} Pw1Fn B <-> B = ~P1 A)
Theorem	pw1fnf1o 5855	Pw1Fn is a one-to-one function with domain 1c and range ~P1c. (Contributed by SF, 26-Feb-2015.)
|- Pw1Fn :1c-1-1-onto->~P1c
Theorem	fnfullfunlem1 5856*	Lemma for fnfullfun 5858. Binary relationship over part one of the full function definition. (Contributed by SF, 9-Mar-2015.)
|- (A(( _I o. F) \ ( ∼ _I o. F))B <-> (AFB /\ A.x(AFx -> x = B)))
Theorem	fnfullfunlem2 5857	Lemma for fnfullfun 5858. Part one of the full function operator yields a function. (Contributed by SF, 9-Mar-2015.)
|- Fun (( _I o. F) \ ( ∼ _I o. F))
Theorem	fnfullfun 5858	The full function operator yields a function over _V. (Contributed by SF, 9-Mar-2015.)
|- FullFun F Fn _V
Theorem	fullfunexg 5859	The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
|- (F e. V -> FullFun F e. _V)
Theorem	fullfunex 5860	The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
|- F e. _V   =>   |- FullFun F e. _V
Theorem	fvfullfunlem1 5861*	Lemma for fvfullfun 5864. Calculate the domain of part one of the full function definition. (Contributed by SF, 9-Mar-2015.)
|- dom (( _I o. F) \ ( ∼ _I o. F)) = {x | E!y xFy}
Theorem	fvfullfunlem2 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 o. F) \ ( ∼ _I o. F)) C_ F
Theorem	fvfullfunlem3 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 e. dom (( _I o. F) \ ( ∼ _I o. F)) -> ((( _I o. F) \ ( ∼ _I o. F))` A) = (F` A))
Theorem	fvfullfun 5864	The value of the full function definition agrees with the function value everywhere. (Contributed by SF, 9-Mar-2015.)
|- ( FullFun F` A) = (F` A)
Theorem	brfullfung 5865	Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
|- (A e. V -> (A FullFun FB <-> (F` A) = B))
Theorem	brfullfun 5866	Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
|- A e. _V   =>   |- (A FullFun FB <-> (F` A) = B)
Theorem	brfullfunop 5867	Binary relationship of the full function operation over an ordered pair. (Contributed by SF, 9-Mar-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<.A, B>. FullFun FC <-> (AFB) = C)
Theorem	fvdomfn 5868	Calculate the value of the domain function. (Contributed by Scott Fenton, 9-Aug-2019.)
|- (A e. V -> ( Dom ` A) = dom A)
Theorem	fvranfn 5869	Calculate the value of the range function. (Contributed by Scott Fenton, 9-Aug-2019.)
|- (A e. V -> ( Ran ` A) = ran A)
Theorem	domfnex 5870	The domain function is stratified. (Contributed by Scott Fenton, 9-Aug-2019.)
|- Dom e. _V
Theorem	ranfnex 5871	The range function is stratified. (Contributed by Scott Fenton, 9-Aug-2019.)
|- Ran e. _V
2.3.11  Closure operation
Syntax	cclos1 5872	Extend the definition of a class to include the closure operation.
class Clos1 (A, R)
Definition	df-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 C_ a /\ (R"a) C_ a)}
Theorem	clos1eq1 5874	Equality law for closure. (Contributed by SF, 11-Feb-2015.)
|- (S = T -> Clos1 (S, R) = Clos1 (T, R))
Theorem	clos1eq2 5875	Equality law for closure. (Contributed by SF, 11-Feb-2015.)
|- (R = T -> Clos1 (S, R) = Clos1 (S, T))
Theorem	clos1ex 5876	The closure of a set under a set is a set. (Contributed by SF, 11-Feb-2015.)
|- S e. _V   &   |- R e. _V   =>   |- Clos1 (S, R) e. _V
Theorem	clos1exg 5877	The closure of a set under a set is a set. (Contributed by SF, 11-Feb-2015.)
|- ((S e. V /\ R e. W) -> Clos1 (S, R) e. _V)
Theorem	clos1base 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_ C
Theorem	clos1conn 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 e. C /\ ARB) -> B e. C)
Theorem	clos1induct 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 e. _V   &   |- R e. _V   &   |- C = Clos1 (S, R)   =>   |- ((X e. V /\ S C_ X /\ A.x e. C A.z((x e. X /\ xRz) -> z e. X)) -> C C_ X)
Theorem	clos1is 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 e. _V   &   |- R e. _V   &   |- C = Clos1 (S, R)   &   |- {x | ph} e. _V   &   |- (x = y -> (ph <-> ps))   &   |- (x = z -> (ph <-> ch))   &   |- (x = A -> (ph <-> th))   &   |- (x e. S -> ph)   &   |- ((y e. C /\ yRz /\ ps) -> ch)   =>   |- (A e. C -> th)
Theorem	clos1basesuc 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 e. _V   &   |- R e. _V   &   |- C = Clos1 (S, R)   =>   |- (A e. C <-> (A e. S \/ E.x e. C xRA))
Theorem	clos1baseima 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 e. _V   &   |- R e. _V   &   |- C = Clos1 (S, R)   =>   |- C = (S u. (R"C))
Theorem	clos1basesucg 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 e. V /\ R e. W) -> (A e. C <-> (A e. S \/ E.x e. C xRA)))
Theorem	dfnnc3 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 e. _V |-> (x +o 1c)))
Theorem	clos1nrel 5886	The value of a closure when the base set is not related to anything in R. (Contributed by SF, 13-Mar-2015.)
|- S e. _V   &   |- R e. _V   &   |- C = Clos1 (S, R)   =>   |- ((R"S) = (/) -> C = S)
Theorem	clos10 5887	The value of a closure over an empty base set. (Contributed by Scott Fenton, 31-Jul-2019.)
|- R e. _V   &   |- C = Clos1 ((/), R)   =>   |- C = (/)
2.4  Orderings
2.4.1  Basic ordering relationships
Syntax	ctrans 5888	Extend the definition of a class to include the set of all transitive relationships.
class Trans
Syntax	cref 5889	Extend the definition of a class to include the set of all reflexive relationships.
class Ref
Syntax	cantisym 5890	Extend the definition of a class to include the set of all antisymmetric relationships.
class Antisym
Syntax	cpartial 5891	Extend the definition of a class to include the set of all partial orderings.
class Po
Syntax	cconnex 5892	Extend the definition of a class to include the set of all connected relationships.
class Connex
Syntax	cstrict 5893	Extend the definition of a class to include the set of all strict linear orderings.
class Or
Syntax	cfound 5894	Extend the definition of a class to include the set of all founded relationships.
class Fr
Syntax	cwe 5895	Extend the definition of a class to include the set of all well-ordered relationships.
class We
Syntax	cext 5896	Extend the definition of a class to include the set of all extensional relationships.
class Ext
Syntax	csym 5897	Extend the definition of a class to include the symmetric relationships.
class Sym
Syntax	cer 5898	Extend the definition of a class to include the equivalence relationships.
class Er
Definition	df-trans 5899*	Define the set of all transitive relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Trans = {<.r, a>. | A.x e. a A.y e. a A.z e. a ((xry /\ yrz) -> xrz)}
Definition	df-ref 5900*	Define the set of all reflexive relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Ref = {<.r, a>. | A.x e. a xrx}