Home Intuitionistic Logic ExplorerTheorem List (p. 57 of 75) < 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 - 5601-5700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcaov12d 5601* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))       (φ → (A𝐹(B𝐹𝐶)) = (B𝐹(A𝐹𝐶)))

Theoremcaov31d 5602* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))       (φ → ((A𝐹B)𝐹𝐶) = ((𝐶𝐹B)𝐹A))

Theoremcaov13d 5603* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))       (φ → (A𝐹(B𝐹𝐶)) = (𝐶𝐹(B𝐹A)))

Theoremcaov4d 5604* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   (φ𝐷 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)       (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((A𝐹𝐶)𝐹(B𝐹𝐷)))

Theoremcaov411d 5605* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   (φ𝐷 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)       (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹B)𝐹(A𝐹𝐷)))

Theoremcaov42d 5606* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   (φ𝐷 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)       (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((A𝐹𝐶)𝐹(𝐷𝐹B)))

Theoremcaov32 5607* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
A V    &   B V    &   𝐶 V    &   (x𝐹y) = (y𝐹x)    &   ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))       ((A𝐹B)𝐹𝐶) = ((A𝐹𝐶)𝐹B)

Theoremcaov12 5608* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
A V    &   B V    &   𝐶 V    &   (x𝐹y) = (y𝐹x)    &   ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))       (A𝐹(B𝐹𝐶)) = (B𝐹(A𝐹𝐶))

Theoremcaov31 5609* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
A V    &   B V    &   𝐶 V    &   (x𝐹y) = (y𝐹x)    &   ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))       ((A𝐹B)𝐹𝐶) = ((𝐶𝐹B)𝐹A)

Theoremcaov13 5610* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
A V    &   B V    &   𝐶 V    &   (x𝐹y) = (y𝐹x)    &   ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))       (A𝐹(B𝐹𝐶)) = (𝐶𝐹(B𝐹A))

