 Home Intuitionistic Logic ExplorerTheorem List (p. 56 of 73) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5501-5600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcbvoprab12 5501* 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⟩ ∣ ψ}

Theoremcbvoprab12v 5502* 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⟩ ∣ ψ}

Theoremcbvoprab3 5503* 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⟩ ∣ ψ}

Theoremcbvoprab3v 5504* 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⟩ ∣ ψ}

Theoremcbvmpt2x 5505* Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5506 allows B to be a function of x. (Contributed by NM, 29-Dec-2014.)
zB    &   x𝐷    &   z𝐶    &   w𝐶    &   x𝐸    &   y𝐸    &   (x = zB = 𝐷)    &   ((x = z y = w) → 𝐶 = 𝐸)       (x A, y B𝐶) = (z A, w 𝐷𝐸)

Theoremcbvmpt2 5506* 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𝐷)

Theoremcbvmpt2v 5507* Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3825, 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𝐷)

Theoremdmoprab 5508* 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φ}

Theoremdmoprabss 5509* The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
dom {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)} ⊆ (A × B)

Theoremrnoprab 5510* The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
ran {⟨⟨x, y⟩, z⟩ ∣ φ} = {zxyφ}

Theoremrnoprab2 5511* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
ran {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)} = {zx A y B φ}

Theoremreldmoprab 5512* The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
Rel dom {⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremoprabss 5513* Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
{⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ ((V × V) × V)

Theoremeloprabga 5514* The law of concretion for operation class abstraction. Compare elopab 3969. (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⟩ ∣ φ} ↔ ψ))

Theoremeloprabg 5515* The law of concretion for operation class abstraction. Compare elopab 3969. (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⟩ ∣ φ} ↔ θ))

Theoremssoprab2i 5516* 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⟩ ∣ ψ}

Theoremmpt2v 5517* Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
(x V, y V ↦ 𝐶) = {⟨⟨x, y⟩, z⟩ ∣ z = 𝐶}

Theoremmpt2mptx 5518* 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𝐷)

Theoremmpt2mpt 5519* 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𝐷)

Theoremresoprab 5520* Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
({⟨⟨x, y⟩, z⟩ ∣ φ} ↾ (A × B)) = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)}

Theoremresoprab2 5521* 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 𝐷) φ)})

Theoremresmpt2 5522* Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
((𝐶A 𝐷B) → ((x A, y B𝐸) ↾ (𝐶 × 𝐷)) = (x 𝐶, y 𝐷𝐸))

Theoremfunoprabg 5523* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
(xy∃*zφ → Fun {⟨⟨x, y⟩, z⟩ ∣ φ})

Theoremfunoprab 5524* "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⟩ ∣ φ}

Theoremfnoprabg 5525* Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
(xy(φ∃!zψ) → {⟨⟨x, y⟩, z⟩ ∣ (φ ψ)} Fn {⟨x, y⟩ ∣ φ})

Theoremmpt2fun 5526* The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
𝐹 = (x A, y B𝐶)       Fun 𝐹

Theoremfnoprab 5527* Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
(φ∃!zψ)       {⟨⟨x, y⟩, z⟩ ∣ (φ ψ)} Fn {⟨x, y⟩ ∣ φ}

Theoremffnov 5528* 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) 𝐶))

Theoremfovcl 5529 Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
𝐹:(𝑅 × 𝑆)⟶𝐶       ((A 𝑅 B 𝑆) → (A𝐹B) 𝐶)

Theoremeqfnov 5530* 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))))

Theoremeqfnov2 5531* 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)))

Theoremfnovim 5532* 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)))

Theoremmpt22eqb 5533* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5531. (Contributed by Mario Carneiro, 4-Jan-2017.)
(x A y B 𝐶 𝑉 → ((x A, y B𝐶) = (x A, y B𝐷) ↔ x A y B 𝐶 = 𝐷))

Theoremrnmpt2 5534* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
𝐹 = (x A, y B𝐶)       ran 𝐹 = {zx A y B z = 𝐶}

Theoremreldmmpt2 5535* 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 𝐹

Theoremelrnmpt2g 5536* 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 𝐷 = 𝐶))

Theoremelrnmpt2 5537* 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 𝐷 = 𝐶)

Theoremralrnmpt2 5538* 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 ψ))

Theoremrexrnmpt2 5539* 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 ψ))

Theoremovid 5540* 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φ))

