Theorem List for New Foundations Explorer - 4701-4800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorembrabga 4701* The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → (φψ))    &   R = {x, y φ}       ((A V B W) → (ARBψ))

Theoremopelopab2a 4702* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → (φψ))       ((A C B D) → (A, B {x, y ((x C y D) φ)} ↔ ψ))

Theoremopelopaba 4703* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
A V    &   B V    &   ((x = A y = B) → (φψ))       (A, B {x, y φ} ↔ ψ)

Theorembraba 4704* The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
A V    &   B V    &   ((x = A y = B) → (φψ))    &   R = {x, y φ}       (ARBψ)

Theoremopelopabg 4705* 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.)
(x = A → (φψ))    &   (y = B → (ψχ))       ((A V B W) → (A, B {x, y φ} ↔ χ))

Theorembrabg 4706* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by set.mm contributors, 19-Dec-2013.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   R = {x, y φ}       ((A C B D) → (ARBχ))

Theoremopelopab2 4707* Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by set.mm contributors, 19-Dec-2013.)
(x = A → (φψ))    &   (y = B → (ψχ))       ((A C B D) → (A, B {x, y ((x C y D) φ)} ↔ χ))

Theoremopelopab 4708* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))       (A, B {x, y φ} ↔ χ)

Theorembrab 4709* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))    &   R = {x, y φ}       (ARBχ)

Theoremopelopabaf 4710* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4708 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.)
xψ    &   yψ    &   A V    &   B V    &   ((x = A y = B) → (φψ))       (A, B {x, y φ} ↔ ψ)

Theoremopelopabf 4711* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4708 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
xψ    &   yχ    &   A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))       (A, B {x, y φ} ↔ χ)

Theoremssopab2 4712 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
(xy(φψ) → {x, y φ} {x, y ψ})

Theoremssopab2b 4713 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
({x, y φ} {x, y ψ} ↔ xy(φψ))

Theoremssopab2i 4714 Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
(φψ)       {x, y φ} {x, y ψ}

Theoremssopab2dv 4715* Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
(φ → (ψχ))       (φ → {x, y ψ} {x, y χ})

Theoremopabn0 4716 Non-empty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
({x, y φ} ≠ xyφ)

2.3.5  Set construction functions

Syntaxc1st 4717 Extend the definition of a class to include the first member an ordered pair function.
class 1st

Syntaxcswap 4718 Extend the definition of a class to include the swap function.
class Swap

Syntaxcsset 4719 Extend the definition of a class to include the subset relationship.
class S

Syntaxcsi 4720 Extend the definition of a class to include the singleton image.
class SI A

Syntaxccom 4721 Extend the definition of a class to include the composition of two classes.
class (A B)

Syntaxcima 4722 Extend the definition of a class to include the image of one class under another.
class (AB)

Definitiondf-1st 4723* Define a function that extracts the first member, or abscissa, of an ordered pair. (Contributed by SF, 5-Jan-2015.)
1st = {x, y z x = y, z}

Definitiondf-swap 4724* Define a function that swaps the two elements of an ordered pair. (Contributed by SF, 5-Jan-2015.)
Swap = {x, y zw(x = z, w y = w, z)}

Definitiondf-sset 4725* Define a relationship that holds between subsets. (Contributed by SF, 5-Jan-2015.)
S = {x, y x y}

Definitiondf-co 4726* Define the composition of two classes. (Contributed by SF, 5-Jan-2015.)
(A B) = {x, y z(xBz zAy)}

Definitiondf-ima 4727* Define the image of one class under another. (Contributed by SF, 5-Jan-2015.)
(AB) = {x y B yAx}

Definitiondf-si 4728* Define the singleton image of a class. (Contributed by SF, 5-Jan-2015.)
SI A = {x, y zw(x = {z} y = {w} zAw)}

Theoremel1st 4729* Membership in 1st. (Contributed by SF, 5-Jan-2015.)
(A 1stxy A = x, y, x)

Theorembr1stg 4730 The binary relationship over the 1st function. (Contributed by SF, 5-Jan-2015.)
((A V B W) → (A, B1st CA = C))

Theoremsetconslem1 4731* Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
A V    &   B V       (⟪{A}, B ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ↔ x B A = Phi x)

Theoremsetconslem2 4732* Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
A V    &   B V       (⟪{A}, B (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c) ↔ x B A = ( Phi x ∪ {0c}))

Theoremsetconslem3 4733 Lemma for set construction functions. Set up a mapping between Kuratowski and Quine ordered pairs. (Contributed by SF, 7-Jan-2015.)
A V    &   B V    &   C V       (⟪{{A}}, ⟪B, C⟫⟫ ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ A = B, C)