Theoremcaovdilemd 5611* Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)
((φ (x 𝑆 y 𝑆)) → (x𝐺y) = (y𝐺x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐺y) 𝑆)    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   (φ𝐷 𝑆)    &   (φ𝐻 𝑆)       (φ → (((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻) = ((A𝐺(𝐶𝐺𝐻))𝐹(B𝐺(𝐷𝐺𝐻))))

Theoremcaovlem2d 5612* Rearrangement of expression involving multiplication (𝐺) and addition (𝐹). (Contributed by Jim Kingdon, 3-Jan-2020.)
((φ (x 𝑆 y 𝑆)) → (x𝐺y) = (y𝐺x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐺y) 𝑆)    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   (φ𝐷 𝑆)    &   (φ𝐻 𝑆)    &   (φ𝑅 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)       (φ → ((((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻)𝐹(((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅)) = ((A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))))

Theoremcaovimo 5613* Uniqueness of inverse element in commutative, associative operation with identity. The identity element is B. (Contributed by Jim Kingdon, 18-Sep-2019.)
B 𝑆    &   ((x 𝑆 y 𝑆) → (x𝐹y) = (y𝐹x))    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   (x 𝑆 → (x𝐹B) = x)       (A 𝑆∃*w(w 𝑆 (A𝐹w) = B))

Theoremgrprinvlem 5614* Lemma for grprinvd 5615. (Contributed by NM, 9-Aug-2013.)
((φ x B y B) → (x + y) B)    &   (φ𝑂 B)    &   ((φ x B) → (𝑂 + x) = x)    &   ((φ (x B y B z B)) → ((x + y) + z) = (x + (y + z)))    &   ((φ x B) → y B (y + x) = 𝑂)    &   ((φ ψ) → 𝑋 B)    &   ((φ ψ) → (𝑋 + 𝑋) = 𝑋)       ((φ ψ) → 𝑋 = 𝑂)

Theoremgrprinvd 5615* Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
((φ x B y B) → (x + y) B)    &   (φ𝑂 B)    &   ((φ x B) → (𝑂 + x) = x)    &   ((φ (x B y B z B)) → ((x + y) + z) = (x + (y + z)))    &   ((φ x B) → y B (y + x) = 𝑂)    &   ((φ ψ) → 𝑋 B)    &   ((φ ψ) → 𝑁 B)    &   ((φ ψ) → (𝑁 + 𝑋) = 𝑂)       ((φ ψ) → (𝑋 + 𝑁) = 𝑂)

Theoremgrpridd 5616* Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
((φ x B y B) → (x + y) B)    &   (φ𝑂 B)    &   ((φ x B) → (𝑂 + x) = x)    &   ((φ (x B y B z B)) → ((x + y) + z) = (x + (y + z)))    &   ((φ x B) → y B (y + x) = 𝑂)       ((φ x B) → (x + 𝑂) = x)

2.6.11  "Maps to" notation

Theoremelmpt2cl 5617* If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (x A, y B𝐶)       (𝑋 (𝑆𝐹𝑇) → (𝑆 A 𝑇 B))

Theoremelmpt2cl1 5618* If a two-parameter class is not empty, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (x A, y B𝐶)       (𝑋 (𝑆𝐹𝑇) → 𝑆 A)

Theoremelmpt2cl2 5619* If a two-parameter class is not empty, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (x A, y B𝐶)       (𝑋 (𝑆𝐹𝑇) → 𝑇 B)

Theoremelovmpt2 5620* Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.)
𝐷 = (𝑎 A, 𝑏 B𝐶)    &   𝐶 V    &   ((𝑎 = 𝑋 𝑏 = 𝑌) → 𝐶 = 𝐸)       (𝐹 (𝑋𝐷𝑌) ↔ (𝑋 A 𝑌 B 𝐹 𝐸))

Theoremf1ocnvd 5621* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (x A𝐶)    &   ((φ x A) → 𝐶 𝑊)    &   ((φ y B) → 𝐷 𝑋)    &   (φ → ((x A y = 𝐶) ↔ (y B x = 𝐷)))       (φ → (𝐹:A1-1-ontoB 𝐹 = (y B𝐷)))

Theoremf1od 5622* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
𝐹 = (x A𝐶)    &   ((φ x A) → 𝐶 𝑊)    &   ((φ y B) → 𝐷 𝑋)    &   (φ → ((x A y = 𝐶) ↔ (y B x = 𝐷)))       (φ𝐹:A1-1-ontoB)

Theoremf1ocnv2d 5623* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (x A𝐶)    &   ((φ x A) → 𝐶 B)    &   ((φ y B) → 𝐷 A)    &   ((φ (x A y B)) → (x = 𝐷y = 𝐶))       (φ → (𝐹:A1-1-ontoB 𝐹 = (y B𝐷)))

Theoremf1o2d 5624* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
𝐹 = (x A𝐶)    &   ((φ x A) → 𝐶 B)    &   ((φ y B) → 𝐷 A)    &   ((φ (x A y B)) → (x = 𝐷y = 𝐶))       (φ𝐹:A1-1-ontoB)

Theoremf1opw2 5625* A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 5626 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.)
(φ𝐹:A1-1-ontoB)    &   (φ → (𝐹𝑎) V)    &   (φ → (𝐹𝑏) V)       (φ → (𝑏 𝒫 A ↦ (𝐹𝑏)):𝒫 A1-1-onto→𝒫 B)

Theoremf1opw 5626* A one-to-one mapping induces a one-to-one mapping on power sets. (Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario Carneiro, 26-Jun-2015.)
(𝐹:A1-1-ontoB → (𝑏 𝒫 A ↦ (𝐹𝑏)):𝒫 A1-1-onto→𝒫 B)

Theoremsuppssfv 5627* Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(φ → ((x 𝐷A) “ (V ∖ {𝑌})) ⊆ 𝐿)    &   (φ → (𝐹𝑌) = 𝑍)    &   ((φ x 𝐷) → A 𝑉)       (φ → ((x 𝐷 ↦ (𝐹A)) “ (V ∖ {𝑍})) ⊆ 𝐿)

Theoremsuppssov1 5628* Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(φ → ((x 𝐷A) “ (V ∖ {𝑌})) ⊆ 𝐿)    &   ((φ v 𝑅) → (𝑌𝑂v) = 𝑍)    &   ((φ x 𝐷) → A 𝑉)    &   ((φ x 𝐷) → B 𝑅)       (φ → ((x 𝐷 ↦ (A𝑂B)) “ (V ∖ {𝑍})) ⊆ 𝐿)

2.6.12  Function operation

Syntaxcof 5629 Extend class notation to include mapping of an operation to a function operation.
class 𝑓 𝑅

Syntaxcofr 5630 Extend class notation to include mapping of a binary relation to a function relation.
class 𝑟 𝑅

Definitiondf-of 5631* Define the function operation map. The definition is designed so that if 𝑅 is a binary operation, then 𝑓 𝑅 is the analogous operation on functions which corresponds to applying 𝑅 pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
𝑓 𝑅 = (f V, g V ↦ (x (dom f ∩ dom g) ↦ ((fx)𝑅(gx))))

Definitiondf-ofr 5632* Define the function relation map. The definition is designed so that if 𝑅 is a binary relation, then 𝑓 𝑅 is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014.)
𝑟 𝑅 = {⟨f, g⟩ ∣ x (dom f ∩ dom g)(fx)𝑅(gx)}

Theoremofeq 5633 Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝑅 = 𝑆 → ∘𝑓 𝑅 = ∘𝑓 𝑆)

Theoremofreq 5634 Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝑅 = 𝑆 → ∘𝑟 𝑅 = ∘𝑟 𝑆)