Theoremovidig 5541* The value of an operation class abstraction. Compare ovidi 5542. The condition (x 𝑅 y 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
∃*zφ    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}       (φ → (x𝐹y) = z)

Theoremovidi 5542* 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))

Theoremov 5543* 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) = 𝐶θ))

Theoremovigg 5544* The value of an operation class abstraction. Compare ovig 5545. 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) = 𝐶))

Theoremovig 5545* 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) = 𝐶))

Theoremovmpt4g 5546* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5179.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
𝐹 = (x A, y B𝐶)       ((x A y B 𝐶 𝑉) → (x𝐹y) = 𝐶)

Theoremovmpt2s 5547* 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 / xB / y𝑅 𝑉) → (A𝐹B) = A / xB / y𝑅)

Theoremov2gf 5548* The value of an operation class abstraction. A version of ovmpt2g 5558 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) = 𝑆)

Theoremovmpt2dxf 5549* 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) = 𝑆)

Theoremovmpt2dx 5550* 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) = 𝑆)

Theoremovmpt2d 5551* 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) = 𝑆)

Theoremovmpt2x 5552* The value of an operation class abstraction. Variant of ovmpt2ga 5553 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) = 𝑆)

Theoremovmpt2ga 5553* 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) = 𝑆)

Theoremovmpt2a 5554* 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) = 𝑆)

Theoremovmpt2df 5555* Alternate deduction version of ovmpt2 5559, 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 𝐷𝑅) → ψ))

Theoremovmpt2dv 5556* Alternate deduction version of ovmpt2 5559, 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 𝐷𝑅) → ψ))

Theoremovmpt2dv2 5557* Alternate deduction version of ovmpt2 5559, 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) = 𝑆))

Theoremovmpt2g 5558* 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) = 𝑆)

Theoremovmpt2 5559* 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) = 𝑆)

Theoremovi3 5560* 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 (𝐻 × 𝐻)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = 𝑅))}       (((A 𝐻 B 𝐻) (𝐶 𝐻 𝐷 𝐻)) → (⟨A, B𝐹𝐶, 𝐷⟩) = 𝑆)

Theoremov6g 5561* 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) = 𝑆)

Theoremovg 5562* 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) = 𝐶θ))

Theoremovres 5563 The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
((A 𝐶 B 𝐷) → (A(𝐹 ↾ (𝐶 × 𝐷))B) = (A𝐹B))

Theoremovresd 5564 Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
(φA 𝑋)    &   (φB 𝑋)       (φ → (A(𝐷 ↾ (𝑋 × 𝑋))B) = (A𝐷B))

Theoremoprssov 5565 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))

Theoremfovrn 5566 An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
((𝐹:(𝑅 × 𝑆)⟶𝐶 A 𝑅 B 𝑆) → (A𝐹B) 𝐶)

Theoremfovrnda 5567 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(φ𝐹:(𝑅 × 𝑆)⟶𝐶)       ((φ (A 𝑅 B 𝑆)) → (A𝐹B) 𝐶)

Theoremfovrnd 5568 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(φ𝐹:(𝑅 × 𝑆)⟶𝐶)    &   (φA 𝑅)    &   (φB 𝑆)       (φ → (A𝐹B) 𝐶)

Theoremfnrnov 5569* The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
(𝐹 Fn (A × B) → ran 𝐹 = {zx A y B z = (x𝐹y)})

Theoremfoov 5570* 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)))

Theoremfnovrn 5571 An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
((𝐹 Fn (A × B) 𝐶 A 𝐷 B) → (𝐶𝐹𝐷) ran 𝐹)

Theoremovelrn 5572* 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)))

Theoremfunimassov 5573* 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) 𝐶))

Theoremovelimab 5574* 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)))

Theoremovconst2 5575 The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
𝐶 V       ((𝑅 A 𝑆 B) → (𝑅((A × B) × {𝐶})𝑆) = 𝐶)

Theoremcaovclg 5576* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
((φ (x 𝐶 y 𝐷)) → (x𝐹y) 𝐸)       ((φ (A 𝐶 B 𝐷)) → (A𝐹B) 𝐸)

Theoremcaovcld 5577* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝐶 y 𝐷)) → (x𝐹y) 𝐸)    &   (φA 𝐶)    &   (φB 𝐷)       (φ → (A𝐹B) 𝐸)