Theoremsetconslem4 4734* Lemma for set construction functions. Create a mapping between the two types of ordered pair abstractions. (Contributed by SF, 7-Jan-2015.)
11((((V ×k V) ×k V) ∩ k ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k A) = {x, y x, y A}

Theoremsetconslem5 4735 Lemma for set construction theorems. The big expression in the middle of setconslem4 4734 forms a set. (Contributed by SF, 7-Jan-2015.)
∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) V

Theoremsetconslem6 4736* Lemma for the set construction functions. Invert the expression from setconslem4 4734. (Contributed by SF, 7-Jan-2015.)
(((V ×k (V ×k V)) ∩ ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11A) = {z xy(z = ⟪x, y x, y A)}

Theoremsetconslem7 4737 Lemma for the set construction theorems. Reorganized version of setconslem3 4733. (Contributed by SF, 4-Feb-2015.)
A V    &   B V    &   C V       (⟪{{C}}, ⟪A, B⟫⟫ ∼ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ A = B, C)

Theoremdf1st2 4738 Express the 1st function via the set construction functions. (Contributed by SF, 4-Feb-2015.)
1st = ⋃11((((V ×k V) ×k V) ∩ k ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k ( ∼ (( Ins2k Ins3k Sk ⊕ ( Ins2k Ins2k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) “k 11c))

Theorem1stex 4739 The 1st function is a set. (Contributed by SF, 6-Jan-2015.)
1st V

Theoremelswap 4740* Membership in the Swap function. (Contributed by SF, 6-Jan-2015.)
(A Swap xy A = x, y, y, x)

Theoremdfswap2 4741 Express the Swap function via set construction operators. (Contributed by SF, 6-Jan-2015.)
Swap = (( ∼ (( Ins2k Ins2k Sk ⊕ ((( Ins2k ( Ins2k Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)) ∩ Ins3k SIk SIk SIk SIk SIk Imagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) “k 1111111c) ∪ (( Ins2k ( Ins3k SIk SIk ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k Ins3k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c)) ∩ Ins3k SIk SIk SIk SIk SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 1111111c))) “k 11111c) “k 11c) “k V)

Theoremswapex 4742 The Swap function is a set. (Contributed by SF, 6-Jan-2015.)
Swap V

Theoremdfsset2 4743 Express the S relationship via the set construction functors. (Contributed by SF, 7-Jan-2015.)
S = ⋃11((((V ×k V) ×k V) ∩ k ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k Sk )

Theoremssetex 4744 The subset relationship is a set. (Contributed by SF, 6-Jan-2015.)
S V

Theoremdfima2 4745 Express the image functor in terms of the set construction functions. (Contributed by SF, 7-Jan-2015.)
(AB) = ((((V ×k (V ×k V)) ∩ ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11A) “k B)

Theoremimaexg 4746 The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
((A V B W) → (AB) V)

Theoremimaex 4747 The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
A V    &   B V       (AB) V

Theoremdfco1 4748 Express Quine composition via Kuratowski composition. (Contributed by SF, 7-Jan-2015.)
(A B) = ⋃11((((V ×k V) ×k V) ∩ k ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k ((((V ×k (V ×k V)) ∩ ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11A) k (((V ×k (V ×k V)) ∩ ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11B)))

Theoremcoexg 4749 The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
((A V B W) → (A B) V)

Theoremcoex 4750 The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
A V    &   B V       (A B) V

Theoremdfsi2 4751 Express singleton image in terms of the Kuratowski singleton image. (Contributed by SF, 7-Jan-2015.)
SI A = ⋃11((((V ×k V) ×k V) ∩ k ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k SIk (((V ×k (V ×k V)) ∩ ∼ (( Ins3k SIk SIk SkIns2k ( Ins3k ( Sk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SkIns3k SIk ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11A))

Theoremsiexg 4752 The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
(A V SI A V)

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

Theoremelima 4754* Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 19-Apr-2004.)
(A (BC) ↔ x C xBA)

Theoremelima2 4755* Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 11-Aug-2004.)
(A (BC) ↔ x(x C xBA))

Theoremelima3 4756* Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 14-Aug-1994.)
(A (BC) ↔ x(x C x, A B))

Theorembrssetg 4757 Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
((A V B W) → (A S BA B))

Theorembrsset 4758 Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
A V    &   B V       (A S BA B)

Theorembrssetsn 4759 Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
A V    &   B V       ({A} S BA B)

Theoremopelssetsn 4760 Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
A V    &   B V       ({A}, B S A B)

Theorembrsi 4761* Binary relationship over a singleton image. (Contributed by SF, 11-Feb-2015.)
(A SI RBxy(A = {x} B = {y} xRy))

2.3.6  Epsilon and identity relations

Syntaxcep 4762 Extend class notation to include the epsilon relation.
class E

Syntaxcid 4763 Extend the definition of a class to include identity relation.
class I

Definitiondf-eprel 4764* Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. (Contributed by SF, 5-Jan-2015.)
E = {x, y x y}

Theoremepelc 4765 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
B V       (A E BA B)

Theoremepel 4766 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
(x E yx y)

Definitiondf-id 4767* Define the identity relation. Definition 9.15 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
I = {x, y x = y}

Theoremdfid3 4768 A stronger version of df-id 4767 that doesn't require x and y 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.)
I = {x, y x = y}

Theoremdfid2 4769 Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)
I = {x, x x = x}

2.3.7  Functions and relations

Syntaxcxp 4770 Extend the definition of a class to include the cross product.
class (A × B)

Syntaxccnv 4771 Extend the definition of a class to include the converse of a class.
class A

Syntaxcdm 4772 Extend the definition of a class to include the domain of a class.
class dom A

Syntaxcrn 4773 Extend the definition of a class to include the range of a class.
class ran A

Syntaxcres 4774 Extend the definition of a class to include the restriction of a class. (Read: The restriction of A to B.)
class (A B)

Syntaxwfun 4775 Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A

Syntaxwfn 4776 Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B.)
wff A Fn B

Syntaxwf 4777 Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B.)
wff F:A–→B

Syntaxwf1 4778 Extend the definition of a wff to include one-to-one functions. (Read: F maps A one-to-one into B.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff F:A1-1B

Syntaxwfo 4779 Extend the definition of a wff to include onto functions. (Read: F maps A onto B.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff F:AontoB

Syntaxwf1o 4780 Extend the definition of a wff to include one-to-one onto functions. (Read: F maps A one-to-one onto B.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff F:A1-1-ontoB

Syntaxcfv 4781 Extend the definition of a class to include the value of a function. (Read: The value of F at A, or "F of A.")
class (FA)

Syntaxwiso 4782 Extend the definition of a wff to include the isomorphism property. (Read: H is an R, S isomorphism of A onto B.)
wff H Isom R, S (A, B)

Syntaxc2nd 4783 Extend the definition of a class to include the second function.
class 2nd

Definitiondf-xp 4784* Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
(A × B) = {x, y (x A y B)}

Definitiondf-cnv 4785* 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.)
A = {x, y yAx}

Definitiondf-rn 4786 Define the range of a class. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by SF, 5-Jan-2015.)
ran A = (A “ V)

Definitiondf-dm 4787 Define the domain of a class. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by SF, 5-Jan-2015.)
dom A = ran A

Definitiondf-res 4788 Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. (Contributed by SF, 5-Jan-2015.)
(A B) = (A ∩ (B × V))

Definitiondf-fun 4789 Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5119, dffun3 5120, dffun4 5121, dffun5 5122, dffun6 5124, dffun7 5133, dffun8 5134, and dffun9 5135. (Contributed by SF, 5-Jan-2015.) (Revised by Scott Fenton, 14-Apr-2021.)
(Fun A ↔ (A A) I )

Definitiondf-fn 4790 Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5224, dffn3 5229, dffn4 5275, and dffn5 5363. (Contributed by SF, 5-Jan-2015.)
(A Fn B ↔ (Fun A dom A = B))

Definitiondf-f 4791 Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5419, dff3 5420, and dff4 5421. (Contributed by SF, 5-Jan-2015.)
(F:A–→B ↔ (F Fn A ran F B))

Definitiondf-f1 4792 Define a one-to-one function. For equivalent definitions see dff12 5257 and dff13 5471. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)
(F:A1-1B ↔ (F:A–→B Fun F))

Definitiondf-fo 4793 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 5273, dffo3 5422, dffo4 5423, and dffo5 5424. (Contributed by SF, 5-Jan-2015.)
(F:AontoB ↔ (F Fn A ran F = B))

Definitiondf-f1o 4794 Define a one-to-one onto function. For equivalent definitions see dff1o2 5291, dff1o3 5292, dff1o4 5294, and dff1o5 5295. 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.)
(F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))

Definitiondf-fv 4795* Define the value of a function. (Contributed by SF, 5-Jan-2015.)
(FA) = (℩xAFx)

Definitiondf-iso 4796* Define the isomorphism predicate. We read this as "H is an R, S isomorphism of A onto B." Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by SF, 5-Jan-2015.)
(H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))

Definitiondf-2nd 4797* Define the 2nd function. This function extracts the second member of an ordered pair. (Contributed by SF, 5-Jan-2015.)
2nd = {x, y z x = z, y}

Theoremxpeq1 4798 Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
(A = B → (A × C) = (B × C))

Theoremxpeq2 4799 Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
(A = B → (C × A) = (C × B))

Theoremelxpi 4800* Membership in a cross product. Uses fewer axioms than elxp 4801. (Contributed by NM, 4-Jul-1994.)
(A (B × C) → xy(A = x, y (x B y C)))

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 >