HomeHome New Foundations Explorer
Theorem List (p. 48 of 64)
< Previous  Next >
Bad symbols? Try the
GIF 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)
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 Nonempty 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)))
    < 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-6338
  Copyright terms: Public domain < Previous  Next >