Theorem List for Intuitionistic Logic Explorer - 5501-5600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | oprabbidv 5501* |
Equivalent wff's yield equal operation class abstractions (deduction
rule). (Contributed by NM, 21-Feb-2004.)
|
⊢ (φ
→ (ψ ↔ χ)) ⇒ ⊢ (φ → {〈〈x, y〉,
z〉 ∣ ψ} = {〈〈x, y〉,
z〉 ∣ χ}) |
|
Theorem | oprabbii 5502* |
Equivalent wff's yield equal operation class abstractions. (Contributed
by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ (φ
↔ ψ)
⇒ ⊢ {〈〈x, y〉,
z〉 ∣ φ} = {〈〈x, y〉,
z〉 ∣ ψ} |
|
Theorem | ssoprab2 5503 |
Equivalence of ordered pair abstraction subclass and implication.
Compare ssopab2 4003. (Contributed by FL, 6-Nov-2013.) (Proof
shortened
by Mario Carneiro, 11-Dec-2016.)
|
⊢ (∀x∀y∀z(φ →
ψ) → {〈〈x, y〉,
z〉 ∣ φ} ⊆ {〈〈x, y〉,
z〉 ∣ ψ}) |
|
Theorem | ssoprab2b 5504 |
Equivalence of ordered pair abstraction subclass and implication. Compare
ssopab2b 4004. (Contributed by FL, 6-Nov-2013.) (Proof
shortened by Mario
Carneiro, 11-Dec-2016.)
|
⊢ ({〈〈x, y〉,
z〉 ∣ φ} ⊆ {〈〈x, y〉,
z〉 ∣ ψ} ↔ ∀x∀y∀z(φ → ψ)) |
|
Theorem | eqoprab2b 5505 |
Equivalence of ordered pair abstraction subclass and biconditional.
Compare eqopab2b 4007. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ({〈〈x, y〉,
z〉 ∣ φ} = {〈〈x, y〉,
z〉 ∣ ψ} ↔ ∀x∀y∀z(φ ↔ ψ)) |
|
Theorem | mpt2eq123 5506* |
An equality theorem for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
|
⊢ ((A = 𝐷 ∧ ∀x ∈ A (B = 𝐸 ∧ ∀y ∈ B 𝐶 = 𝐹)) → (x ∈ A, y ∈ B ↦
𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹)) |
|
Theorem | mpt2eq12 5507* |
An equality theorem for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ ((A = 𝐶 ∧ B = 𝐷) → (x ∈ A, y ∈ B ↦
𝐸) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝐸)) |
|
Theorem | mpt2eq123dva 5508* |
An equality deduction for the maps to notation. (Contributed by Mario
Carneiro, 26-Jan-2017.)
|
⊢ (φ
→ A = 𝐷)
& ⊢ ((φ
∧ x ∈ A) →
B = 𝐸)
& ⊢ ((φ
∧ (x
∈ A
∧ y ∈ B)) →
𝐶 = 𝐹) ⇒ ⊢ (φ → (x ∈ A, y ∈ B ↦
𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹)) |
|
Theorem | mpt2eq123dv 5509* |
An equality deduction for the maps to notation. (Contributed by NM,
12-Sep-2011.)
|
⊢ (φ
→ A = 𝐷)
& ⊢ (φ
→ B = 𝐸)
& ⊢ (φ
→ 𝐶 = 𝐹)
⇒ ⊢ (φ → (x ∈ A, y ∈ B ↦
𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹)) |
|
Theorem | mpt2eq123i 5510 |
An equality inference for the maps to notation. (Contributed by NM,
15-Jul-2013.)
|
⊢ A = 𝐷 & ⊢ B = 𝐸
& ⊢ 𝐶 = 𝐹 ⇒ ⊢ (x ∈ A, y ∈ B ↦
𝐶) = (x ∈ 𝐷, y ∈ 𝐸 ↦ 𝐹) |
|
Theorem | mpt2eq3dva 5511* |
Slightly more general equality inference for the maps to notation.
(Contributed by NM, 17-Oct-2013.)
|
⊢ ((φ
∧ x ∈ A ∧ y ∈ B) →
𝐶 = 𝐷) ⇒ ⊢ (φ → (x ∈ A, y ∈ B ↦
𝐶) = (x ∈ A, y ∈ B ↦
𝐷)) |
|
Theorem | mpt2eq3ia 5512 |
An equality inference for the maps to notation. (Contributed by Mario
Carneiro, 16-Dec-2013.)
|
⊢ ((x ∈ A ∧ y ∈ B) →
𝐶 = 𝐷) ⇒ ⊢ (x ∈ A, y ∈ B ↦
𝐶) = (x ∈ A, y ∈ B ↦
𝐷) |
|
Theorem | nfmpt21 5513 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
⊢ Ⅎx(x ∈ A, y ∈ B ↦ 𝐶) |
|
Theorem | nfmpt22 5514 |
Bound-variable hypothesis builder for an operation in maps-to notation.
(Contributed by NM, 27-Aug-2013.)
|
⊢ Ⅎy(x ∈ A, y ∈ B ↦ 𝐶) |
|
Theorem | nfmpt2 5515* |
Bound-variable hypothesis builder for the maps-to notation.
(Contributed by NM, 20-Feb-2013.)
|
⊢ ℲzA & ⊢
ℲzB
& ⊢ Ⅎz𝐶 ⇒ ⊢ Ⅎz(x ∈ A, y ∈ B ↦ 𝐶) |
|
Theorem | mpt20 5516 |
A mapping operation with empty domain. (Contributed by Stefan O'Rear,
29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
|
⊢ (x ∈ ∅, y
∈ B
↦ 𝐶) =
∅ |
|
Theorem | oprab4 5517* |
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 5518* |
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 5519* |
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 5520* |
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 5521* |
Rule used to change first two bound variables in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.)
|
⊢ ((x =
w ∧
y = v)
→ (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉,
z〉 ∣ φ} = {〈〈w, v〉,
z〉 ∣ ψ} |
|
Theorem | cbvoprab3 5522* |
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 5523* |
Rule used to change the third bound variable in an operation
abstraction, using implicit substitution. (Contributed by NM,
8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ (z =
w → (φ ↔ ψ)) ⇒ ⊢ {〈〈x, y〉,
z〉 ∣ φ} = {〈〈x, y〉,
w〉 ∣ ψ} |
|
Theorem | cbvmpt2x 5524* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version of cbvmpt2 5525 allows B to be a function
of x.
(Contributed by NM, 29-Dec-2014.)
|
⊢ ℲzB & ⊢
Ⅎx𝐷
& ⊢ Ⅎz𝐶
& ⊢ Ⅎw𝐶
& ⊢ Ⅎx𝐸
& ⊢ Ⅎy𝐸
& ⊢ (x =
z → B = 𝐷)
& ⊢ ((x =
z ∧
y = w)
→ 𝐶 = 𝐸)
⇒ ⊢ (x ∈ A, y ∈ B ↦
𝐶) = (z ∈ A, w ∈ 𝐷 ↦ 𝐸) |
|
Theorem | cbvmpt2 5525* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by NM, 17-Dec-2013.)
|
⊢ Ⅎz𝐶
& ⊢ Ⅎw𝐶
& ⊢ Ⅎx𝐷
& ⊢ Ⅎy𝐷
& ⊢ ((x =
z ∧
y = w)
→ 𝐶 = 𝐷)
⇒ ⊢ (x ∈ A, y ∈ B ↦
𝐶) = (z ∈ A, w ∈ B ↦
𝐷) |
|
Theorem | cbvmpt2v 5526* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. With a longer proof analogous to cbvmpt 3842, some distinct
variable requirements could be eliminated. (Contributed by NM,
11-Jun-2013.)
|
⊢ (x =
z → 𝐶 = 𝐸)
& ⊢ (y =
w → 𝐸 = 𝐷) ⇒ ⊢ (x ∈ A, y ∈ B ↦
𝐶) = (z ∈ A, w ∈ B ↦
𝐷) |
|
Theorem | dmoprab 5527* |
The domain of an operation class abstraction. (Contributed by NM,
17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ dom {〈〈x, y〉,
z〉 ∣ φ} = {〈x, y〉
∣ ∃zφ} |
|
Theorem | dmoprabss 5528* |
The domain of an operation class abstraction. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom {〈〈x, y〉,
z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A × B) |
|
Theorem | rnoprab 5529* |
The range of an operation class abstraction. (Contributed by NM,
30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|
⊢ ran {〈〈x, y〉,
z〉 ∣ φ} = {z
∣ ∃x∃yφ} |
|
Theorem | rnoprab2 5530* |
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 | reldmoprab 5531* |
The domain of an operation class abstraction is a relation.
(Contributed by NM, 17-Mar-1995.)
|
⊢ Rel dom {〈〈x, y〉,
z〉 ∣ φ} |
|
Theorem | oprabss 5532* |
Structure of an operation class abstraction. (Contributed by NM,
28-Nov-2006.)
|
⊢ {〈〈x, y〉,
z〉 ∣ φ} ⊆ ((V × V) ×
V) |
|
Theorem | eloprabga 5533* |
The law of concretion for operation class abstraction. Compare
elopab 3986. (Contributed by NM, 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 =
𝐶) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈A, B〉,
𝐶〉 ∈ {〈〈x, y〉,
z〉 ∣ φ} ↔ ψ)) |
|
Theorem | eloprabg 5534* |
The law of concretion for operation class abstraction. Compare
elopab 3986. (Contributed by NM, 14-Sep-1999.) (Revised
by David
Abernethy, 19-Jun-2012.)
|
⊢ (x =
A → (φ ↔ ψ)) & ⊢ (y = B →
(ψ ↔ χ)) & ⊢ (z = 𝐶 → (χ ↔ θ)) ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈A, B〉,
𝐶〉 ∈ {〈〈x, y〉,
z〉 ∣ φ} ↔ θ)) |
|
Theorem | ssoprab2i 5535* |
Inference of operation class abstraction subclass from implication.
(Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ (φ
→ ψ)
⇒ ⊢ {〈〈x, y〉,
z〉 ∣ φ} ⊆ {〈〈x, y〉,
z〉 ∣ ψ} |
|
Theorem | mpt2v 5536* |
Operation with universal domain in maps-to notation. (Contributed by
NM, 16-Aug-2013.)
|
⊢ (x ∈ V, y ∈ V ↦ 𝐶) = {〈〈x, y〉,
z〉 ∣ z = 𝐶} |
|
Theorem | mpt2mptx 5537* |
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〉 → 𝐶 = 𝐷) ⇒ ⊢ (z ∈ ∪ x ∈ A ({x} × B)
↦ 𝐶) = (x ∈ A, y ∈ B ↦
𝐷) |
|
Theorem | mpt2mpt 5538* |
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〉 → 𝐶 = 𝐷) ⇒ ⊢ (z ∈ (A × B)
↦ 𝐶) = (x ∈ A, y ∈ B ↦
𝐷) |
|
Theorem | resoprab 5539* |
Restriction of an operation class abstraction. (Contributed by NM,
10-Feb-2007.)
|
⊢ ({〈〈x, y〉,
z〉 ∣ φ} ↾ (A × B)) =
{〈〈x, y〉, z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} |
|
Theorem | resoprab2 5540* |
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ({〈〈x, y〉,
z〉 ∣ ((x ∈ A ∧ y ∈ B) ∧ φ)} ↾ (𝐶 × 𝐷)) = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)}) |
|
Theorem | resmpt2 5541* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
17-Dec-2013.)
|
⊢ ((𝐶 ⊆ A ∧ 𝐷 ⊆ B) → ((x
∈ A,
y ∈
B ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝐸)) |
|
Theorem | funoprabg 5542* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
|
⊢ (∀x∀y∃*zφ →
Fun {〈〈x, y〉, z〉 ∣ φ}) |
|
Theorem | funoprab 5543* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
|
⊢ ∃*zφ ⇒ ⊢ Fun {〈〈x, y〉,
z〉 ∣ φ} |
|
Theorem | fnoprabg 5544* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 28-Aug-2007.)
|
⊢ (∀x∀y(φ →
∃!zψ) →
{〈〈x, y〉, z〉 ∣ (φ ∧ ψ)} Fn {〈x, y〉
∣ φ}) |
|
Theorem | mpt2fun 5545* |
The maps-to notation for an operation is always a function.
(Contributed by Scott Fenton, 21-Mar-2012.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶) ⇒ ⊢ Fun 𝐹 |
|
Theorem | fnoprab 5546* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 15-May-1995.)
|
⊢ (φ
→ ∃!zψ) ⇒ ⊢ {〈〈x, y〉,
z〉 ∣ (φ ∧ ψ)} Fn {〈x, y〉
∣ φ} |
|
Theorem | ffnov 5547* |
An operation maps to a class to which all values belong. (Contributed
by NM, 7-Feb-2004.)
|
⊢ (𝐹:(A
× B)⟶𝐶 ↔ (𝐹 Fn (A
× B) ∧ ∀x ∈ A ∀y ∈ B (x𝐹y) ∈ 𝐶)) |
|
Theorem | fovcl 5548 |
Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
|
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆) → (A𝐹B)
∈ 𝐶) |
|
Theorem | eqfnov 5549* |
Equality of two operations is determined by their values. (Contributed
by NM, 1-Sep-2005.)
|
⊢ ((𝐹 Fn (A
× B) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((A × B) =
(𝐶 × 𝐷) ∧ ∀x ∈ A ∀y ∈ B (x𝐹y) = (x𝐺y)))) |
|
Theorem | eqfnov2 5550* |
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.)
|
⊢ ((𝐹 Fn (A
× B) ∧ 𝐺 Fn (A
× B)) → (𝐹 = 𝐺 ↔ ∀x ∈ A ∀y ∈ B (x𝐹y) =
(x𝐺y))) |
|
Theorem | fnovim 5551* |
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 16-Jan-2019.)
|
⊢ (𝐹 Fn (A
× B) → 𝐹 = (x
∈ A,
y ∈
B ↦ (x𝐹y))) |
|
Theorem | mpt22eqb 5552* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnov2 5550. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → ((x ∈ A, y ∈ B ↦
𝐶) = (x ∈ A, y ∈ B ↦
𝐷) ↔ ∀x ∈ A ∀y ∈ B 𝐶 = 𝐷)) |
|
Theorem | rnmpt2 5553* |
The range of an operation given by the "maps to" notation.
(Contributed
by FL, 20-Jun-2011.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶) ⇒ ⊢ ran 𝐹 = {z
∣ ∃x ∈ A ∃y ∈ B z = 𝐶} |
|
Theorem | reldmmpt2 5554* |
The domain of an operation defined by maps-to notation is a relation.
(Contributed by Stefan O'Rear, 27-Nov-2014.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶) ⇒ ⊢ Rel dom 𝐹 |
|
Theorem | elrnmpt2g 5555* |
Membership in the range of an operation class abstraction. (Contributed
by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran
𝐹 ↔ ∃x ∈ A ∃y ∈ B 𝐷 = 𝐶)) |
|
Theorem | elrnmpt2 5556* |
Membership in the range of an operation class abstraction.
(Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶)
& ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐷 ∈ ran
𝐹 ↔ ∃x ∈ A ∃y ∈ B 𝐷 = 𝐶) |
|
Theorem | ralrnmpt2 5557* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶)
& ⊢ (z = 𝐶 → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∀z ∈ ran 𝐹φ
↔ ∀x ∈ A ∀y ∈ B ψ)) |
|
Theorem | rexrnmpt2 5558* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶)
& ⊢ (z = 𝐶 → (φ ↔ ψ)) ⇒ ⊢ (∀x ∈ A ∀y ∈ B 𝐶 ∈ 𝑉 → (∃z ∈ ran 𝐹φ
↔ ∃x ∈ A ∃y ∈ B ψ)) |
|
Theorem | ovid 5559* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ ((x ∈ 𝑅 ∧
y ∈
𝑆) → ∃!zφ)
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ⇒ ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ((x𝐹y) =
z ↔ φ)) |
|
Theorem | ovidig 5560* |
The value of an operation class abstraction. Compare ovidi 5561. The
condition (x ∈ 𝑅 ∧ y ∈ 𝑆) is been removed.
(Contributed by
Mario Carneiro, 29-Dec-2014.)
|
⊢ ∃*zφ
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ φ} ⇒ ⊢ (φ → (x𝐹y) =
z) |
|
Theorem | ovidi 5561* |
The value of an operation class abstraction (weak version).
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ ((x ∈ 𝑅 ∧
y ∈
𝑆) → ∃*zφ)
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ⇒ ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → (φ → (x𝐹y) =
z)) |
|
Theorem | ov 5562* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ 𝐶 ∈
V
& ⊢ (x =
A → (φ ↔ ψ)) & ⊢ (y = B →
(ψ ↔ χ)) & ⊢ (z = 𝐶 → (χ ↔ θ)) & ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃!zφ)
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ⇒ ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆) → ((A𝐹B) =
𝐶 ↔ θ)) |
|
Theorem | ovigg 5563* |
The value of an operation class abstraction. Compare ovig 5564.
The
condition (x ∈ 𝑅 ∧ y ∈ 𝑆) is been removed.
(Contributed by FL,
24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B
∧ z =
𝐶) → (φ ↔ ψ)) & ⊢ ∃*zφ
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ φ} ⇒ ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (ψ → (A𝐹B) =
𝐶)) |
|
Theorem | ovig 5564* |
The value of an operation class abstraction (weak version).
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by
Mario Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B
∧ z =
𝐶) → (φ ↔ ψ)) & ⊢ ((x ∈ 𝑅 ∧ y ∈ 𝑆) → ∃*zφ)
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ⇒ ⊢ ((A ∈ 𝑅 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (ψ → (A𝐹B) =
𝐶)) |
|
Theorem | ovmpt4g 5565* |
Value of a function given by the "maps to" notation. (This is the
operation analog of fvmpt2 5197.) (Contributed by NM, 21-Feb-2004.)
(Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (x
∈ A,
y ∈
B ↦ 𝐶) ⇒ ⊢ ((x ∈ A ∧ y ∈ B ∧ 𝐶 ∈ 𝑉) → (x𝐹y) =
𝐶) |
|
Theorem | ovmpt2s 5566* |
Value of a function given by the "maps to" notation, expressed using
explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|
⊢ 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧
⦋A / x⦌⦋B / y⦌𝑅 ∈ 𝑉) → (A𝐹B) =
⦋A / x⦌⦋B / y⦌𝑅) |
|
Theorem | ov2gf 5567* |
The value of an operation class abstraction. A version of ovmpt2g 5577
using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ℲxA & ⊢
ℲyA
& ⊢ ℲyB & ⊢
Ⅎx𝐺
& ⊢ Ⅎy𝑆
& ⊢ (x =
A → 𝑅 = 𝐺)
& ⊢ (y =
B → 𝐺 = 𝑆)
& ⊢ 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2dxf 5568* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ (φ
→ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 = 𝑆)
& ⊢ ((φ
∧ x =
A) → 𝐷 = 𝐿)
& ⊢ (φ
→ A ∈ 𝐶)
& ⊢ (φ
→ B ∈ 𝐿)
& ⊢ (φ
→ 𝑆 ∈ 𝑋)
& ⊢ Ⅎxφ
& ⊢ Ⅎyφ
& ⊢ ℲyA & ⊢
ℲxB
& ⊢ Ⅎx𝑆
& ⊢ Ⅎy𝑆 ⇒ ⊢ (φ → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2dx 5569* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ (φ
→ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 = 𝑆)
& ⊢ ((φ
∧ x =
A) → 𝐷 = 𝐿)
& ⊢ (φ
→ A ∈ 𝐶)
& ⊢ (φ
→ B ∈ 𝐿)
& ⊢ (φ
→ 𝑆 ∈ 𝑋) ⇒ ⊢ (φ → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2d 5570* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 7-Dec-2014.)
|
⊢ (φ
→ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 = 𝑆)
& ⊢ (φ
→ A ∈ 𝐶)
& ⊢ (φ
→ B ∈ 𝐷)
& ⊢ (φ
→ 𝑆 ∈ 𝑋) ⇒ ⊢ (φ → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2x 5571* |
The value of an operation class abstraction. Variant of ovmpt2ga 5572
which does not require 𝐷 and x to be distinct. (Contributed by
Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ 𝑅 = 𝑆) & ⊢ (x = A →
𝐷 = 𝐿)
& ⊢ 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2ga 5572* |
Value of an operation given by a maps-to rule. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ 𝑅 = 𝑆) & ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2a 5573* |
Value of an operation given by a maps-to rule. (Contributed by NM,
19-Dec-2013.)
|
⊢ ((x =
A ∧
y = B)
→ 𝑅 = 𝑆) & ⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
& ⊢ 𝑆 ∈
V ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2df 5574* |
Alternate deduction version of ovmpt2 5578, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝐶)
& ⊢ ((φ
∧ x =
A) → B ∈ 𝐷) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 ∈ 𝑉) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → ((A𝐹B) =
𝑅 → ψ)) & ⊢
Ⅎx𝐹
& ⊢ Ⅎxψ
& ⊢ Ⅎy𝐹
& ⊢ Ⅎyψ ⇒ ⊢ (φ → (𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → ψ)) |
|
Theorem | ovmpt2dv 5575* |
Alternate deduction version of ovmpt2 5578, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝐶)
& ⊢ ((φ
∧ x =
A) → B ∈ 𝐷) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 ∈ 𝑉) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → ((A𝐹B) =
𝑅 → ψ)) ⇒ ⊢ (φ → (𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → ψ)) |
|
Theorem | ovmpt2dv2 5576* |
Alternate deduction version of ovmpt2 5578, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝐶)
& ⊢ ((φ
∧ x =
A) → B ∈ 𝐷) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 ∈ 𝑉) & ⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 = 𝑆) ⇒ ⊢ (φ → (𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → (A𝐹B) =
𝑆)) |
|
Theorem | ovmpt2g 5577* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ (x =
A → 𝑅 = 𝐺)
& ⊢ (y =
B → 𝐺 = 𝑆)
& ⊢ 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (A𝐹B) =
𝑆) |
|
Theorem | ovmpt2 5578* |
Value of an operation given by a maps-to rule. Special case.
(Contributed by NM, 16-May-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ (x =
A → 𝑅 = 𝐺)
& ⊢ (y =
B → 𝐺 = 𝑆)
& ⊢ 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)
& ⊢ 𝑆 ∈
V ⇒ ⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → (A𝐹B) =
𝑆) |
|
Theorem | ovi3 5579* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
⊢ (((A ∈ 𝐻 ∧
B ∈
𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻)) & ⊢ (((w = A ∧ v = B) ∧ (u = 𝐶 ∧
f = 𝐷)) → 𝑅 = 𝑆)
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ (𝐻 × 𝐻) ∧
y ∈
(𝐻 × 𝐻)) ∧ ∃w∃v∃u∃f((x =
〈w, v〉 ∧ y = 〈u,
f〉) ∧ z = 𝑅))}
⇒ ⊢ (((A ∈ 𝐻 ∧ B ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈A, B〉𝐹〈𝐶, 𝐷〉) = 𝑆) |
|
Theorem | ov6g 5580* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 13-Nov-2006.)
|
⊢ (〈x,
y〉 = 〈A, B〉
→ 𝑅 = 𝑆) & ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ (〈x, y〉
∈ 𝐶 ∧
z = 𝑅)} ⇒ ⊢ (((A ∈ 𝐺 ∧ B ∈ 𝐻 ∧
〈A, B〉 ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (A𝐹B) =
𝑆) |
|
Theorem | ovg 5581* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
⊢ (x =
A → (φ ↔ ψ)) & ⊢ (y = B →
(ψ ↔ χ)) & ⊢ (z = 𝐶 → (χ ↔ θ)) & ⊢ ((τ ∧
(x ∈
𝑅 ∧ y ∈ 𝑆)) → ∃!zφ)
& ⊢ 𝐹 = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝑅 ∧ y ∈ 𝑆) ∧ φ)} ⇒ ⊢ ((τ ∧
(A ∈
𝑅 ∧ B ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((A𝐹B) =
𝐶 ↔ θ)) |
|
Theorem | ovres 5582 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
⊢ ((A ∈ 𝐶 ∧
B ∈
𝐷) → (A(𝐹 ↾ (𝐶 × 𝐷))B) =
(A𝐹B)) |
|
Theorem | ovresd 5583 |
Lemma for converting metric theorems to metric space theorems.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ (φ
→ A ∈ 𝑋)
& ⊢ (φ
→ B ∈ 𝑋) ⇒ ⊢ (φ → (A(𝐷 ↾ (𝑋 × 𝑋))B) =
(A𝐷B)) |
|
Theorem | oprssov 5584 |
The value of a member of the domain of a subclass of an operation.
(Contributed by NM, 23-Aug-2007.)
|
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧
(A ∈
𝐶 ∧ B ∈ 𝐷)) → (A𝐹B) =
(A𝐺B)) |
|
Theorem | fovrn 5585 |
An operation's value belongs to its codomain. (Contributed by NM,
27-Aug-2006.)
|
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧
A ∈
𝑅 ∧ B ∈ 𝑆) → (A𝐹B)
∈ 𝐶) |
|
Theorem | fovrnda 5586 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (φ
→ 𝐹:(𝑅 × 𝑆)⟶𝐶) ⇒ ⊢ ((φ ∧
(A ∈
𝑅 ∧ B ∈ 𝑆)) → (A𝐹B)
∈ 𝐶) |
|
Theorem | fovrnd 5587 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (φ
→ 𝐹:(𝑅 × 𝑆)⟶𝐶)
& ⊢ (φ
→ A ∈ 𝑅)
& ⊢ (φ
→ B ∈ 𝑆) ⇒ ⊢ (φ → (A𝐹B)
∈ 𝐶) |
|
Theorem | fnrnov 5588* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by NM, 29-Oct-2006.)
|
⊢ (𝐹 Fn (A
× B) → ran 𝐹 = {z
∣ ∃x ∈ A ∃y ∈ B z = (x𝐹y)}) |
|
Theorem | foov 5589* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
⊢ (𝐹:(A
× B)–onto→𝐶 ↔ (𝐹:(A
× B)⟶𝐶 ∧ ∀z ∈ 𝐶 ∃x ∈ A ∃y ∈ B z = (x𝐹y))) |
|
Theorem | fnovrn 5590 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
⊢ ((𝐹 Fn (A
× B) ∧ 𝐶 ∈
A ∧ 𝐷 ∈ B) →
(𝐶𝐹𝐷) ∈ ran
𝐹) |
|
Theorem | ovelrn 5591* |
A member of an operation's range is a value of the operation.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
30-Jan-2014.)
|
⊢ (𝐹 Fn (A
× B) → (𝐶 ∈ ran
𝐹 ↔ ∃x ∈ A ∃y ∈ B 𝐶 = (x𝐹y))) |
|
Theorem | funimassov 5592* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
⊢ ((Fun 𝐹 ∧
(A × B) ⊆ dom 𝐹) → ((𝐹 “ (A × B))
⊆ 𝐶 ↔ ∀x ∈ A ∀y ∈ B (x𝐹y)
∈ 𝐶)) |
|
Theorem | ovelimab 5593* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
⊢ ((𝐹 Fn A
∧ (B
× 𝐶) ⊆
A) → (𝐷 ∈ (𝐹 “ (B × 𝐶)) ↔ ∃x ∈ B ∃y ∈ 𝐶 𝐷 = (x𝐹y))) |
|
Theorem | ovconst2 5594 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
⊢ 𝐶 ∈
V ⇒ ⊢ ((𝑅 ∈
A ∧ 𝑆 ∈ B) →
(𝑅((A × B)
× {𝐶})𝑆) = 𝐶) |
|
Theorem | caovclg 5595* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
⊢ ((φ
∧ (x
∈ 𝐶 ∧
y ∈
𝐷)) → (x𝐹y)
∈ 𝐸) ⇒ ⊢ ((φ ∧
(A ∈
𝐶 ∧ B ∈ 𝐷)) → (A𝐹B)
∈ 𝐸) |
|
Theorem | caovcld 5596* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
⊢ ((φ
∧ (x
∈ 𝐶 ∧
y ∈
𝐷)) → (x𝐹y)
∈ 𝐸)
& ⊢ (φ
→ A ∈ 𝐶)
& ⊢ (φ
→ B ∈ 𝐷) ⇒ ⊢ (φ → (A𝐹B)
∈ 𝐸) |
|
Theorem | caovcl 5597* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
⊢ ((x ∈ 𝑆 ∧
y ∈
𝑆) → (x𝐹y)
∈ 𝑆) ⇒ ⊢ ((A ∈ 𝑆 ∧ B ∈ 𝑆) → (A𝐹B)
∈ 𝑆) |
|
Theorem | caovcomg 5598* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
⊢ ((φ
∧ (x
∈ 𝑆 ∧
y ∈
𝑆)) → (x𝐹y) =
(y𝐹x)) ⇒ ⊢ ((φ ∧
(A ∈
𝑆 ∧ B ∈ 𝑆)) → (A𝐹B) =
(B𝐹A)) |
|
Theorem | caovcomd 5599* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((φ
∧ (x
∈ 𝑆 ∧
y ∈
𝑆)) → (x𝐹y) =
(y𝐹x))
& ⊢ (φ
→ A ∈ 𝑆)
& ⊢ (φ
→ B ∈ 𝑆) ⇒ ⊢ (φ → (A𝐹B) =
(B𝐹A)) |
|
Theorem | caovcom 5600* |
Convert an operation commutative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ (x𝐹y) = (y𝐹x) ⇒ ⊢ (A𝐹B) =
(B𝐹A) |