Theoremofexg 5635 A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.)
(A 𝑉 → ( ∘𝑓 𝑅A) V)

Theoremnfof 5636* Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
x𝑅       x𝑓 𝑅

Theoremnfofr 5637* Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
x𝑅       x𝑟 𝑅

Theoremoffval 5638* Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn B)    &   (φA 𝑉)    &   (φB 𝑊)    &   (AB) = 𝑆    &   ((φ x A) → (𝐹x) = 𝐶)    &   ((φ x B) → (𝐺x) = 𝐷)       (φ → (𝐹𝑓 𝑅𝐺) = (x 𝑆 ↦ (𝐶𝑅𝐷)))

Theoremofrfval 5639* Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn B)    &   (φA 𝑉)    &   (φB 𝑊)    &   (AB) = 𝑆    &   ((φ x A) → (𝐹x) = 𝐶)    &   ((φ x B) → (𝐺x) = 𝐷)       (φ → (𝐹𝑟 𝑅𝐺x 𝑆 𝐶𝑅𝐷))

Theoremfnofval 5640 Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn B)    &   (φA 𝑉)    &   (φB 𝑊)    &   (AB) = 𝑆    &   ((φ 𝑋 A) → (𝐹𝑋) = 𝐶)    &   ((φ 𝑋 B) → (𝐺𝑋) = 𝐷)    &   (φ𝑅 Fn (𝑈 × 𝑉))    &   (φ𝐶 𝑈)    &   (φ𝐷 𝑉)       ((φ 𝑋 𝑆) → ((𝐹𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))

Theoremofrval 5641 Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn B)    &   (φA 𝑉)    &   (φB 𝑊)    &   (AB) = 𝑆    &   ((φ 𝑋 A) → (𝐹𝑋) = 𝐶)    &   ((φ 𝑋 B) → (𝐺𝑋) = 𝐷)       ((φ 𝐹𝑟 𝑅𝐺 𝑋 𝑆) → 𝐶𝑅𝐷)

Theoremofmresval 5642 Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
(φ𝐹 A)    &   (φ𝐺 B)       (φ → (𝐹( ∘𝑓 𝑅 ↾ (A × B))𝐺) = (𝐹𝑓 𝑅𝐺))

Theoremoff 5643* The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
((φ (x 𝑆 y 𝑇)) → (x𝑅y) 𝑈)    &   (φ𝐹:A𝑆)    &   (φ𝐺:B𝑇)    &   (φA 𝑉)    &   (φB 𝑊)    &   (AB) = 𝐶       (φ → (𝐹𝑓 𝑅𝐺):𝐶𝑈)

Theoremofres 5644 Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn B)    &   (φA 𝑉)    &   (φB 𝑊)    &   (AB) = 𝐶       (φ → (𝐹𝑓 𝑅𝐺) = ((𝐹𝐶) ∘𝑓 𝑅(𝐺𝐶)))