Theoremcaovcl 5578* 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) 𝑆)

Theoremcaovcomg 5579* 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))

Theoremcaovcomd 5580* 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))

Theoremcaovcom 5581* 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)

Theoremcaovassg 5582* Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))       ((φ (A 𝑆 B 𝑆 𝐶 𝑆)) → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶)))

Theoremcaovassd 5583* Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)       (φ → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶)))

Theoremcaovass 5584* Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
A V    &   B V    &   𝐶 V    &   ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))       ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶))

Theoremcaovcang 5585* Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑇 y 𝑆 z 𝑆)) → ((x𝐹y) = (x𝐹z) ↔ y = z))       ((φ (A 𝑇 B 𝑆 𝐶 𝑆)) → ((A𝐹B) = (A𝐹𝐶) ↔ B = 𝐶))

Theoremcaovcand 5586* Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑇 y 𝑆 z 𝑆)) → ((x𝐹y) = (x𝐹z) ↔ y = z))    &   (φA 𝑇)    &   (φB 𝑆)    &   (φ𝐶 𝑆)       (φ → ((A𝐹B) = (A𝐹𝐶) ↔ B = 𝐶))

Theoremcaovcanrd 5587* Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑇 y 𝑆 z 𝑆)) → ((x𝐹y) = (x𝐹z) ↔ y = z))    &   (φA 𝑇)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   (φA 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))       (φ → ((B𝐹A) = (𝐶𝐹A) ↔ B = 𝐶))

Theoremcaovcan 5588* Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)
𝐶 V    &   ((x 𝑆 y 𝑆) → ((x𝐹y) = (x𝐹z) → y = z))       ((A 𝑆 B 𝑆) → ((A𝐹B) = (A𝐹𝐶) → B = 𝐶))

Theoremcaovordig 5589* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y → (z𝐹x)𝑅(z𝐹y)))       ((φ (A 𝑆 B 𝑆 𝐶 𝑆)) → (A𝑅B → (𝐶𝐹A)𝑅(𝐶𝐹B)))

Theoremcaovordid 5590* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y → (z𝐹x)𝑅(z𝐹y)))    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)       (φ → (A𝑅B → (𝐶𝐹A)𝑅(𝐶𝐹B)))

Theoremcaovordg 5591* Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))       ((φ (A 𝑆 B 𝑆 𝐶 𝑆)) → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))

Theoremcaovordd 5592* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)       (φ → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))

Theoremcaovord2d 5593* Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))       (φ → (A𝑅B ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))

Theoremcaovord3d 5594* Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   (φ𝐷 𝑆)       (φ → ((A𝐹B) = (𝐶𝐹𝐷) → (A𝑅𝐶𝐷𝑅B)))

Theoremcaovord 5595* Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)
A V    &   B V    &   (z 𝑆 → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))       (𝐶 𝑆 → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))

Theoremcaovord2 5596* Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)
A V    &   B V    &   (z 𝑆 → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   𝐶 V    &   (x𝐹y) = (y𝐹x)       (𝐶 𝑆 → (A𝑅B ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))

Theoremcaovord3 5597* Ordering law. (Contributed by NM, 29-Feb-1996.)
A V    &   B V    &   (z 𝑆 → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))    &   𝐶 V    &   (x𝐹y) = (y𝐹x)    &   𝐷 V       (((B 𝑆 𝐶 𝑆) (A𝐹B) = (𝐶𝐹𝐷)) → (A𝑅𝐶𝐷𝑅B))

Theoremcaovdig 5598* Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
((φ (x 𝐾 y 𝑆 z 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐻(x𝐺z)))       ((φ (A 𝐾 B 𝑆 𝐶 𝑆)) → (A𝐺(B𝐹𝐶)) = ((A𝐺B)𝐻(A𝐺𝐶)))

Theoremcaovdid 5599* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝐾 y 𝑆 z 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐻(x𝐺z)))    &   (φA 𝐾)    &   (φB 𝑆)    &   (φ𝐶 𝑆)       (φ → (A𝐺(B𝐹𝐶)) = ((A𝐺B)𝐻(A𝐺𝐶)))

Theoremcaovdir2d 5600* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐹(x𝐺z)))    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐺y) = (y𝐺x))       (φ → ((A𝐹B)𝐺𝐶) = ((A𝐺𝐶)𝐹(B𝐺𝐶)))

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-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7215
 Copyright terms: Public domain < Previous  Next >