Home New Foundations ExplorerTheorem List (p. 48 of 64) < Previous  Next > Bad symbols? Use Firefox (or GIF version for IE).

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

Theorembrab 4701* 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 4702* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4700 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 4703* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4700 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 4704 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 4705 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 4706 Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
(φψ)       {x, y φ} {x, y ψ}

Theoremssopab2dv 4707* 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 4708 Non-empty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
({x, y φ} ≠ xyφ)

2.3.5  Set construction functions

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

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

Syntaxcsset 4711 Extend the definition of a class to include the subset relationship.
class SSet

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

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

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

Definitiondf-1st 4715* Define a function that extracts the first member, or abscissa, of an ordered pair.
1st = {x, y z x = y, z}

Definitiondf-swap 4716* Define a function that swaps the two elements of an ordered pair.
Swap = {x, y zw(x = z, w y = w, z)}

Definitiondf-sset 4717* Define a relationship that holds between subsets.
SSet = {x, y x y}

Definitiondf-co 4718* Define the composition of two classes.
(A B) = {x, y z(xBz zAy)}

Definitiondf-ima 4719* Define the image of one class under another.
(AB) = {x y B yAx}

Definitiondf-si 4720* Define the singleton image of a class.
SI A = {x, y zw(x = {z} y = {w} zAw)}

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

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

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

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

Theoremsetconslem3 4725 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 SSetkIns2k ( Ins3k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) ↔ A = B, C)

Theoremsetconslem4 4726* 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 SSetkIns2k ( Ins3k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k A) = {x, y x, y A}

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

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

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

Theoremdf1st2 4730 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 SSetkIns2k ( Ins3k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k ( ∼ (( Ins2k Ins3k SSetk ⊕ ( Ins2k Ins2k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins3k SIk SIk (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c) “k 11c))

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

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

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

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

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

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

Theoremdfima2 4737 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 SSetkIns2k ( Ins3k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11A) “k B)

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

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

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

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

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

Theoremdfsi2 4743 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 SSetkIns2k ( Ins3k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k SIk (((V ×k (V ×k V)) ∩ ∼ (( Ins3k SIk SIk SSetkIns2k ( Ins3k ( SSetk k SIk kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V)))) ∪ Ins2k (( Ins2k SSetkIns3k SIk ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c)) “k 111c))) “k 11111c)) “k 11A))

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

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

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

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

Theoremelima3 4748* 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 4749 Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
((A V B W) → (A SSet BA B))

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

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

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

Theorembrsi 4753* 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 4754 Extend class notation to include the epsilon relation.
class E

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

Definitiondf-eprel 4756* Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
E = {x, y x y}

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

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

Definitiondf-id 4759* Define the identity relation. Definition 9.15 of [Quine] p. 64.
I = {x, y x = y}

Theoremdfid3 4760 A stronger version of df-id 4759 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 4761 Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)
I = {x, x x = x}

2.3.7  Functions and relations

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

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

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

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

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

Syntaxwrel 4767 Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A

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

Syntaxwfn 4769 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 4770 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 4771 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 4772 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 4773 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 4774 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 4775 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 4776 Extend the definition of a class to include the second function.
class 2nd

Definitiondf-xp 4777* Define the cross product of two classes. Definition 9.11 of [Quine] p. 64.
(A × B) = {x, y (x A y B)}

Definitiondf-rel 4778 Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5079 and dfrel3 5097.
(Rel AA (V × V))

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

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

Definitiondf-dm 4781 Define the domain of a class. The notation "dom " is used by Enderton; other authors sometimes use script D.
dom A = ran A

Definitiondf-res 4782 Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24.
(A B) = (A ∩ (B × V))

Definitiondf-fun 4783 Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5152, dffun3 5153, dffun4 5154, dffun5 5155, dffun6 5157, dffun7 5167, dffun8 5168, and dffun9 5169.
(Fun A ↔ (Rel A (A A) I ))

Definitiondf-fn 4784 Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5261, dffn3 5267, dffn4 5314, and dffn5 5403.
(A Fn B ↔ (Fun A dom A = B))

Definitiondf-f 4785 Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5459, dff3 5460, and dff4 5461.
(F:A–→B ↔ (F Fn A ran F B))

Definitiondf-f1 4786 Define a one-to-one function. For equivalent definitions see dff12 5295 and dff13 5511. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow).
(F:A1-1B ↔ (F:A–→B Fun F))

Definitiondf-fo 4787 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 5312, dffo3 5462, dffo4 5463, and dffo5 5464.
(F:AontoB ↔ (F Fn A ran F = B))

Definitiondf-f1o 4788 Define a one-to-one onto function. For equivalent definitions see dff1o2 5331, dff1o3 5332, dff1o4 5334, and dff1o5 5335. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).
(F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))

Definitiondf-fv 4789* Define the value of a function.
(FA) = (℩xAFx)

Definitiondf-iso 4790* 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.
(H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))

Definitiondf-2nd 4791* Define the 2nd function. This function extracts the second member of an ordered pair.
2nd = {x, y z x = z, y}

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

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

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

Theoremelxp 4795* Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
(A (B × C) ↔ xy(A = x, y (x B y C)))

Theoremelxp2 4796* Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
(A (B × C) ↔ x B y C A = x, y)

Theoremxpeq12 4797 Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
((A = B C = D) → (A × C) = (B × D))

Theoremxpeq1i 4798 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
A = B       (A × C) = (B × C)

Theoremxpeq2i 4799 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
A = B       (C × A) = (C × B)

Theoremxpeq12i 4800 Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
A = B    &   C = D       (A × C) = (B × D)

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-6308
 Copyright terms: Public domain < Previous  Next >