Theoremoffval2 5645* The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
(φA 𝑉)    &   ((φ x A) → B 𝑊)    &   ((φ x A) → 𝐶 𝑋)    &   (φ𝐹 = (x AB))    &   (φ𝐺 = (x A𝐶))       (φ → (𝐹𝑓 𝑅𝐺) = (x A ↦ (B𝑅𝐶)))

Theoremofrfval2 5646* The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
(φA 𝑉)    &   ((φ x A) → B 𝑊)    &   ((φ x A) → 𝐶 𝑋)    &   (φ𝐹 = (x AB))    &   (φ𝐺 = (x A𝐶))       (φ → (𝐹𝑟 𝑅𝐺x A B𝑅𝐶))

Theoremsuppssof1 5647* Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(φ → (A “ (V ∖ {𝑌})) ⊆ 𝐿)    &   ((φ v 𝑅) → (𝑌𝑂v) = 𝑍)    &   (φA:𝐷𝑉)    &   (φB:𝐷𝑅)    &   (φ𝐷 𝑊)       (φ → ((A𝑓 𝑂B) “ (V ∖ {𝑍})) ⊆ 𝐿)

Theoremofco 5648 The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.)
(φ𝐹 Fn A)    &   (φ𝐺 Fn B)    &   (φ𝐻:𝐷𝐶)    &   (φA 𝑉)    &   (φB 𝑊)    &   (φ𝐷 𝑋)    &   (AB) = 𝐶       (φ → ((𝐹𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹𝐻) ∘𝑓 𝑅(𝐺𝐻)))

Theoremoffveqb 5649* Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
(φA 𝑉)    &   (φ𝐹 Fn A)    &   (φ𝐺 Fn A)    &   (φ𝐻 Fn A)    &   ((φ x A) → (𝐹x) = B)    &   ((φ x A) → (𝐺x) = 𝐶)       (φ → (𝐻 = (𝐹𝑓 𝑅𝐺) ↔ x A (𝐻x) = (B𝑅𝐶)))

Theoremofc12 5650 Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
(φA 𝑉)    &   (φB 𝑊)    &   (φ𝐶 𝑋)       (φ → ((A × {B}) ∘𝑓 𝑅(A × {𝐶})) = (A × {(B𝑅𝐶)}))

Theoremcaofref 5651* Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(φA 𝑉)    &   (φ𝐹:A𝑆)    &   ((φ x 𝑆) → x𝑅x)       (φ𝐹𝑟 𝑅𝐹)

Theoremcaofinvl 5652* Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.)
(φA 𝑉)    &   (φ𝐹:A𝑆)    &   (φB 𝑊)    &   (φ𝑁:𝑆𝑆)    &   (φ𝐺 = (v A ↦ (𝑁‘(𝐹v))))    &   ((φ x 𝑆) → ((𝑁x)𝑅x) = B)       (φ → (𝐺𝑓 𝑅𝐹) = (A × {B}))

Theoremcaofcom 5653* Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
(φA 𝑉)    &   (φ𝐹:A𝑆)    &   (φ𝐺:A𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝑅y) = (y𝑅x))       (φ → (𝐹𝑓 𝑅𝐺) = (𝐺𝑓 𝑅𝐹))

Theoremcaofrss 5654* Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(φA 𝑉)    &   (φ𝐹:A𝑆)    &   (φ𝐺:A𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝑅yx𝑇y))       (φ → (𝐹𝑟 𝑅𝐺𝐹𝑟 𝑇𝐺))

Theoremcaoftrn 5655* Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(φA 𝑉)    &   (φ𝐹:A𝑆)    &   (φ𝐺:A𝑆)    &   (φ𝐻:A𝑆)    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝑅y y𝑇z) → x𝑈z))       (φ → ((𝐹𝑟 𝑅𝐺 𝐺𝑟 𝑇𝐻) → 𝐹𝑟 𝑈𝐻))

2.6.13  Functions (continued)

TheoremresfunexgALT 5656 The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. This version has a shorter proof than resfunexg 5303 but requires ax-pow 3897 and ax-un 4116. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
((Fun A B 𝐶) → (AB) V)

