Theorem List for New Foundations Explorer - 5701-5800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fvmpts 5701* |
Value of a function given in maps-to notation, using explicit class
substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
⊢ F =
(x ∈
C ↦
B) ⇒ ⊢ ((A ∈ C ∧ [A /
x]B ∈ V) → (F
‘A) = [A / x]B) |
|
Theorem | fvmptd 5702* |
Deduction version of fvmpt 5700. (Contributed by Scott Fenton,
18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ (φ
→ F = (x ∈ D ↦ B))
& ⊢ ((φ
∧ x =
A) → B = C)
& ⊢ (φ
→ A ∈ D)
& ⊢ (φ
→ C ∈ V) ⇒ ⊢ (φ
→ (F ‘A) = C) |
|
Theorem | fvmpt2i 5703* |
Value of a function given by the "maps to" notation. (Contributed by
Mario Carneiro, 23-Apr-2014.)
|
⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (x ∈ A →
(F ‘x) = ( I ‘B)) |
|
Theorem | fvmpt2 5704* |
Value of a function given by the "maps to" notation. (Contributed by
FL, 21-Jun-2010.)
|
⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ ((x ∈ A ∧ B ∈ C) →
(F ‘x) = B) |
|
Theorem | fvmptss 5705* |
If all the values of the mapping are subsets of a class C, then so
is any evaluation of the mapping, even if D is not in the base set
A. (Contributed by
Mario Carneiro, 13-Feb-2015.)
|
⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (∀x ∈ A B ⊆ C →
(F ‘D) ⊆ C) |
|
Theorem | dffn5v 5706* |
Representation of a function in terms of its values. (Contributed by
FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|
⊢ (F Fn
A ↔ F = (x ∈ A ↦ (F
‘x))) |
|
Theorem | fnov2 5707* |
Representation of a function in terms of its values. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
⊢ (F Fn
(A × B) ↔ F =
(x ∈
A, y
∈ B
↦ (xFy))) |
|
Theorem | mpt2mptx 5708* |
Express a two-argument function as a one-argument function, or
vice-versa. In this version B(x) is
not assumed to be constant
w.r.t x. (Contributed
by Mario Carneiro, 29-Dec-2014.)
|
⊢ (z = 〈x, y〉 →
C = D) ⇒ ⊢ (z ∈ ∪x ∈ A ({x} ×
B) ↦
C) = (x ∈ A, y ∈ B ↦ D) |
|
Theorem | mpt2mpt 5709* |
Express a two-argument function as a one-argument function, or
vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by
Mario Carneiro, 29-Dec-2014.)
|
⊢ (z = 〈x, y〉 →
C = D) ⇒ ⊢ (z ∈ (A ×
B) ↦
C) = (x ∈ A, y ∈ B ↦ D) |
|
Theorem | ovmpt4g 5710* |
Value of a function given by the "maps to" notation. (This is the
operation analog of fvmpt2 5704.) (Contributed by NM, 21-Feb-2004.)
(Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ ((x ∈ A ∧ y ∈ B ∧ C ∈ V) →
(xFy) = C) |
|
Theorem | ov2gf 5711* |
The value of an operation class abstraction. A version of ovmpt2g 5715
using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ℲxA & ⊢ ℲyA & ⊢ ℲyB & ⊢ ℲxG & ⊢ ℲyS & ⊢ (x =
A → R = G)
& ⊢ (y =
B → G = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R) ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) |
|
Theorem | ovmpt2x 5712* |
The value of an operation class abstraction. Variant of ovmpt2ga 5713
which does not require D and x to be distinct. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ (x =
A → D = L)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R) ⇒ ⊢ ((A ∈ C ∧ B ∈ L ∧ S ∈ H) →
(AFB) = S) |
|
Theorem | ovmpt2ga 5713* |
Value of an operation given by a maps-to rule. Equivalent to ov2ag 5598.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R) ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) |
|
Theorem | ovmpt2a 5714* |
Value of an operation given by a maps-to rule. Equivalent to
ov2ag 5598. (Contributed by set.mm contributors,
19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R)
& ⊢ S ∈ V ⇒ ⊢ ((A ∈ C ∧ B ∈ D) →
(AFB) = S) |
|
Theorem | ovmpt2g 5715* |
Value of an operation given by a maps-to rule. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Jun-2012.)
(Contributed by set.mm contributors, 2-Oct-2007.) (Revised by set.mm
contributors, 24-Jul-2012.)
|
⊢ (x =
A → R = G)
& ⊢ (y =
B → G = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R) ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) |
|
Theorem | ovmpt2 5716* |
Value of an operation given by a maps-to rule. Equivalent to ov2 in
set.mm. (Contributed by set.mm contributors, 12-Sep-2011.)
|
⊢ (x =
A → R = G)
& ⊢ (y =
B → G = S)
& ⊢ F =
(x ∈
C, y
∈ D
↦ R)
& ⊢ S ∈ V ⇒ ⊢ ((A ∈ C ∧ B ∈ D) →
(AFB) = S) |
|
Theorem | rnmpt2 5717* |
The range of an operation given by the "maps to" notation.
(Contributed
by FL, 20-Jun-2011.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ ran F =
{z ∣
∃x
∈ A
∃y
∈ B
z = C} |
|
Theorem | mptv 5718* |
Function with universal domain in maps-to notation. (Contributed by
set.mm contributors, 16-Aug-2013.)
|
⊢ (x ∈ V ↦ B) = {〈x, y〉 ∣ y = B} |
|
Theorem | mpt2v 5719* |
Operation with universal domain in maps-to notation. (Contributed by
set.mm contributors, 16-Aug-2013.)
|
⊢ (x ∈ V, y ∈ V ↦ C) = {〈〈x, y〉, z〉 ∣ z =
C} |
|
Theorem | mptresid 5720* |
The restricted identity expressed with the "maps to" notation.
(Contributed by FL, 25-Apr-2012.)
|
⊢ (x ∈ A ↦ x) = ( I
↾ A) |
|
Theorem | fvmptex 5721* |
Express a function F whose
value B may not always be a
set in
terms of another function G for which sethood is guaranteed. (Note
that ( I ‘B) is
just shorthand for
if(B ∈ V, B, ∅), and it is always a set by fvex 5339.) Note
also that these functions are not the same; wherever B(C) is
not
a set, C is not in the
domain of F (so it evaluates
to the empty
set), but C is in the
domain of G, and G(C) is defined
to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
⊢ F =
(x ∈
A ↦
B)
& ⊢ G =
(x ∈
A ↦ ( I
‘B)) ⇒ ⊢ (F
‘C) = (G ‘C) |
|
Theorem | fvmptf 5722* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5698 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
⊢ ℲxA & ⊢ ℲxC & ⊢ (x =
A → B = C)
& ⊢ F =
(x ∈
D ↦
B) ⇒ ⊢ ((A ∈ D ∧ C ∈ V) →
(F ‘A) = C) |
|
Theorem | fvmptnf 5723* |
The value of a function given by an ordered-pair class abstraction is
the empty set when the class it would otherwise map to is a proper
class. This version of fvmptn 5724 uses bound-variable hypotheses
instead
of distinct variable conditions. (Contributed by NM, 21-Oct-2003.)
(Revised by Mario Carneiro, 11-Sep-2015.)
|
⊢ ℲxA & ⊢ ℲxC & ⊢ (x =
A → B = C)
& ⊢ F =
(x ∈
D ↦
B) ⇒ ⊢ (¬ C
∈ V → (F ‘A) =
∅) |
|
Theorem | fvmptn 5724* |
This somewhat non-intuitive theorem tells us the value of its function
is the empty set when the class C it would otherwise map to is a
proper class. This is a technical lemma that can help eliminate
redundant sethood antecedents otherwise required by fvmptg 5698.
(Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro,
9-Sep-2013.)
|
⊢ (x =
D → B = C)
& ⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (¬ C
∈ V → (F ‘D) =
∅) |
|
Theorem | fvmptss2 5725* |
A mapping always evaluates to a subset of the substituted expression in
the mapping, even if this is a proper class, or we are out of the
domain. (Contributed by Mario Carneiro, 13-Feb-2015.)
|
⊢ (x =
D → B = C)
& ⊢ F =
(x ∈
A ↦
B) ⇒ ⊢ (F
‘D) ⊆ C |
|
Theorem | f1od 5726* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
⊢ F =
(x ∈
A ↦
C)
& ⊢ ((φ
∧ x ∈ A) →
C ∈
W)
& ⊢ ((φ
∧ y ∈ B) →
D ∈
X)
& ⊢ (φ
→ ((x ∈ A ∧ y = C) ↔ (y
∈ B
∧ x =
D))) ⇒ ⊢ (φ
→ F:A–1-1-onto→B) |
|
Theorem | f1o2d 5727* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
⊢ F =
(x ∈
A ↦
C)
& ⊢ ((φ
∧ x ∈ A) →
C ∈
B)
& ⊢ ((φ
∧ y ∈ B) →
D ∈
A)
& ⊢ ((φ
∧ (x
∈ A
∧ y ∈ B)) →
(x = D
↔ y = C)) ⇒ ⊢ (φ
→ F:A–1-1-onto→B) |
|
Theorem | dfswap3 5728* |
Alternate definition of Swap as an
operator abstraction.
(Contributed by SF, 23-Feb-2015.)
|
⊢ Swap = {〈〈x, y〉, z〉 ∣ z = 〈y, x〉} |
|
Theorem | dfswap4 5729* |
Alternate definition of Swap as an
operator mapping. (Contributed
by SF, 23-Feb-2015.)
|
⊢ Swap = (x ∈ V, y ∈ V ↦ 〈y, x〉) |
|
Theorem | fmpt2x 5730* |
Functionality, domain and codomain of a class given by the "maps to"
notation, where B(x) is not constant but depends on x.
(Contributed by NM, 29-Dec-2014.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ (∀x ∈ A ∀y ∈ B C ∈ D ↔
F:∪x ∈ A ({x} × B)–→D) |
|
Theorem | fmpt2 5731* |
Functionality, domain and range of a class given by the "maps to"
notation. (Contributed by FL, 17-May-2010.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ (∀x ∈ A ∀y ∈ B C ∈ D ↔
F:(A
× B)–→D) |
|
Theorem | fnmpt2 5732* |
Functionality and domain of a class given by the "maps to" notation.
(Contributed by FL, 17-May-2010.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C) ⇒ ⊢ (∀x ∈ A ∀y ∈ B C ∈ V →
F Fn (A × B)) |
|
Theorem | fnmpt2i 5733* |
Functionality and domain of a class given by the "maps to" notation.
(Contributed by FL, 17-May-2010.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C)
& ⊢ C ∈ V ⇒ ⊢ F Fn
(A × B) |
|
Theorem | dmmpt2 5734* |
Domain of a class given by the "maps to" notation. (Contributed by
FL,
17-May-2010.)
|
⊢ F =
(x ∈
A, y
∈ B
↦ C)
& ⊢ C ∈ V ⇒ ⊢ dom F =
(A × B) |
|
2.3.10 Set construction lemmas
|
|
Syntax | ctxp 5735 |
Extend the definition of a class to include the tail cross product.
|
class
(A ⊗ B) |
|
Definition | df-txp 5736 |
Define the tail cross product of two classes. Definition from [Holmes]
p. 40. See brtxp 5783 for membership. (Contributed by SF,
9-Feb-2015.)
|
⊢ (A ⊗
B) = ((◡1st ∘ A) ∩
(◡2nd ∘ B)) |
|
Syntax | cpprod 5737 |
Extend the definition of a class to include the parallel product
operation.
|
class
PProd (A, B) |
|
Definition | df-pprod 5738 |
Define the parallel product operation. (Contributed by SF,
9-Feb-2015.)
|
⊢ PProd (A, B) =
((A ∘
1st ) ⊗ (B ∘ 2nd )) |
|
Syntax | cfix 5739 |
Extend the definition of a class to include the fixed points of a
relationship.
|
class
Fix A |
|
Definition | df-fix 5740 |
Define the fixed points of a relationship. (Contributed by SF,
9-Feb-2015.)
|
⊢ Fix A = ran (A
∩ I ) |
|
Syntax | ccup 5741 |
Extend the definition of a class to include the cup function.
|
class
Cup |
|
Definition | df-cup 5742* |
Define the cup function. (Contributed by SF, 9-Feb-2015.)
|
⊢ Cup = (x ∈ V, y ∈ V ↦ (x ∪
y)) |
|
Syntax | cdisj 5743 |
Extend the definition of a class to include the disjoint relationship.
|
class
Disj |
|
Definition | df-disj 5744* |
Define the relationship of all disjoint sets. (Contributed by SF,
9-Feb-2015.)
|
⊢ Disj = {〈x, y〉 ∣ (x ∩
y) = ∅} |
|
Syntax | caddcfn 5745 |
Extend the definition of a class to include the cardinal sum function.
|
class
AddC |
|
Definition | df-addcfn 5746* |
Define the function representing cardinal sum. (Contributed by SF,
9-Feb-2015.)
|
⊢ AddC = (x ∈ V, y ∈ V ↦ (x
+c y)) |
|
Syntax | ccompose 5747 |
Extend the definition of a class to include the compostion function.
|
class
Compose |
|
Definition | df-compose 5748* |
Define the composition function. (Contributed by Scott Fenton,
19-Apr-2021.)
|
⊢ Compose =
(x ∈ V,
y ∈ V
↦ (x
∘ y)) |
|
Syntax | cins2 5749 |
Extend the definition of a class to include the second insertion
operation.
|
class
Ins2 A |
|
Definition | df-ins2 5750 |
Define the second insertion operation. (Contributed by SF,
9-Feb-2015.)
|
⊢ Ins2 A = (V ⊗ A) |
|
Syntax | cins3 5751 |
Extend the definition of a class to include the third insertion
operation.
|
class
Ins3 A |
|
Definition | df-ins3 5752 |
Define the third insertion operation. (Contributed by SF, 9-Feb-2015.)
|
⊢ Ins3 A = (A ⊗
V) |
|
Syntax | cimage 5753 |
Extend the definition of a class to include the image function.
|
class
ImageA |
|
Definition | df-image 5754 |
Define the image function of a class. (Contributed by SF, 9-Feb-2015.)
(Revised by Scott Fenton, 19-Apr-2021.)
|
⊢ ImageA =
∼ (( Ins2 S
⊕ Ins3 ( S
∘ ◡ SI A)) “ 1c) |
|
Syntax | cins4 5755 |
Extend the definition of a class to include the fourth insertion
operation.
|
class
Ins4 A |
|
Definition | df-ins4 5756 |
Define the fourth insertion operation. (Contributed by SF,
9-Feb-2015.)
|
⊢ Ins4 A = (◡(1st ⊗ ((1st
∘ 2nd ) ⊗
((1st ∘ 2nd ) ∘ 2nd ))) “ A) |
|
Syntax | csi3 5757 |
Extend the definition of a class to include the triple singleton image.
|
class
SI3 A |
|
Definition | df-si3 5758 |
Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)
|
⊢ SI3 A = (( SI
1st ⊗ ( SI
(1st ∘ 2nd )
⊗ SI (2nd ∘ 2nd ))) “ ℘1A) |
|
Syntax | cfuns 5759 |
Extend the definition of a class to include the set of all functions.
|
class
Funs |
|
Definition | df-funs 5760 |
Define the class of all functions. (Contributed by SF, 9-Feb-2015.)
|
⊢ Funs = {f ∣ Fun f} |
|
Syntax | cfns 5761 |
Extend the definition of a class to include the function with domain
relationship.
|
class
Fns |
|
Definition | df-fns 5762* |
Define the function with domain relationship. (Contributed by SF,
9-Feb-2015.)
|
⊢ Fns = {〈f, a〉 ∣ f Fn
a} |
|
Syntax | ccross 5763 |
Extend the definition of a class to include the cross product function.
|
class
Cross |
|
Definition | df-cross 5764* |
Define the cross product function. (Contributed by SF, 9-Feb-2015.)
|
⊢ Cross = (x ∈ V, y ∈ V ↦ (x ×
y)) |
|
Syntax | cpw1fn 5765 |
Extend the definition of a class to include the unit power class
function.
|
class
Pw1Fn |
|
Definition | df-pw1fn 5766 |
Define the function that takes a singleton to the unit power class of its
member. This function is defined in such a way as to ensure
stratification. (Contributed by SF, 9-Feb-2015.)
|
⊢ Pw1Fn = (x ∈
1c ↦ ℘1∪x) |
|
Syntax | cfullfun 5767 |
Extend the definition of a class to include the full function
operation.
|
class
FullFun F |
|
Definition | df-fullfun 5768 |
Define the full function operator. This is a function over V
that
agrees with the function value of F at every point. (Contributed by
SF, 9-Feb-2015.)
|
⊢ FullFun F = ((( I ∘
F) ∖ (
∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) × {∅})) |
|
Syntax | cdomfn 5769 |
Extend the definition of a class to include the domain function.
|
class
Dom |
|
Definition | df-domfn 5770 |
Define the domain function. This is a function wrapper for the domain
operator. (Contributed by Scott Fenton, 9-Aug-2019.)
|
⊢ Dom = (x ∈ V ↦ dom x) |
|
Syntax | cranfn 5771 |
Extend the definition of a class to include the range function.
|
class
Ran |
|
Definition | df-ranfn 5772 |
Define the range function. This is a function wrapper for the range
operator. (Contributed by Scott Fenton, 9-Aug-2019.)
|
⊢ Ran = (x ∈ V ↦ ran x) |
|
Theorem | brsnsi 5773 |
Binary relationship of singletons in a singleton image. (Contributed by
SF, 9-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({A} SI R{B} ↔ ARB) |
|
Theorem | opsnelsi 5774 |
Ordered pair membership of singletons in a singleton image.
(Contributed by SF, 9-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈{A}, {B}〉 ∈ SI R ↔ 〈A, B〉 ∈ R) |
|
Theorem | brsnsi1 5775* |
Binary relationship of a singleton to an arbitrary set in a singleton
image. (Contributed by SF, 9-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ ({A} SI RB ↔ ∃x(B = {x} ∧ ARx)) |
|
Theorem | brsnsi2 5776* |
Binary relationship of an arbitrary set to a singleton in a singleton
image. (Contributed by SF, 9-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ (B SI R{A} ↔ ∃x(B = {x} ∧ xRA)) |
|
Theorem | brco1st 5777 |
Binary relationship of composition with 1st.
(Contributed by SF,
9-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉(R ∘ 1st )C ↔ ARC) |
|
Theorem | brco2nd 5778 |
Binary relationship of composition with 2nd.
(Contributed by SF,
9-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉(R ∘ 2nd )C ↔ BRC) |
|
Theorem | txpeq1 5779 |
Equality theorem for tail cross product. (Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (A =
B → (A ⊗ C) =
(B ⊗ C)) |
|
Theorem | txpeq2 5780 |
Equality theorem for tail cross product. (Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (A =
B → (C ⊗ A) =
(C ⊗ B)) |
|
Theorem | trtxp 5781 |
Trinary relationship over a tail cross product. (Contributed by SF,
13-Feb-2015.)
|
⊢ (A(R ⊗ S)〈B, C〉 ↔ (ARB ∧ ASC)) |
|
Theorem | oteltxp 5782 |
Ordered triple membership in a tail cross product. (Contributed by SF,
13-Feb-2015.)
|
⊢ (〈A, 〈B, C〉〉 ∈ (R ⊗
S) ↔ (〈A, B〉 ∈ R ∧ 〈A, C〉 ∈ S)) |
|
Theorem | brtxp 5783* |
Binary relationship over a tail cross product. (Contributed by SF,
11-Feb-2015.)
|
⊢ (A(R ⊗ S)B ↔
∃x∃y(B = 〈x, y〉 ∧ ARx ∧ ASy)) |
|
Theorem | txpexg 5784 |
The tail cross product of two sets is a set. (Contributed by SF,
9-Feb-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
(A ⊗ B) ∈
V) |
|
Theorem | txpex 5785 |
The tail cross product of two sets is a set. (Contributed by SF,
9-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ⊗
B) ∈
V |
|
Theorem | restxp 5786 |
Restriction distributes over tail cross product. (Contributed by SF,
24-Feb-2015.)
|
⊢ ((A
⊗ B) ↾ C) =
((A ↾
C) ⊗ (B ↾ C)) |
|
Theorem | elfix 5787 |
Membership in the fixed points of a relationship. (Contributed by SF,
11-Feb-2015.)
|
⊢ (A ∈ Fix R ↔ ARA) |
|
Theorem | fixexg 5788 |
The fixed points of a set form a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ (R ∈ V →
Fix R ∈ V) |
|
Theorem | fixex 5789 |
The fixed points of a set form a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ R ∈ V ⇒ ⊢ Fix R ∈
V |
|
Theorem | op1st2nd 5790 |
Express equality to an ordered pair via 1st and 2nd.
(Contributed by SF, 12-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ((C1st A ∧ C2nd B) ↔ C =
〈A,
B〉) |
|
Theorem | otelins2 5791 |
Ordered triple membership in Ins2.
(Contributed by SF,
13-Feb-2015.)
|
⊢ B ∈ V ⇒ ⊢ (〈A, 〈B, C〉〉 ∈ Ins2 R ↔ 〈A, C〉 ∈ R) |
|
Theorem | otelins3 5792 |
Ordered triple membership in Ins3.
(Contributed by SF,
13-Feb-2015.)
|
⊢ C ∈ V ⇒ ⊢ (〈A, 〈B, C〉〉 ∈ Ins3 R ↔ 〈A, B〉 ∈ R) |
|
Theorem | brimage 5793 |
Binary relationship over the image function. (Contributed by SF,
11-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (AImageRB ↔ B =
(R “ A)) |
|
Theorem | oqelins4 5794 |
Ordered quadruple membership in Ins4. (Contributed by SF,
13-Feb-2015.)
|
⊢ D ∈ V ⇒ ⊢ (〈A, 〈B, 〈C, D〉〉〉 ∈ Ins4 R ↔ 〈A, 〈B, C〉〉 ∈ R) |
|
Theorem | ins2exg 5795 |
Ins2 preserves sethood.
(Contributed by SF, 9-Mar-2015.)
|
⊢ (A ∈ V →
Ins2 A ∈ V) |
|
Theorem | ins3exg 5796 |
Ins3 preserves sethood.
(Contributed by SF, 22-Feb-2015.)
|
⊢ (A ∈ V →
Ins3 A ∈ V) |
|
Theorem | ins2ex 5797 |
Ins2 preserves sethood.
(Contributed by SF, 12-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ Ins2 A ∈
V |
|
Theorem | ins3ex 5798 |
Ins3 preserves sethood.
(Contributed by SF, 12-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ Ins3 A ∈
V |
|
Theorem | ins4ex 5799 |
Ins4 preserves sethood.
(Contributed by SF, 12-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ Ins4 A ∈
V |
|
Theorem | imageexg 5800 |
The image function of a set is a set. (Contributed by SF,
11-Feb-2015.)
|
⊢ (A ∈ V →
ImageA ∈
V) |