P. 48 of Theorem List - New Foundations Explorer

Home	New Foundations Explorer Theorem List (p. 48 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 -** 4701-4800 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	opelopabga 4701*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
$/\$ $/\$

Theorem	brabga 4702*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
$/\$ $/\$

Theorem	opelopab2a 4703*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	opelopaba 4704*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
$/\$

Theorem	braba 4705*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
$/\$

Theorem	opelopabg 4706*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by set.mm contributors, 19-Dec-2013.)
$/\$

Theorem	brabg 4707*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by set.mm contributors, 19-Dec-2013.)
$/\$

Theorem	opelopab2 4708*	Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by set.mm contributors, 19-Dec-2013.)
$/\$ $/\$ $/\$

Theorem	opelopab 4709*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)


Theorem	brab 4710*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)


Theorem	opelopabaf 4711*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4709 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
$/\$

Theorem	opelopabf 4712*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4709 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)


Theorem	ssopab2 4713	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)


Theorem	ssopab2b 4714	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)


Theorem	ssopab2i 4715	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)


Theorem	ssopab2dv 4716*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)


Theorem	opabn0 4717	Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)


2.3.5 Set construction functions

Syntax	c1st 4718	Extend the definition of a class to include the first member an ordered pair function.


Syntax	cswap 4719	Extend the definition of a class to include the swap function.
Swap

Syntax	csset 4720	Extend the definition of a class to include the subset relationship.
S

Syntax	csi 4721	Extend the definition of a class to include the singleton image.
SI

Syntax	ccom 4722	Extend the definition of a class to include the composition of two classes.


Syntax	cima 4723	Extend the definition of a class to include the image of one class under another.


Definition	df-1st 4724*	Define a function that extracts the first member, or abscissa, of an ordered pair. (Contributed by SF, 5-Jan-2015.)


Definition	df-swap 4725*	Define a function that swaps the two elements of an ordered pair. (Contributed by SF, 5-Jan-2015.)
Swap $/\$

Definition	df-sset 4726*	Define a relationship that holds between subsets. (Contributed by SF, 5-Jan-2015.)
S

Definition	df-co 4727*	Define the composition of two classes. (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-ima 4728*	Define the image of one class under another. (Contributed by SF, 5-Jan-2015.)


Definition	df-si 4729*	Define the singleton image of a class. (Contributed by SF, 5-Jan-2015.)
SI $/\$ $/\$

Theorem	el1st 4730*	Membership in . (Contributed by SF, 5-Jan-2015.)


Theorem	br1stg 4731	The binary relationship over the function. (Contributed by SF, 5-Jan-2015.)
$/\$

Theorem	setconslem1 4732*	Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Phi

Theorem	setconslem2 4733*	Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c Phi 0_c

Theorem	setconslem3 4734	Lemma for set construction functions. Set up a mapping between Kuratowski and Quine ordered pairs. (Contributed by SF, 7-Jan-2015.)
∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c

Theorem	setconslem4 4735*	Lemma for set construction functions. Create a mapping between the two types of ordered pair abstractions. (Contributed by SF, 7-Jan-2015.)
⋃₁⋃₁ _k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k

Theorem	setconslem5 4736	Lemma for set construction theorems. The big expression in the middle of setconslem4 4735 forms a set. (Contributed by SF, 7-Jan-2015.)
∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c

Theorem	setconslem6 4737*	Lemma for the set construction functions. Invert the expression from setconslem4 4735. (Contributed by SF, 7-Jan-2015.)
_k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ ₁ $/\$

Theorem	setconslem7 4738	Lemma for the set construction theorems. Reorganized version of setconslem3 4734. (Contributed by SF, 4-Feb-2015.)
∼ Ins2_k Ins3_k S_k Ins2_k Ins2_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins3_k SI_k SI_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c

Theorem	df1st2 4739	Express the function via the set construction functions. (Contributed by SF, 4-Feb-2015.)
⋃₁⋃₁ _k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k ∼ Ins2_k Ins3_k S_k Ins2_k Ins2_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins3_k SI_k SI_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ 1_c

Theorem	1stex 4740	The function is a set. (Contributed by SF, 6-Jan-2015.)


Theorem	elswap 4741*	Membership in the Swap function. (Contributed by SF, 6-Jan-2015.)
Swap

Theorem	dfswap2 4742	Express the Swap function via set construction operators. (Contributed by SF, 6-Jan-2015.)
Swap ∼ Ins2_k Ins2_k S_k Ins2_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins3_k SI_k SI_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k SI_k Image_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k₁ ₁ ₁ ₁ ₁ ₁ 1_c Ins2_k Ins3_k SI_k SI_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins3_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c Ins3_k SI_k SI_k SI_k SI_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ ₁ ₁ ₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ 1_c_k

Theorem	swapex 4743	The Swap function is a set. (Contributed by SF, 6-Jan-2015.)
Swap

Theorem	dfsset2 4744	Express the S relationship via the set construction functors. (Contributed by SF, 7-Jan-2015.)
S ⋃₁⋃₁ _k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k S_k

Theorem	ssetex 4745	The subset relationship is a set. (Contributed by SF, 6-Jan-2015.)
S

Theorem	dfima2 4746	Express the image functor in terms of the set construction functions. (Contributed by SF, 7-Jan-2015.)
_k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ ₁ _k

Theorem	imaexg 4747	The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
$/\$

Theorem	imaex 4748	The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)


Theorem	dfco1 4749	Express Quine composition via Kuratowski composition. (Contributed by SF, 7-Jan-2015.)
⋃₁⋃₁ _k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ ₁ _k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ ₁

