Theorem List for New Foundations Explorer - 5501-5600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | opbr1st 5501 |
Binary relationship of an ordered pair over 1st.
(Contributed by
SF, 6-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉1st C ↔ A =
C) |
|
Theorem | opbr2nd 5502 |
Binary relationship of an ordered pair over 2nd.
(Contributed by
SF, 6-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (〈A, B〉2nd C ↔ B =
C) |
|
Theorem | dfid4 5503 |
Alternate definition of the identity relationship. (Contributed by SF,
11-Feb-2015.)
|
⊢ I = ( S ∩
◡ S
) |
|
Theorem | idex 5504 |
The identity relationship is a set. (Contributed by SF, 11-Feb-2015.)
|
⊢ I ∈
V |
|
Theorem | 1stfo 5505 |
1st is a mapping from the universe onto the universe.
(Contributed
by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
|
⊢ 1st :V–onto→V |
|
Theorem | 2ndfo 5506 |
2nd is a mapping from the universe onto the universe.
(Contributed
by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
|
⊢ 2nd :V–onto→V |
|
Theorem | dfdm4 5507 |
Alternate definition of domain. (Contributed by SF, 23-Feb-2015.)
|
⊢ dom A =
(1st “ A) |
|
Theorem | dfrn5 5508 |
Alternate definition of range. (Contributed by SF, 23-Feb-2015.)
|
⊢ ran A =
(2nd “ A) |
|
Theorem | brswap 5509* |
Binary relationship of Swap .
(Contributed by SF, 23-Feb-2015.)
|
⊢ (A Swap B ↔
∃x∃y(A = 〈x, y〉 ∧ B = 〈y, x〉)) |
|
Theorem | cnvswap 5510 |
The converse of Swap is Swap . (Contributed by SF,
23-Feb-2015.)
|
⊢ ◡ Swap = Swap
|
|
Theorem | swapf1o 5511 |
Swap is a bijection over the
universe. (Contributed by SF,
23-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
|
⊢ Swap
:V–1-1-onto→V |
|
Theorem | swapres 5512 |
Bijection law for restrictions of Swap
. (Contributed by SF,
23-Feb-2015.) (Modified by Scott Fenton, 17-Apr-2021.)
|
⊢ ( Swap ↾ A):A–1-1-onto→◡A |
|
Theorem | xpnedisj 5513 |
Cross products with non-equal singletons are disjoint. (Contributed by
SF, 23-Feb-2015.)
|
⊢ C ∈ V
& ⊢ C ≠
D ⇒ ⊢ ((A ×
{C}) ∩ (B × {D}))
= ∅ |
|
Theorem | opfv1st 5514 |
The value of the 1st function on an ordered pair.
(Contributed by
SF, 23-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (1st ‘〈A, B〉) = A |
|
Theorem | opfv2nd 5515 |
The value of the 2nd function on an ordered pair.
(Contributed by
SF, 23-Feb-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (2nd ‘〈A, B〉) = B |
|
Theorem | 1st2nd2 5516 |
Reconstruction of a member of a cross product in terms of its ordered
pair components. (Contributed by SF, 20-Oct-2013.)
|
⊢ (A ∈ (B ×
C) → A = 〈(1st ‘A), (2nd ‘A)〉) |
|
Theorem | fununiq 5517 |
Implicational form of part of the definition of a function.
(Contributed by SF, 24-Feb-2015.)
|
⊢ ((Fun F
∧ AFB ∧ AFC) → B =
C) |
|
Theorem | cnvsi 5518 |
Calculate the converse of a singleton image. (Contributed by SF,
26-Feb-2015.)
|
⊢ ◡ SI R = SI ◡R |
|
Theorem | dmsi 5519 |
Calculate the domain of a singleton image. Theorem X.4.29.I of [Rosser]
p. 301. (Contributed by SF, 26-Feb-2015.)
|
⊢ dom SI R = ℘1dom R |
|
Theorem | funsi 5520 |
The singleton image of a function is a function. (Contributed by SF,
26-Feb-2015.)
|
⊢ (Fun F
→ Fun SI F) |
|
Theorem | rnsi 5521 |
Calculate the range of a singleton image. Theorem X.4.29.II of [Rosser]
p. 302. (Contributed by SF, 26-Feb-2015.)
|
⊢ ran SI R = ℘1ran R |
|
Theorem | op1std 5522 |
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (C = 〈A, B〉 →
(1st ‘C) = A) |
|
Theorem | op2ndd 5523 |
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31-Aug-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (C = 〈A, B〉 →
(2nd ‘C) = B) |
|
Theorem | dmep 5524 |
The domain of the epsilon relationship. (Contributed by Scott Fenton,
20-Apr-2021.)
|
⊢ dom E = V |
|
2.3.8 Operations
|
|
Syntax | co 5525 |
Extend class notation to include the value of an operation F for two
arguments A and B. Note that the syntax is simply
three class
symbols in a row surrounded by parentheses. Since operation values are
the only possible class expressions consisting of three class expressions
in a row surrounded by parentheses, the syntax is unambiguous.
|
class
(AFB) |
|
Definition | df-ov 5526 |
Define the value of an operation. Definition of operation value in
[Enderton] p. 79. Note that the syntax
is simply three class expressions
in a row bracketed by parentheses. There are no restrictions of any kind
on what those class expressions may be, although only certain kinds of
class expressions - a binary operation F and its arguments A and
B- will be useful for
proving meaningful theorems. This definition
is well-defined, although not very meaningful, when classes A and/or
B are proper classes
(i.e. are not sets). On the other hand, we often
find uses for this definition when F is a proper class. F is
normally equal to a class of nested ordered pairs of the form defined by
df-oprab 5528. (Contributed by SF, 5-Jan-2015.)
|
⊢ (AFB) = (F ‘〈A, B〉) |
|
Syntax | coprab 5527 |
Extend class notation to include class abstraction (class builder) of
nested ordered pairs.
|
class
{〈〈x, y〉, z〉 ∣ φ} |
|
Definition | df-oprab 5528* |
Define the class abstraction (class builder) of a collection of nested
ordered pairs (for use in defining operations). This is a special case
of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y,
and z are distinct,
although the definition doesn't strictly require
it. See df-ov 5526 for the value of an operation. The brace
notation is
called "class abstraction" by Quine; it is also called a
"class builder"
in the literature. The value of the most common operation class builder
is given by ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)
|
⊢ {〈〈x, y〉, z〉 ∣ φ} =
{w ∣
∃x∃y∃z(w = 〈〈x, y〉, z〉 ∧ φ)} |
|
Theorem | oveq 5529 |
Equality theorem for operation value. (Contributed by set.mm
contributors, 28-Feb-1995.)
|
⊢ (F =
G → (AFB) = (AGB)) |
|
Theorem | oveq1 5530 |
Equality theorem for operation value. (Contributed by set.mm
contributors, 28-Feb-1995.)
|
⊢ (A =
B → (AFC) = (BFC)) |
|
Theorem | oveq2 5531 |
Equality theorem for operation value. (Contributed by set.mm
contributors, 28-Feb-1995.)
|
⊢ (A =
B → (CFA) = (CFB)) |
|
Theorem | oveq12 5532 |
Equality theorem for operation value. (Contributed by set.mm
contributors, 16-Jul-1995.)
|
⊢ ((A =
B ∧
C = D)
→ (AFC) = (BFD)) |
|
Theorem | oveq1i 5533 |
Equality inference for operation value. (Contributed by set.mm
contributors, 28-Feb-1995.)
|
⊢ A =
B ⇒ ⊢ (AFC) = (BFC) |
|
Theorem | oveq2i 5534 |
Equality inference for operation value. (Contributed by set.mm
contributors, 28-Feb-1995.)
|
⊢ A =
B ⇒ ⊢ (CFA) = (CFB) |
|
Theorem | oveq12i 5535 |
Equality inference for operation value. (The proof was shortened by
Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors,
28-Feb-1995.) (Revised by set.mm contributors, 22-Oct-2011.)
|
⊢ A =
B
& ⊢ C =
D ⇒ ⊢ (AFC) = (BFD) |
|
Theorem | oveqi 5536 |
Equality inference for operation value. (Contributed by set.mm
contributors, 24-Nov-2007.)
|
⊢ A =
B ⇒ ⊢ (CAD) = (CBD) |
|
Theorem | oveq1d 5537 |
Equality deduction for operation value. (Contributed by set.mm
contributors, 13-Mar-1995.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (AFC) = (BFC)) |
|
Theorem | oveq2d 5538 |
Equality deduction for operation value. (Contributed by set.mm
contributors, 13-Mar-1995.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (CFA) = (CFB)) |
|
Theorem | oveqd 5539 |
Equality deduction for operation value. (Contributed by set.mm
contributors, 9-Sep-2006.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (CAD) = (CBD)) |
|
Theorem | oveq12d 5540 |
Equality deduction for operation value. (The proof was shortened by
Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors,
13-Mar-1995.) (Revised by set.mm contributors, 22-Oct-2011.)
|
⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ (AFC) = (BFD)) |
|
Theorem | oveqan12d 5541 |
Equality deduction for operation value. (Contributed by set.mm
contributors, 10-Aug-1995.)
|
⊢ (φ
→ A = B)
& ⊢ (ψ
→ C = D) ⇒ ⊢ ((φ
∧ ψ)
→ (AFC) = (BFD)) |
|
Theorem | oveqan12rd 5542 |
Equality deduction for operation value. (Contributed by set.mm
contributors, 10-Aug-1995.)
|
⊢ (φ
→ A = B)
& ⊢ (ψ
→ C = D) ⇒ ⊢ ((ψ
∧ φ)
→ (AFC) = (BFD)) |
|
Theorem | oveq123d 5543 |
Equality deduction for operation value. (Contributed by FL,
22-Dec-2008.)
|
⊢ (φ
→ F = G)
& ⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ (AFC) = (BGD)) |
|
Theorem | nfovd 5544 |
Deduction version of bound-variable hypothesis builder nfov 5545.
(Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
⊢ (φ
→ ℲxA)
& ⊢ (φ
→ ℲxF)
& ⊢ (φ
→ ℲxB) ⇒ ⊢ (φ
→ Ⅎx(AFB)) |
|
Theorem | nfov 5545 |
Bound-variable hypothesis builder for operation value. (Contributed by
NM, 4-May-2004.)
|
⊢ ℲxA & ⊢ ℲxF & ⊢ ℲxB ⇒ ⊢ Ⅎx(AFB) |
|
Theorem | nfoprab1 5546 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ Ⅎx{〈〈x, y〉, z〉 ∣ φ} |
|
Theorem | nfoprab2 5547 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy,
30-Jul-2012.)
|
⊢ Ⅎy{〈〈x, y〉, z〉 ∣ φ} |
|
Theorem | nfoprab3 5548 |
The abstraction variables in an operation class abstraction are not
free. (Contributed by NM, 22-Aug-2013.)
|
⊢ Ⅎz{〈〈x, y〉, z〉 ∣ φ} |
|
Theorem | nfoprab 5549* |
Bound-variable hypothesis builder for an operation class abstraction.
(Contributed by NM, 22-Aug-2013.)
|
⊢ Ⅎwφ ⇒ ⊢ Ⅎw{〈〈x, y〉, z〉 ∣ φ} |
|
Theorem | oprabid 5550 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by Mario Carneiro, 20-Mar-2013.)
|
⊢ (〈〈x, y〉, z〉 ∈ {〈〈x, y〉, z〉 ∣ φ}
↔ φ) |
|
Theorem | ovex 5551 |
The result of an operation is a set. (Contributed by set.mm contributors,
13-Mar-1995.)
|
⊢ (AFB) ∈ V |
|
Theorem | csbovg 5552 |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|
⊢ (A ∈ D →
[A / x](BFC) = ([A
/ x]B[A /
x]F[A /
x]C)) |
|
Theorem | csbov12g 5553* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
⊢ (A ∈ D →
[A / x](BFC) = ([A
/ x]BF[A /
x]C)) |
|
Theorem | csbov1g 5554* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
⊢ (A ∈ D →
[A / x](BFC) = ([A
/ x]BFC)) |
|
Theorem | csbov2g 5555* |
Move class substitution in and out of an operation. (Contributed by NM,
12-Nov-2005.)
|
⊢ (A ∈ D →
[A / x](BFC) = (BF[A /
x]C)) |
|
Theorem | rspceov 5556* |
A frequently used special case of rspc2ev 2963 for operation values.
(Contributed by set.mm contributors, 21-Mar-2007.)
|
⊢ ((C ∈ A ∧ D ∈ B ∧ S = (CFD)) → ∃x ∈ A ∃y ∈ B S = (xFy)) |
|
Theorem | fnopovb 5557 |
Equivalence of operation value and ordered triple membership, analogous to
fnopfvb 5359. (Contributed by set.mm contributors,
17-Dec-2008.)
|
⊢ ((F Fn
(A × B) ∧ C ∈ A ∧ D ∈ B) → ((CFD) = R ↔
〈〈C, D〉, R〉 ∈ F)) |
|
Theorem | dfoprab2 5558* |
Class abstraction for operations in terms of class abstraction of
ordered pairs. (Contributed by set.mm contributors, 12-Mar-1995.)
|
⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈w,
z〉 ∣ ∃x∃y(w = 〈x, y〉 ∧ φ)} |
|
Theorem | hboprab1 5559* |
The abstraction variables in an operation class abstraction are not
free. (Unnecessary distinct variable restrictions were removed by David
Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors,
25-Apr-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
|
⊢ (w ∈ {〈〈x, y〉, z〉 ∣ φ}
→ ∀x w ∈ {〈〈x, y〉, z〉 ∣ φ}) |
|
Theorem | hboprab2 5560* |
The abstraction variables in an operation class abstraction are not
free. (Unnecessary distinct variable restrictions were removed by David
Abernethy, 30-Jul-2012.) (Contributed by set.mm contributors,
25-Apr-1995.) (Revised by set.mm contributors, 31-Jul-2012.)
|
⊢ (w ∈ {〈〈x, y〉, z〉 ∣ φ}
→ ∀y w ∈ {〈〈x, y〉, z〉 ∣ φ}) |
|
Theorem | hboprab3 5561* |
The abstraction variables in an operation class abstraction are not
free. (Contributed by set.mm contributors, 22-Aug-2013.)
|
⊢ (w ∈ {〈〈x, y〉, z〉 ∣ φ}
→ ∀z w ∈ {〈〈x, y〉, z〉 ∣ φ}) |
|
Theorem | hboprab 5562* |
Bound-variable hypothesis builder for an operation class abstraction.
(Contributed by set.mm contributors, 22-Aug-2013.)
|
⊢ (φ
→ ∀wφ) ⇒ ⊢ (u ∈ {〈〈x, y〉, z〉 ∣ φ}
→ ∀w u ∈ {〈〈x, y〉, z〉 ∣ φ}) |
|
Theorem | oprabbid 5563* |
Equivalent wff's yield equal operation class abstractions (deduction
rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
⊢ Ⅎxφ
& ⊢ Ⅎyφ
& ⊢ Ⅎzφ
& ⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ
→ {〈〈x, y〉, z〉 ∣ ψ} =
{〈〈x, y〉, z〉 ∣ χ}) |
|
Theorem | oprabbidv 5564* |
Equivalent wff's yield equal operation class abstractions (deduction
rule). (Contributed by NM, 21-Feb-2004.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ
→ {〈〈x, y〉, z〉 ∣ ψ} =
{〈〈x, y〉, z〉 ∣ χ}) |
|
Theorem | oprabbii 5565* |
Equivalent wff's yield equal operation class abstractions. (Unnecessary
distinct variable restrictions were removed by David Abernethy,
19-Jun-2012.) (Contributed by set.mm contributors, 28-May-1995.)
(Revised by set.mm contributors, 24-Jul-2012.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} = {〈〈x, y〉, z〉 ∣ ψ} |
|
Theorem | oprab4 5566* |
Two ways to state the domain of an operation. (Contributed by FL,
24-Jan-2010.)
|
⊢ {〈〈x, y〉, z〉 ∣ (〈x, y〉 ∈ (A × B)
∧ φ)}
= {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} |
|
Theorem | cbvoprab1 5567* |
Rule used to change first bound variable in an operation abstraction,
using implicit substitution. (Contributed by NM, 20-Dec-2008.)
(Revised by Mario Carneiro, 5-Dec-2016.)
|
⊢ Ⅎwφ
& ⊢ Ⅎxψ
& ⊢ (x =
w → (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈〈w, y〉, z〉 ∣ ψ} |
|
Theorem | cbvoprab2 5568* |
Change the second bound variable in an operation abstraction.
(Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
⊢ Ⅎwφ
& ⊢ Ⅎyψ
& ⊢ (y =
w → (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈〈x, w〉, z〉 ∣ ψ} |
|
Theorem | cbvoprab12 5569* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ Ⅎwφ
& ⊢ Ⅎvφ
& ⊢ Ⅎxψ
& ⊢ Ⅎyψ
& ⊢ ((x =
w ∧
y = v)
→ (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈〈w, v〉, z〉 ∣ ψ} |
|
Theorem | cbvoprab12v 5570* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by set.mm
contributors, 8-Oct-2004.)
|
⊢ ((x =
w ∧
y = v)
→ (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈〈w, v〉, z〉 ∣ ψ} |
|
Theorem | cbvoprab3 5571* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
22-Aug-2013.)
|
⊢ Ⅎwφ
& ⊢ Ⅎzψ
& ⊢ (z =
w → (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈〈x, y〉, w〉 ∣ ψ} |
|
Theorem | cbvoprab3v 5572* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Jun-2012.)
(Contributed by set.mm contributors, 8-Oct-2004.) (Revised by set.mm
contributors, 24-Jul-2012.)
|
⊢ (z =
w → (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} =
{〈〈x, y〉, w〉 ∣ ψ} |
|
Theorem | elimdelov 5573 |
Eliminate a hypothesis which is a predicate expressing membership in the
result of an operator (deduction version). (Contributed by Paul
Chapman, 25-Mar-2008.)
|
⊢ (φ
→ C ∈ (AFB))
& ⊢ Z ∈ (XFY) ⇒ ⊢ if(φ,
C, Z)
∈ ( if(φ, A,
X)F
if(φ, B, Y)) |
|
Theorem | dmoprab 5574* |
The domain of an operation class abstraction. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Jun-2012.)
(Contributed by set.mm contributors, 17-Mar-1995.) (Revised by set.mm
contributors, 24-Jul-2012.)
|
⊢ dom {〈〈x, y〉, z〉 ∣ φ} =
{〈x,
y〉 ∣ ∃zφ} |
|
Theorem | dmoprabss 5575* |
The domain of an operation class abstraction. (Contributed by set.mm
contributors, 24-Aug-1995.)
|
⊢ dom {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A ×
B) |
|
Theorem | rnoprab 5576* |
The range of an operation class abstraction. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Apr-2013.)
(Contributed by set.mm contributors, 30-Aug-2004.) (Revised by set.mm
contributors, 19-Apr-2013.)
|
⊢ ran {〈〈x, y〉, z〉 ∣ φ} =
{z ∣
∃x∃yφ} |
|
Theorem | rnoprab2 5577* |
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21-Mar-2012.)
|
⊢ ran {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} =
{z ∣
∃x
∈ A
∃y
∈ B
φ} |
|
Theorem | eloprabga 5578* |
The law of concretion for operation class abstraction. Compare
elopab 4696. (Contributed by NM, 14-Sep-1999.) (Revised
by David
Abernethy, 18-Jun-2012.) Removed unnecessary distinct variable
requirements. (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) →
(〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ}
↔ ψ)) |
|
Theorem | eloprabg 5579* |
The law of concretion for operation class abstraction. Compare
elopab 4696. (Contributed by set.mm contributors,
14-Sep-1999.) (Revised
by David Abernethy, 19-Jun-2012.) Removed unnecessary distinct variable
requirements. (Revised by set.mm contributors, 19-Dec-2013.)
|
⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (z =
C → (χ ↔ θ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) →
(〈〈A, B〉, C〉 ∈ {〈〈x, y〉, z〉 ∣ φ}
↔ θ)) |
|
Theorem | ssoprab2i 5580* |
Inference of operation class abstraction subclass from implication.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors,
11-Nov-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
|
⊢ (φ
→ ψ)
⇒ ⊢ {〈〈x, y〉, z〉 ∣ φ} ⊆
{〈〈x, y〉, z〉 ∣ ψ} |
|
Theorem | resoprab 5581* |
Restriction of an operation class abstraction. (Contributed by set.mm
contributors, 10-Feb-2007.)
|
⊢ ({〈〈x, y〉, z〉 ∣ φ}
↾ (A
× B)) = {〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} |
|
Theorem | resoprab2 5582* |
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((C ⊆ A ∧ D ⊆ B) →
({〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ↾ (C ×
D)) = {〈〈x, y〉, z〉 ∣ ((x ∈ C ∧ y ∈ D) ∧ φ)}) |
|
Theorem | funoprabg 5583* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by set.mm contributors,
28-Aug-2007.)
|
⊢ (∀x∀y∃*zφ →
Fun {〈〈x, y〉, z〉 ∣ φ}) |
|
Theorem | funoprab 5584* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by set.mm contributors,
17-Mar-1995.)
|
⊢ ∃*zφ ⇒ ⊢ Fun {〈〈x, y〉, z〉 ∣ φ} |
|
Theorem | fnoprabg 5585* |
Functionality and domain of an operation class abstraction.
(Contributed by set.mm contributors, 28-Aug-2007.)
|
⊢ (∀x∀y(φ →
∃!zψ) →
{〈〈x, y〉, z〉 ∣ (φ
∧ ψ)}
Fn {〈x,
y〉 ∣ φ}) |
|
Theorem | fnoprab 5586* |
Functionality and domain of an operation class abstraction.
(Contributed by set.mm contributors, 15-May-1995.)
|
⊢ (φ
→ ∃!zψ) ⇒ ⊢ {〈〈x, y〉, z〉 ∣ (φ
∧ ψ)}
Fn {〈x,
y〉 ∣ φ} |
|
Theorem | ffnov 5587* |
An operation maps to a class to which all values belong. (Contributed
by set.mm contributors, 7-Feb-2004.)
|
⊢ (F:(A ×
B)–→C ↔ (F Fn
(A × B) ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C)) |
|
Theorem | fovcl 5588 |
Closure law for an operation. (Contributed by set.mm contributors,
19-Apr-2007.)
|
⊢ F:(R × S)–→C ⇒ ⊢ ((A ∈ R ∧ B ∈ S) →
(AFB) ∈ C) |
|
Theorem | eqfnov 5589* |
Equality of two operations is determined by their values. (Contributed
by set.mm contributors, 1-Sep-2005.)
|
⊢ ((F Fn
(A × B) ∧ G Fn (C ×
D)) → (F = G ↔
((A × B) = (C ×
D) ∧
∀x
∈ A
∀y
∈ B
(xFy) = (xGy)))) |
|
Theorem | eqfnov2 5590* |
Two operators with the same domain are equal iff their values at each
point in the domain are equal. (Contributed by Jeff Madsen,
7-Jun-2010.)
|
⊢ ((F Fn
(A × B) ∧ G Fn (A ×
B)) → (F = G ↔
∀x
∈ A
∀y
∈ B
(xFy) = (xGy))) |
|
Theorem | fnov 5591* |
Representation of an operation class abstraction in terms of its values.
(Contributed by set.mm contributors, 7-Feb-2004.)
|
⊢ (F Fn
(A × B) ↔ F =
{〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ z = (xFy))}) |
|
Theorem | fov 5592* |
Representation of an operation class abstraction in terms of its values.
(Contributed by set.mm contributors, 7-Feb-2004.)
|
⊢ (F:(A ×
B)–→C ↔ (F =
{〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ z = (xFy))} ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C)) |
|
Theorem | ovidig 5593* |
The value of an operation class abstraction. Compare ovidi 5594. The
condition (x ∈ R ∧ y ∈ S) is
been removed. (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
⊢ ∃*zφ
& ⊢ F = {〈〈x, y〉, z〉 ∣ φ} ⇒ ⊢ (φ
→ (xFy) = z) |
|
Theorem | ovidi 5594* |
The value of an operation class abstraction (weak version).
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ ((x ∈ R ∧ y ∈ S) →
∃*zφ)
& ⊢ F = {〈〈x, y〉, z〉 ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)} ⇒ ⊢ ((x ∈ R ∧ y ∈ S) →
(φ → (xFy) = z)) |
|
Theorem | ov 5595* |
The value of an operation class abstraction. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19-Jun-2012.)
(Contributed by set.mm contributors, 16-May-1995.) (Revised by set.mm
contributors, 24-Jul-2012.)
|
⊢ C ∈ V
& ⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (z =
C → (χ ↔ θ))
& ⊢ ((x ∈ R ∧ y ∈ S) →
∃!zφ)
& ⊢ F = {〈〈x, y〉, z〉 ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)} ⇒ ⊢ ((A ∈ R ∧ B ∈ S) →
((AFB) = C ↔ θ)) |
|
Theorem | ovigg 5596* |
The value of an operation class abstraction. Compare ovig 5597.
The
condition (x ∈ R ∧ y ∈ S) is
been removed. (Contributed by FL,
24-Mar-2007.)
|
⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ))
& ⊢ ∃*zφ
& ⊢ F = {〈〈x, y〉, z〉 ∣ φ} ⇒ ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) →
(ψ → (AFB) = C)) |
|
Theorem | ovig 5597* |
The value of an operation class abstraction (weak version).
(Contributed by set.mm contributors, 14-Sep-1999.) (Unnecessary
distinct variable restrictions were removed by David Abernethy,
19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B
∧ z =
C) → (φ ↔ ψ))
& ⊢ ((x ∈ R ∧ y ∈ S) →
∃*zφ)
& ⊢ F = {〈〈x, y〉, z〉 ∣ ((x ∈ R ∧ y ∈ S) ∧ φ)} ⇒ ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ D) →
(ψ → (AFB) = C)) |
|
Theorem | ov2ag 5598* |
The value of an operation class abstraction. Special case.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ R = S)
& ⊢ F = {〈〈x, y〉, z〉 ∣ ((x ∈ C ∧ y ∈ D) ∧ z = R)} ⇒ ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) →
(AFB) = S) |
|
Theorem | ov3 5599* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
⊢ S ∈ V
& ⊢ (((w =
A ∧
v = B)
∧ (u =
C ∧
f = D)) → R =
S)
& ⊢ F = {〈〈x, y〉, z〉 ∣ ((x ∈ (H × H)
∧ y ∈ (H ×
H)) ∧
∃w∃v∃u∃f((x = 〈w, v〉 ∧ y = 〈u, f〉) ∧ z = R))} ⇒ ⊢ (((A ∈ H ∧ B ∈ H) ∧ (C ∈ H ∧ D ∈ H)) →
(〈A,
B〉F〈C, D〉) = S) |
|
Theorem | ov6g 5600* |
The value of an operation class abstraction. Special case.
(Contributed by set.mm contributors, 13-Nov-2006.)
|
⊢ (〈x, y〉 = 〈A, B〉 → R =
S)
& ⊢ F = {〈〈x, y〉, z〉 ∣ (〈x, y〉 ∈ C ∧ z = R)} ⇒ ⊢ (((A ∈ G ∧ B ∈ H ∧ 〈A, B〉 ∈ C) ∧ S ∈ J) → (AFB) = S) |