Theoremcofunexg 5657 Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
((Fun A B 𝐶) → (AB) V)

Theoremcofunex2g 5658 Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
((A 𝑉 Fun B) → (AB) V)

TheoremfnexALT 5659 If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 4905. This version of fnex 5304 uses ax-pow 3897 and ax-un 4116, whereas fnex 5304 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐹 Fn A A B) → 𝐹 V)

Theoremfunrnex 5660 If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 5305. (Contributed by NM, 11-Nov-1995.)
(dom 𝐹 B → (Fun 𝐹 → ran 𝐹 V))

Theoremfornex 5661 If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
(A 𝐶 → (𝐹:AontoBB V))

Theoremf1dmex 5662 If the codomain of a one-to-one function exists, so does its domain. This can be thought of as a form of the Axiom of Replacement. (Contributed by NM, 4-Sep-2004.)
((𝐹:A1-1B B 𝐶) → A V)

Theoremabrexex 5663* Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in the class expression substituted for B, which can be thought of as B(x). This simple-looking theorem is actually quite powerful and appears to involve the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path mptexg 5307, funex 5305, fnex 5304, resfunexg 5303, and funimaexg 4905. See also abrexex2 5670. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
A V       {yx A y = B} V

Theoremabrexexg 5664* Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. The antecedent assures us that A is a set. (Contributed by NM, 3-Nov-2003.)
(A 𝑉 → {yx A y = B} V)

Theoremiunexg 5665* The existence of an indexed union. x is normally a free-variable parameter in B. (Contributed by NM, 23-Mar-2006.)
((A 𝑉 x A B 𝑊) → x A B V)

Theoremabrexex2g 5666* Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
((A 𝑉 x A {yφ} 𝑊) → {yx A φ} V)

Theoremopabex3d 5667* Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.)
(φA V)    &   ((φ x A) → {yψ} V)       (φ → {⟨x, y⟩ ∣ (x A ψ)} V)

Theoremopabex3 5668* Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
A V    &   (x A → {yφ} V)       {⟨x, y⟩ ∣ (x A φ)} V

Theoremiunex 5669* The existence of an indexed union. x is normally a free-variable parameter in the class expression substituted for B, which can be read informally as B(x). (Contributed by NM, 13-Oct-2003.)
A V    &   B V        x A B V

Theoremabrexex2 5670* Existence of an existentially restricted class abstraction. φ is normally has free-variable parameters x and y. See also abrexex 5663. (Contributed by NM, 12-Sep-2004.)
A V    &   {yφ} V       {yx A φ} V

Theoremabexssex 5671* Existence of a class abstraction with an existentially quantified expression. Both x and y can be free in φ. (Contributed by NM, 29-Jul-2006.)
A V    &   {yφ} V       {yx(xA φ)} V

Theoremabexex 5672* A condition where a class builder continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.)
A V    &   (φx A)    &   {yφ} V       {yxφ} V

Theoremoprabexd 5673* Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
(φA V)    &   (φB V)    &   ((φ (x A y B)) → ∃*zψ)    &   (φ𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) ψ)})       (φ𝐹 V)

Theoremoprabex 5674* Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
A V    &   B V    &   ((x A y B) → ∃*zφ)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)}       𝐹 V

Theoremoprabex3 5675* Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
𝐻 V    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x (𝐻 × 𝐻) y (𝐻 × 𝐻)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = 𝑅))}       𝐹 V

Theoremoprabrexex2 5676* Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
A V    &   {⟨⟨x, y⟩, z⟩ ∣ φ} V       {⟨⟨x, y⟩, z⟩ ∣ w A φ} V

Theoremab2rexex 5677* Existence of a class abstraction of existentially restricted sets. Variables x and y are normally free-variable parameters in the class expression substituted for 𝐶, which can be thought of as 𝐶(x, y). See comments for abrexex 5663. (Contributed by NM, 20-Sep-2011.)
A V    &   B V       {zx A y B z = 𝐶} V

Theoremab2rexex2 5678* Existence of an existentially restricted class abstraction. φ normally has free-variable parameters x, y, and z. Compare abrexex2 5670. (Contributed by NM, 20-Sep-2011.)
A V    &   B V    &   {zφ} V       {zx A y B φ} V