Theorem	coexg 4750	The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
$/\$

Theorem	coex 4751	The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)


Theorem	dfsi2 4752	Express singleton image in terms of the Kuratowski singleton image. (Contributed by SF, 7-Jan-2015.)
SI ⋃₁⋃₁ _k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k SI_k _k _k ∼ Ins3_k SI_k SI_k S_k Ins2_k Ins3_k S_k _k SI_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k Ins2_k Ins2_k S_k Ins3_k SI_k ∼ Ins2_k S_k Ins3_k _kImage_kImage_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c Nn _k _k ∼ Nn _k _k S_k 0_c _k _k₁ ₁ 1_c_k₁ ₁ 1_c_k₁ ₁ ₁ ₁ 1_c_k₁ ₁

Theorem	siexg 4753	The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
SI

Theorem	siex 4754	The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
SI

Theorem	elima 4755*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 19-Apr-2004.)


Theorem	elima2 4756*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 11-Aug-2004.)
$/\$

Theorem	elima3 4757*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 14-Aug-1994.)
$/\$

Theorem	brssetg 4758	Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
$/\$ S

Theorem	brsset 4759	Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
S

Theorem	brssetsn 4760	Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
S

Theorem	opelssetsn 4761	Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
S

Theorem	brsi 4762*	Binary relationship over a singleton image. (Contributed by SF, 11-Feb-2015.)
SI $/\$ $/\$

2.3.6 Epsilon and identity relations

Syntax	cep 4763	Extend class notation to include the epsilon relation.


Syntax	cid 4764	Extend the definition of a class to include identity relation.


Definition	df-eprel 4765*	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. (Contributed by SF, 5-Jan-2015.)


Theorem	epelc 4766	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)


Theorem	epel 4767	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)


Definition	df-id 4768*	Define the identity relation. Definition 9.15 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)


Theorem	dfid3 4769	A stronger version of df-id 4768 that doesn't require and to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.)


Theorem	dfid2 4770	Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)


2.3.7 Functions and relations

Syntax	cxp 4771	Extend the definition of a class to include the cross product.


Syntax	ccnv 4772	Extend the definition of a class to include the converse of a class.


Syntax	cdm 4773	Extend the definition of a class to include the domain of a class.


Syntax	crn 4774	Extend the definition of a class to include the range of a class.


Syntax	cres 4775	Extend the definition of a class to include the restriction of a class. (Read: The restriction of to .)


Syntax	wfun 4776	Extend the definition of a wff to include the function predicate. (Read: is a function.)


Syntax	wfn 4777	Extend the definition of a wff to include the function predicate with a domain. (Read: is a function on .)


Syntax	wf 4778	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: maps into .)


Syntax	wf1 4779	Extend the definition of a wff to include one-to-one functions. (Read: maps one-to-one into .) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.


Syntax	wfo 4780	Extend the definition of a wff to include onto functions. (Read: maps onto .) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.


Syntax	wf1o 4781	Extend the definition of a wff to include one-to-one onto functions. (Read: maps one-to-one onto .) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.


Syntax	cfv 4782	Extend the definition of a class to include the value of a function. (Read: The value of at , or " of .")


Syntax	wiso 4783	Extend the definition of a wff to include the isomorphism property. (Read: is an , isomorphism of onto .)


Syntax	c2nd 4784	Extend the definition of a class to include the second function.


Definition	df-xp 4785*	Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-cnv 4786*	Define the converse of a class. Definition 9.12 of [Quine] p. 64. We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. Many authors use the postfix superscript "to the minus one." "Converse" is Quine's terminology; some authors call it "inverse," especially when the argument is a function. (Contributed by SF, 5-Jan-2015.)


Definition	df-rn 4787	Define the range of a class. The notation " " is used by Enderton; other authors sometimes use script R or script W. (Contributed by SF, 5-Jan-2015.)


Definition	df-dm 4788	Define the domain of a class. The notation " " is used by Enderton; other authors sometimes use script D. (Contributed by SF, 5-Jan-2015.)


Definition	df-res 4789	Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. (Contributed by SF, 5-Jan-2015.)


Definition	df-fun 4790	Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5120, dffun3 5121, dffun4 5122, dffun5 5123, dffun6 5125, dffun7 5134, dffun8 5135, and dffun9 5136. (Contributed by SF, 5-Jan-2015.) (Revised by Scott Fenton, 14-Apr-2021.)


Definition	df-fn 4791	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5225, dffn3 5230, dffn4 5276, and dffn5 5364. (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-f 4792	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5420, dff3 5421, and dff4 5422. (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-f1 4793	Define a one-to-one function. For equivalent definitions see dff12 5258 and dff13 5472. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-fo 4794	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 5274, dffo3 5423, dffo4 5424, and dffo5 5425. (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-f1o 4795	Define a one-to-one onto function. For equivalent definitions see dff1o2 5292, dff1o3 5293, dff1o4 5295, and dff1o5 5296. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-fv 4796*	Define the value of a function. (Contributed by SF, 5-Jan-2015.)


Definition	df-iso 4797*	Define the isomorphism predicate. We read this as " is an , isomorphism of onto ." Normally, and are ordering relations on and respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that and are subscripts. (Contributed by SF, 5-Jan-2015.)
$/\$

Definition	df-2nd 4798*	Define the function. This function extracts the second member of an ordered pair. (Contributed by SF, 5-Jan-2015.)


Theorem	xpeq1 4799	Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)


Theorem	xpeq2 4800	Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)

< 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-6339

< Previous Next >