Theorem List for Intuitionistic Logic Explorer - 5801-5900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cbvmpox 5801* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. This version of cbvmpo 5802 allows 𝐵 to be a function of
𝑥. (Contributed by NM, 29-Dec-2014.)
|
⊢ Ⅎ𝑧𝐵
& ⊢ Ⅎ𝑥𝐷
& ⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑤𝐶
& ⊢ Ⅎ𝑥𝐸
& ⊢ Ⅎ𝑦𝐸
& ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐷)
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐷 ↦ 𝐸) |
|
Theorem | cbvmpo 5802* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. (Contributed by NM, 17-Dec-2013.)
|
⊢ Ⅎ𝑧𝐶
& ⊢ Ⅎ𝑤𝐶
& ⊢ Ⅎ𝑥𝐷
& ⊢ Ⅎ𝑦𝐷
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | cbvmpov 5803* |
Rule to change the bound variable in a maps-to function, using implicit
substitution. With a longer proof analogous to cbvmpt 3981, some distinct
variable requirements could be eliminated. (Contributed by NM,
11-Jun-2013.)
|
⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)
& ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | dmoprab 5804* |
The domain of an operation class abstraction. (Contributed by NM,
17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧𝜑} |
|
Theorem | dmoprabss 5805* |
The domain of an operation class abstraction. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵) |
|
Theorem | rnoprab 5806* |
The range of an operation class abstraction. (Contributed by NM,
30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
|
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦𝜑} |
|
Theorem | rnoprab2 5807* |
The range of a restricted operation class abstraction. (Contributed by
Scott Fenton, 21-Mar-2012.)
|
⊢ ran {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑} |
|
Theorem | reldmoprab 5808* |
The domain of an operation class abstraction is a relation.
(Contributed by NM, 17-Mar-1995.)
|
⊢ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | oprabss 5809* |
Structure of an operation class abstraction. (Contributed by NM,
28-Nov-2006.)
|
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ ((V × V) ×
V) |
|
Theorem | eloprabga 5810* |
The law of concretion for operation class abstraction. Compare
elopab 4138. (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.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | eloprabg 5811* |
The law of concretion for operation class abstraction. Compare
elopab 4138. (Contributed by NM, 14-Sep-1999.) (Revised
by David
Abernethy, 19-Jun-2012.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜃)) |
|
Theorem | ssoprab2i 5812* |
Inference of operation class abstraction subclass from implication.
(Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy,
19-Jun-2012.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⊆ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} |
|
Theorem | mpov 5813* |
Operation with universal domain in maps-to notation. (Contributed by
NM, 16-Aug-2013.)
|
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝐶} |
|
Theorem | mpomptx 5814* |
Express a two-argument function as a one-argument function, or
vice-versa. In this version 𝐵(𝑥) is not assumed to be constant
w.r.t 𝑥. (Contributed by Mario Carneiro,
29-Dec-2014.)
|
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | mpompt 5815* |
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.)
|
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | mpodifsnif 5816 |
A mapping with two arguments with the first argument from a difference set
with a singleton and a conditional as result. (Contributed by AV,
13-Feb-2019.)
|
⊢ (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ (𝐴 ∖ {𝑋}), 𝑗 ∈ 𝐵 ↦ 𝐷) |
|
Theorem | mposnif 5817 |
A mapping with two arguments with the first argument from a singleton and
a conditional as result. (Contributed by AV, 14-Feb-2019.)
|
⊢ (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ if(𝑖 = 𝑋, 𝐶, 𝐷)) = (𝑖 ∈ {𝑋}, 𝑗 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | fconstmpo 5818* |
Representation of a constant operation using the mapping operation.
(Contributed by SO, 11-Jul-2018.)
|
⊢ ((𝐴 × 𝐵) × {𝐶}) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | resoprab 5819* |
Restriction of an operation class abstraction. (Contributed by NM,
10-Feb-2007.)
|
⊢ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↾ (𝐴 × 𝐵)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} |
|
Theorem | resoprab2 5820* |
Restriction of an operator abstraction. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ↾ (𝐶 × 𝐷)) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)}) |
|
Theorem | resmpo 5821* |
Restriction of the mapping operation. (Contributed by Mario Carneiro,
17-Dec-2013.)
|
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) ↾ (𝐶 × 𝐷)) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸)) |
|
Theorem | funoprabg 5822* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
|
⊢ (∀𝑥∀𝑦∃*𝑧𝜑 → Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑}) |
|
Theorem | funoprab 5823* |
"At most one" is a sufficient condition for an operation class
abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
|
⊢ ∃*𝑧𝜑 ⇒ ⊢ Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
|
Theorem | fnoprabg 5824* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 28-Aug-2007.)
|
⊢ (∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑}) |
|
Theorem | mpofun 5825* |
The maps-to notation for an operation is always a function.
(Contributed by Scott Fenton, 21-Mar-2012.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Fun 𝐹 |
|
Theorem | fnoprab 5826* |
Functionality and domain of an operation class abstraction.
(Contributed by NM, 15-May-1995.)
|
⊢ (𝜑 → ∃!𝑧𝜓) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑} |
|
Theorem | ffnov 5827* |
An operation maps to a class to which all values belong. (Contributed
by NM, 7-Feb-2004.)
|
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) |
|
Theorem | fovcl 5828 |
Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
|
⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | eqfnov 5829* |
Equality of two operations is determined by their values. (Contributed
by NM, 1-Sep-2005.)
|
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((𝐴 × 𝐵) = (𝐶 × 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦)))) |
|
Theorem | eqfnov2 5830* |
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 (𝐴 × 𝐵) ∧ 𝐺 Fn (𝐴 × 𝐵)) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) = (𝑥𝐺𝑦))) |
|
Theorem | fnovim 5831* |
Representation of a function in terms of its values. (Contributed by
Jim Kingdon, 16-Jan-2019.)
|
⊢ (𝐹 Fn (𝐴 × 𝐵) → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝑥𝐹𝑦))) |
|
Theorem | mpo2eqb 5832* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnov2 5830. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → ((𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 = 𝐷)) |
|
Theorem | rnmpo 5833* |
The range of an operation given by the maps-to notation. (Contributed
by FL, 20-Jun-2011.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = 𝐶} |
|
Theorem | reldmmpo 5834* |
The domain of an operation defined by maps-to notation is a relation.
(Contributed by Stefan O'Rear, 27-Nov-2014.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ Rel dom 𝐹 |
|
Theorem | elrnmpog 5835* |
Membership in the range of an operation class abstraction. (Contributed
by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶)) |
|
Theorem | elrnmpo 5836* |
Membership in the range of an operation class abstraction.
(Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
& ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐷 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐷 = 𝐶) |
|
Theorem | ralrnmpo 5837* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
& ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∀𝑧 ∈ ran 𝐹𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | rexrnmpo 5838* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
& ⊢ (𝑧 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → (∃𝑧 ∈ ran 𝐹𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)) |
|
Theorem | ovid 5839* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = 𝑧 ↔ 𝜑)) |
|
Theorem | ovidig 5840* |
The value of an operation class abstraction. Compare ovidi 5841. The
condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
⊢ ∃*𝑧𝜑
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ (𝜑 → (𝑥𝐹𝑦) = 𝑧) |
|
Theorem | ovidi 5841* |
The value of an operation class abstraction (weak version).
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → (𝜑 → (𝑥𝐹𝑦) = 𝑧)) |
|
Theorem | ov 5842* |
The value of an operation class abstraction. (Contributed by NM,
16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|
⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) |
|
Theorem | ovigg 5843* |
The value of an operation class abstraction. Compare ovig 5844.
The
condition (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) is been removed. (Contributed by
FL,
24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ ∃*𝑧𝜑
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → (𝐴𝐹𝐵) = 𝐶)) |
|
Theorem | ovig 5844* |
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.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃*𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (𝜓 → (𝐴𝐹𝐵) = 𝐶)) |
|
Theorem | ovmpt4g 5845* |
Value of a function given by the maps-to notation. (This is the
operation analog of fvmpt2 5456.) (Contributed by NM, 21-Feb-2004.)
(Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) = 𝐶) |
|
Theorem | ovmpos 5846* |
Value of a function given by the maps-to notation, expressed using
explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅 ∈ 𝑉) → (𝐴𝐹𝐵) = ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝑅) |
|
Theorem | ov2gf 5847* |
The value of an operation class abstraction. A version of ovmpog 5857
using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.)
(Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐺
& ⊢ Ⅎ𝑦𝑆
& ⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)
& ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)
& ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpodxf 5848* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)
& ⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐿)
& ⊢ (𝜑 → 𝑆 ∈ 𝑋)
& ⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑥𝐵
& ⊢ Ⅎ𝑥𝑆
& ⊢ Ⅎ𝑦𝑆 ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpodx 5849* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 29-Dec-2014.)
|
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿)
& ⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐿)
& ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpod 5850* |
Value of an operation given by a maps-to rule, deduction form.
(Contributed by Mario Carneiro, 7-Dec-2014.)
|
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷)
& ⊢ (𝜑 → 𝑆 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpox 5851* |
The value of an operation class abstraction. Variant of ovmpoga 5852 which
does not require 𝐷 and 𝑥 to be distinct.
(Contributed by Jeff
Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
& ⊢ (𝑥 = 𝐴 → 𝐷 = 𝐿)
& ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐿 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpoga 5852* |
Value of an operation given by a maps-to rule. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
& ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpoa 5853* |
Value of an operation given by a maps-to rule. (Contributed by NM,
19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆)
& ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
& ⊢ 𝑆 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpodf 5854* |
Alternate deduction version of ovmpo 5858, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) & ⊢
Ⅎ𝑥𝐹
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝐹
& ⊢ Ⅎ𝑦𝜓 ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
|
Theorem | ovmpodv 5855* |
Alternate deduction version of ovmpo 5858, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
|
Theorem | ovmpodv2 5856* |
Alternate deduction version of ovmpo 5858, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = 𝑆)) |
|
Theorem | ovmpog 5857* |
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.)
|
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)
& ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)
& ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝑆 ∈ 𝐻) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovmpo 5858* |
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.)
|
⊢ (𝑥 = 𝐴 → 𝑅 = 𝐺)
& ⊢ (𝑦 = 𝐵 → 𝐺 = 𝑆)
& ⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)
& ⊢ 𝑆 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovi3 5859* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻)) & ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆) |
|
Theorem | ov6g 5860* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 13-Nov-2006.)
|
⊢ (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑅 = 𝑆)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ 𝐶 ∧ 𝑧 = 𝑅)} ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ 〈𝐴, 𝐵〉 ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovg 5861* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) |
|
Theorem | ovres 5862 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) |
|
Theorem | ovresd 5863 |
Lemma for converting metric theorems to metric space theorems.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑋)
& ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵)) |
|
Theorem | oprssov 5864 |
The value of a member of the domain of a subclass of an operation.
(Contributed by NM, 23-Aug-2007.)
|
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) |
|
Theorem | fovrn 5865 |
An operation's value belongs to its codomain. (Contributed by NM,
27-Aug-2006.)
|
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | fovrnda 5866 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | fovrnd 5867 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑅)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | fnrnov 5868* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by NM, 29-Oct-2006.)
|
⊢ (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)}) |
|
Theorem | foov 5869* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦))) |
|
Theorem | fnovrn 5870 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹) |
|
Theorem | ovelrn 5871* |
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 (𝐴 × 𝐵) → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥𝐹𝑦))) |
|
Theorem | funimassov 5872* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
⊢ ((Fun 𝐹 ∧ (𝐴 × 𝐵) ⊆ dom 𝐹) → ((𝐹 “ (𝐴 × 𝐵)) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) |
|
Theorem | ovelimab 5873* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (𝐷 ∈ (𝐹 “ (𝐵 × 𝐶)) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐷 = (𝑥𝐹𝑦))) |
|
Theorem | ovconst2 5874 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅((𝐴 × 𝐵) × {𝐶})𝑆) = 𝐶) |
|
Theorem | caovclg 5875* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸) |
|
Theorem | caovcld 5876* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)
& ⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐸) |
|
Theorem | caovcl 5877* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) |
|
Theorem | caovcomg 5878* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) |
|
Theorem | caovcomd 5879* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) |
|
Theorem | caovcom 5880* |
Convert an operation commutative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) ⇒ ⊢ (𝐴𝐹𝐵) = (𝐵𝐹𝐴) |
|
Theorem | caovassg 5881* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro,
26-May-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) |
|
Theorem | caovassd 5882* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) |
|
Theorem | caovass 5883* |
Convert an operation associative law to class notation. (Contributed
by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)) |
|
Theorem | caovcang 5884* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | caovcand 5885* |
Convert an operation cancellation law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))
& ⊢ (𝜑 → 𝐴 ∈ 𝑇)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | caovcanrd 5886* |
Commute the arguments of an operation cancellation law. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))
& ⊢ (𝜑 → 𝐴 ∈ 𝑇)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶)) |
|
Theorem | caovcan 5887* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.)
|
⊢ 𝐶 ∈ V & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶)) |
|
Theorem | caovordig 5888* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovordid 5889* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovordg 5890* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovordd 5891* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovord2d 5892* |
Operation ordering law with commuted arguments. (Contributed by Mario
Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) |
|
Theorem | caovord3d 5893* |
Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ (𝜑 → 𝐷 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐶𝐹𝐷) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵))) |
|
Theorem | caovord 5894* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovord2 5895* |
Operation ordering law with commuted arguments. (Contributed by NM,
27-Feb-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) |
|
Theorem | caovord3 5896* |
Ordering law. (Contributed by NM, 29-Feb-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ 𝐷 ∈ V ⇒ ⊢ (((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴𝐹𝐵) = (𝐶𝐹𝐷)) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵)) |
|
Theorem | caovdig 5897* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) |
|
Theorem | caovdid 5898* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝐾)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) |
|
Theorem | caovdir2d 5899* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶))) |
|
Theorem | caovdirg 5900* |
Convert an operation reverse distributive law to class notation.
(Contributed by Mario Carneiro, 19-Oct-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) |