TheoremxpexgALT 5679 The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4375 for a version that uses the Power Set axiom instead. (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
((A 𝑉 B 𝑊) → (A × B) V)

Theoremoffval3 5680* General value of (𝐹𝑓 𝑅𝐺) with no assumptions on functionality of 𝐹 and 𝐺. (Contributed by Stefan O'Rear, 24-Jan-2015.)
((𝐹 𝑉 𝐺 𝑊) → (𝐹𝑓 𝑅𝐺) = (x (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹x)𝑅(𝐺x))))

Theoremoffres 5681 Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
((𝐹 𝑉 𝐺 𝑊) → ((𝐹𝑓 𝑅𝐺) ↾ 𝐷) = ((𝐹𝐷) ∘𝑓 𝑅(𝐺𝐷)))

Theoremofmres 5682* Equivalent expressions for a restriction of the function operation map. Unlike 𝑓 𝑅 which is a proper class, ( ∘𝑓 𝑅 ∣ ‘(A × B)) can be a set by ofmresex 5683, allowing it to be used as a function or structure argument. By ofmresval 5642, the restricted operation map values are the same as the original values, allowing theorems for 𝑓 𝑅 to be reused. (Contributed by NM, 20-Oct-2014.)
( ∘𝑓 𝑅 ↾ (A × B)) = (f A, g B ↦ (f𝑓 𝑅g))

Theoremofmresex 5683 Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
(φA 𝑉)    &   (φB 𝑊)       (φ → ( ∘𝑓 𝑅 ↾ (A × B)) V)

2.6.14  First and second members of an ordered pair

Syntaxc1st 5684 Extend the definition of a class to include the first member an ordered pair function.
class 1st

Syntaxc2nd 5685 Extend the definition of a class to include the second member an ordered pair function.
class 2nd

Definitiondf-1st 5686 Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 5692 proves that it does this. For example, (1st ‘⟨ 3 , 4 ) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 4725 and op1stb 4155). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
1st = (x V ↦ dom {x})

Definitiondf-2nd 5687 Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 5693 proves that it does this. For example, (2nd ‘⟨ 3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 4728 and op2ndb 4727). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
2nd = (x V ↦ ran {x})

Theorem1stvalg 5688 The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
(A V → (1stA) = dom {A})

Theorem2ndvalg 5689 The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
(A V → (2ndA) = ran {A})

Theorem1st0 5690 The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
(1st ‘∅) = ∅

Theorem2nd0 5691 The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
(2nd ‘∅) = ∅

Theoremop1st 5692 Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
A V    &   B V       (1st ‘⟨A, B⟩) = A

Theoremop2nd 5693 Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
A V    &   B V       (2nd ‘⟨A, B⟩) = B

Theoremop1std 5694 Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
A V    &   B V       (𝐶 = ⟨A, B⟩ → (1st𝐶) = A)

Theoremop2ndd 5695 Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
A V    &   B V       (𝐶 = ⟨A, B⟩ → (2nd𝐶) = B)

Theoremop1stg 5696 Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
((A 𝑉 B 𝑊) → (1st ‘⟨A, B⟩) = A)

Theoremop2ndg 5697 Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
((A 𝑉 B 𝑊) → (2nd ‘⟨A, B⟩) = B)

Theoremot1stg 5698 Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 5698, ot2ndg 5699, ot3rdgg 5700.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
((A 𝑉 B 𝑊 𝐶 𝑋) → (1st ‘(1st ‘⟨A, B, 𝐶⟩)) = A)

Theoremot2ndg 5699 Extract the second member of an ordered triple. (See ot1stg 5698 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
((A 𝑉 B 𝑊 𝐶 𝑋) → (2nd ‘(1st ‘⟨A, B, 𝐶⟩)) = B)

Theoremot3rdgg 5700 Extract the third member of an ordered triple. (See ot1stg 5698 comment.) (Contributed by NM, 3-Apr-2015.)
((A 𝑉 B 𝑊 𝐶 𝑋) → (2nd ‘⟨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-7300 74 7301-7400 75 7401-7411
 Copyright terms: Public domain < Previous  Next >