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	imageexg 5801	The image function of a set is a set. (Contributed by SF, 11-Feb-2015.)
⊢ (A ∈ V → ImageA ∈ V)
Theorem	imageex 5802	The image function of a set is a set. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ ImageA ∈ V
Theorem	dmtxp 5803	The domain of a tail cross product is the intersection of the domains of its arguments. (Contributed by SF, 18-Feb-2015.)
⊢ dom (R ⊗ S) = (dom R ∩ dom S)
Theorem	txpcofun 5804	Composition distributes over tail cross product in the case of a function. (Contributed by SF, 18-Feb-2015.)
⊢ Fun F    ⇒   ⊢ ((R ⊗ S) ∘ F) = ((R ∘ F) ⊗ (S ∘ F))
Theorem	fntxp 5805	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 ⊗ G) Fn (A ∩ B))
Theorem	otsnelsi3 5806	Ordered triple membership in triple singleton image. (Contributed by SF, 12-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (⟨{A}, ⟨{B}, {C}⟩⟩ ∈ SI3 R ↔ ⟨A, ⟨B, C⟩⟩ ∈ R)
Theorem	si3ex 5807	SI3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ SI3 A ∈ V
Theorem	releqel 5808*	Lemma to turn a membership condition into an equality condition. (Contributed by SF, 9-Mar-2015.)
⊢ T ∈ V    &   ⊢ (⟨{y}, T⟩ ∈ R ↔ y ∈ A)    ⇒   ⊢ (⟨x, T⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 R) “ 1c) ↔ x = A)
Theorem	releqmpt 5809*	Equality condition for a mapping. (Contributed by SF, 9-Mar-2015.)
⊢ (⟨{y}, x⟩ ∈ R ↔ y ∈ V)    ⇒   ⊢ ((A × V) ∩ ◡ ∼ (( Ins3 S ⊕ Ins2 R) “ 1c)) = (x ∈ A ↦ V)
Theorem	releqmpt2 5810*	Equality condition for a mapping operation. (Contributed by SF, 13-Feb-2015.)
⊢ (⟨{z}, ⟨x, y⟩⟩ ∈ R ↔ z ∈ V)    ⇒   ⊢ (((A × B) × V) ∖ (( Ins2 S ⊕ Ins3 R) “ 1c)) = (x ∈ A, y ∈ B ↦ V)
Theorem	mptexlem 5811	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
Theorem	mpt2exlem 5812	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
Theorem	cupvalg 5813	The value of the little cup function. (Contributed by SF, 11-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A Cup B) = (A ∪ B))
Theorem	fncup 5814	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 5815	Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟨A, B⟩ Cup C ↔ C = (A ∪ B)))
Theorem	brcup 5816	Binary relationship form of the cup function. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨A, B⟩ Cup C ↔ C = (A ∪ B))
Theorem	cupex 5817	The little cup function is a set. (Contributed by SF, 11-Feb-2015.)
⊢ Cup ∈ V
Theorem	composevalg 5818	The value of the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ ((A ∈ V ∧ B ∈ W) → (A Compose B) = (A ∘ B))
Theorem	composefn 5819	The compose function is a function over the universe. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ Compose Fn V
Theorem	brcomposeg 5820	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))
Theorem	composeex 5821	The compose function is a set. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ Compose ∈ V
Theorem	brdisjg 5822	The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A Disj B ↔ (A ∩ B) = ∅))
Theorem	brdisj 5823	The binary relationship form of the Disj relationship. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A Disj B ↔ (A ∩ B) = ∅)
Theorem	disjex 5824	The disjointedness relationship is a set. (Contributed by SF, 11-Feb-2015.)
⊢ Disj ∈ V
Theorem	addcfnex 5825	The cardinal addition function exists. (Contributed by SF, 12-Feb-2015.)
⊢ AddC ∈ V
Theorem	addcfn 5826	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 5827	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)
Theorem	epprc 5828	The membership relationship is a proper class. This theorem together with vvex 4110 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
Theorem	funsex 5829	The class of all functions forms a set. (Contributed by SF, 18-Feb-2015.)
⊢ Funs ∈ V
Theorem	elfuns 5830	Membership in the set of all functions. (Contributed by SF, 23-Feb-2015.)
⊢ F ∈ V    ⇒   ⊢ (F ∈ Funs ↔ Fun F)
Theorem	elfunsg 5831	Membership in the set of all functions. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (F ∈ V → (F ∈ Funs ↔ Fun F))
Theorem	elfunsi 5832	Membership in the set of all functions implies functionhood. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (F ∈ Funs → Fun F)
Theorem	fnsex 5833	The function with domain relationship exists. (Contributed by SF, 23-Feb-2015.)
⊢ Fns ∈ V
Theorem	brfns 5834	Binary relationship form of Fns relationship. (Contributed by SF, 23-Feb-2015.)
⊢ F ∈ V    ⇒   ⊢ (F Fns A ↔ F Fn A)
Theorem	pprodeq1 5835	Equality theorem for parallel product. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (A = B → PProd (A, C) = PProd (B, C))
Theorem	pprodeq2 5836	Equality theorem for parallel product. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (A = B → PProd (C, A) = PProd (C, B))
Theorem	qrpprod 5837	A quadratic relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
⊢ (⟨A, B⟩ PProd (R, S)⟨C, D⟩ ↔ (ARC ∧ BSD))
Theorem	pprodexg 5838	The parallel product of two sets is a set. (Contributed by SF, 24-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → PProd (A, B) ∈ V)
Theorem	pprodex 5839	The parallel product of two sets is a set. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ PProd (A, B) ∈ V
Theorem	brpprod 5840*	Binary relationship over a parallel product. (Contributed by SF, 24-Feb-2015.)
⊢ (A PProd (R, S)B ↔ ∃x∃y∃z∃w(A = ⟨x, y⟩ ∧ B = ⟨z, w⟩ ∧ (xRz ∧ ySw)))
Theorem	dmpprod 5841	The domain of a parallel product. (Contributed by SF, 24-Feb-2015.)
⊢ dom PProd (A, B) = (dom A × dom B)
Theorem	cnvpprod 5842	The converse of a parallel product. (Contributed by SF, 24-Feb-2015.)
⊢ ◡ PProd (A, B) = PProd (◡A, ◡B)
Theorem	rnpprod 5843	The range of a parallel product. (Contributed by SF, 24-Feb-2015.)
⊢ ran PProd (A, B) = (ran A × ran B)
Theorem	fnpprod 5844	Functionhood law for parallel product. (Contributed by SF, 24-Feb-2015.)
⊢ ((F Fn A ∧ G Fn B) → PProd (F, G) Fn (A × B))
Theorem	f1opprod 5845	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 × B)–1-1-onto→(C × D))
Theorem	ovcross 5846	The value of the cross product function. (Contributed by SF, 24-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A Cross B) = (A × B))
Theorem	fncross 5847	The cross product function is a function over (V × V) (Contributed by SF, 24-Feb-2015.)
⊢ Cross Fn V
Theorem	dmcross 5848	The domain of the cross product function. (Contributed by SF, 24-Feb-2015.)
⊢ dom Cross = V
Theorem	brcrossg 5849	Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟨A, B⟩ Cross C ↔ C = (A × B)))
Theorem	brcross 5850	Binary relationship over the cross product function. (Contributed by SF, 24-Feb-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟨A, B⟩ Cross C ↔ C = (A × B))
Theorem	crossex 5851	The function mapping x and y to their cross product is a set. (Contributed by SF, 11-Feb-2015.)
⊢ Cross ∈ V
Theorem	pw1fnval 5852	The value of the unit power class function. (Contributed by SF, 25-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ ( Pw1Fn ‘{A}) = ℘1A
Theorem	pw1fnex 5853	The unit power class function is a set. (Contributed by SF, 25-Feb-2015.)
⊢ Pw1Fn ∈ V
Theorem	fnpw1fn 5854	Functionhood statement for Pw1Fn. (Contributed by SF, 25-Feb-2015.)
⊢ Pw1Fn Fn 1c
Theorem	brpw1fn 5855	Binary relationship form of Pw1Fn. (Contributed by SF, 25-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ ({A} Pw1Fn B ↔ B = ℘1A)
Theorem	pw1fnf1o 5856	Pw1Fn is a one-to-one function with domain 1c and range ℘1c. (Contributed by SF, 26-Feb-2015.)
⊢ Pw1Fn :1c–1-1-onto→℘1c
Theorem	fnfullfunlem1 5857*	Lemma for fnfullfun 5859. Binary relationship over part one of the full function definition. (Contributed by SF, 9-Mar-2015.)
⊢ (A(( I ∘ F) ∖ ( ∼ I ∘ F))B ↔ (AFB ∧ ∀x(AFx → x = B)))
Theorem	fnfullfunlem2 5858	Lemma for fnfullfun 5859. Part one of the full function operator yields a function. (Contributed by SF, 9-Mar-2015.)
⊢ Fun (( I ∘ F) ∖ ( ∼ I ∘ F))
Theorem	fnfullfun 5859	The full function operator yields a function over V. (Contributed by SF, 9-Mar-2015.)
⊢ FullFun F Fn V
Theorem	fullfunexg 5860	The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
⊢ (F ∈ V → FullFun F ∈ V)
Theorem	fullfunex 5861	The full function of a set is a set. (Contributed by SF, 9-Mar-2015.)
⊢ F ∈ V    ⇒   ⊢ FullFun F ∈ V
Theorem	fvfullfunlem1 5862*	Lemma for fvfullfun 5865. 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}
Theorem	fvfullfunlem2 5863	Lemma for fvfullfun 5865. Part one of the full function definition is a subset of the function. (Contributed by SF, 9-Mar-2015.)
⊢ (( I ∘ F) ∖ ( ∼ I ∘ F)) ⊆ F
Theorem	fvfullfunlem3 5864	Lemma for fvfullfun 5865. 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) = (F ‘A))
Theorem	fvfullfun 5865	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 5866	Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
⊢ (A ∈ V → (A FullFun FB ↔ (F ‘A) = B))
Theorem	brfullfun 5867	Binary relationship of the full function operation. (Contributed by SF, 9-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ (A FullFun FB ↔ (F ‘A) = B)
Theorem	brfullfunop 5868	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)
Theorem	fvdomfn 5869	Calculate the value of the domain function. (Contributed by Scott Fenton, 9-Aug-2019.)
⊢ (A ∈ V → ( Dom ‘A) = dom A)
Theorem	fvranfn 5870	Calculate the value of the range function. (Contributed by Scott Fenton, 9-Aug-2019.)
⊢ (A ∈ V → ( Ran ‘A) = ran A)
Theorem	domfnex 5871	The domain function is stratified. (Contributed by Scott Fenton, 9-Aug-2019.)
⊢ Dom ∈ V
Theorem	ranfnex 5872	The range function is stratified. (Contributed by Scott Fenton, 9-Aug-2019.)
⊢ Ran ∈ V
2.3.11  Closure operation
Syntax	cclos1 5873	Extend the definition of a class to include the closure operation.
class Clos1 (A, R)
Definition	df-clos1 5874*	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 ∧ (R “ a) ⊆ a)}
Theorem	clos1eq1 5875	Equality law for closure. (Contributed by SF, 11-Feb-2015.)
⊢ (S = T → Clos1 (S, R) = Clos1 (T, R))
Theorem	clos1eq2 5876	Equality law for closure. (Contributed by SF, 11-Feb-2015.)
⊢ (R = T → Clos1 (S, R) = Clos1 (S, T))
Theorem	clos1ex 5877	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
Theorem	clos1exg 5878	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)
Theorem	clos1base 5879	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
Theorem	clos1conn 5880	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)
Theorem	clos1induct 5881*	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)
Theorem	clos1is 5882*	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 → θ)
Theorem	clos1basesuc 5883*	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))
Theorem	clos1baseima 5884	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 ∪ (R “ C))
Theorem	clos1basesucg 5885*	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)))
Theorem	dfnnc3 5886	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)))
Theorem	clos1nrel 5887	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)    ⇒   ⊢ ((R “ S) = ∅ → C = S)
Theorem	clos10 5888	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
Syntax	ctrans 5889	Extend the definition of a class to include the set of all transitive relationships.
class Trans
Syntax	cref 5890	Extend the definition of a class to include the set of all reflexive relationships.
class Ref
Syntax	cantisym 5891	Extend the definition of a class to include the set of all antisymmetric relationships.
class Antisym
Syntax	cpartial 5892	Extend the definition of a class to include the set of all partial orderings.
class Po
Syntax	cconnex 5893	Extend the definition of a class to include the set of all connected relationships.
class Connex
Syntax	cstrict 5894	Extend the definition of a class to include the set of all strict linear orderings.
class Or
Syntax	cfound 5895	Extend the definition of a class to include the set of all founded relationships.
class Fr
Syntax	cwe 5896	Extend the definition of a class to include the set of all well-ordered relationships.
class We
Syntax	cext 5897	Extend the definition of a class to include the set of all extensional relationships.
class Ext
Syntax	csym 5898	Extend the definition of a class to include the symmetric relationships.
class Sym
Syntax	cer 5899	Extend the definition of a class to include the equivalence relationships.
class Er
Definition	df-trans 5900*	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)}