HomeHome Intuitionistic Logic Explorer
Theorem List (p. 60 of 135)
< 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 - 5901-6000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremovmpodx 5901* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
(𝜑𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐿)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐿)    &   (𝜑𝑆𝑋)       (𝜑 → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovmpod 5902* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
(𝜑𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐷)    &   (𝜑𝑆𝑋)       (𝜑 → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovmpox 5903* The value of an operation class abstraction. Variant of ovmpoga 5904 which does not require 𝐷 and 𝑥 to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)    &   (𝑥 = 𝐴𝐷 = 𝐿)    &   𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)       ((𝐴𝐶𝐵𝐿𝑆𝐻) → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovmpoga 5904* Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)    &   𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)       ((𝐴𝐶𝐵𝐷𝑆𝐻) → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovmpoa 5905* Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵) → 𝑅 = 𝑆)    &   𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)    &   𝑆 ∈ V       ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovmpodf 5906* Alternate deduction version of ovmpo 5910, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(𝜑𝐴𝐶)    &   ((𝜑𝑥 = 𝐴) → 𝐵𝐷)    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅𝑉)    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅𝜓))    &   𝑥𝐹    &   𝑥𝜓    &   𝑦𝐹    &   𝑦𝜓       (𝜑 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓))
 
Theoremovmpodv 5907* Alternate deduction version of ovmpo 5910, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(𝜑𝐴𝐶)    &   ((𝜑𝑥 = 𝐴) → 𝐵𝐷)    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅𝑉)    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅𝜓))       (𝜑 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → 𝜓))
 
Theoremovmpodv2 5908* Alternate deduction version of ovmpo 5910, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(𝜑𝐴𝐶)    &   ((𝜑𝑥 = 𝐴) → 𝐵𝐷)    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅𝑉)    &   ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)       (𝜑 → (𝐹 = (𝑥𝐶, 𝑦𝐷𝑅) → (𝐴𝐹𝐵) = 𝑆))
 
Theoremovmpog 5909* 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.)
(𝑥 = 𝐴𝑅 = 𝐺)    &   (𝑦 = 𝐵𝐺 = 𝑆)    &   𝐹 = (𝑥𝐶, 𝑦𝐷𝑅)       ((𝐴𝐶𝐵𝐷𝑆𝐻) → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovmpo 5910* 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       ((𝐴𝐶𝐵𝐷) → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovi3 5911* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
(((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → 𝑆 ∈ (𝐻 × 𝐻))    &   (((𝑤 = 𝐴𝑣 = 𝐵) ∧ (𝑢 = 𝐶𝑓 = 𝐷)) → 𝑅 = 𝑆)    &   𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = 𝑅))}       (((𝐴𝐻𝐵𝐻) ∧ (𝐶𝐻𝐷𝐻)) → (⟨𝐴, 𝐵𝐹𝐶, 𝐷⟩) = 𝑆)
 
Theoremov6g 5912* The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
(⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → 𝑅 = 𝑆)    &   𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ 𝐶𝑧 = 𝑅)}       (((𝐴𝐺𝐵𝐻 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝐶) ∧ 𝑆𝐽) → (𝐴𝐹𝐵) = 𝑆)
 
Theoremovg 5913* The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))    &   (𝑧 = 𝐶 → (𝜒𝜃))    &   ((𝜏 ∧ (𝑥𝑅𝑦𝑆)) → ∃!𝑧𝜑)    &   𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝑅𝑦𝑆) ∧ 𝜑)}       ((𝜏 ∧ (𝐴𝑅𝐵𝑆𝐶𝐷)) → ((𝐴𝐹𝐵) = 𝐶𝜃))
 
Theoremovres 5914 The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
((𝐴𝐶𝐵𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))
 
Theoremovresd 5915 Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
(𝜑𝐴𝑋)    &   (𝜑𝐵𝑋)       (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
 
Theoremoprssov 5916 The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
(((Fun 𝐹𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺𝐹) ∧ (𝐴𝐶𝐵𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
 
Theoremfovrn 5917 An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
((𝐹:(𝑅 × 𝑆)⟶𝐶𝐴𝑅𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝐶)
 
Theoremfovrnda 5918 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(𝜑𝐹:(𝑅 × 𝑆)⟶𝐶)       ((𝜑 ∧ (𝐴𝑅𝐵𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶)
 
Theoremfovrnd 5919 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(𝜑𝐹:(𝑅 × 𝑆)⟶𝐶)    &   (𝜑𝐴𝑅)    &   (𝜑𝐵𝑆)       (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶)
 
Theoremfnrnov 5920* The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
(𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥𝐴𝑦𝐵 𝑧 = (𝑥𝐹𝑦)})
 
Theoremfoov 5921* An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
(𝐹:(𝐴 × 𝐵)–onto𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧𝐶𝑥𝐴𝑦𝐵 𝑧 = (𝑥𝐹𝑦)))
 
Theoremfnovrn 5922 An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶𝐴𝐷𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹)
 
Theoremovelrn 5923* 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 𝐹 ↔ ∃𝑥𝐴𝑦𝐵 𝐶 = (𝑥𝐹𝑦)))
 
Theoremfunimassov 5924* Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
((Fun 𝐹 ∧ (𝐴 × 𝐵) ⊆ dom 𝐹) → ((𝐹 “ (𝐴 × 𝐵)) ⊆ 𝐶 ↔ ∀𝑥𝐴𝑦𝐵 (𝑥𝐹𝑦) ∈ 𝐶))
 
Theoremovelimab 5925* Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (𝐷 ∈ (𝐹 “ (𝐵 × 𝐶)) ↔ ∃𝑥𝐵𝑦𝐶 𝐷 = (𝑥𝐹𝑦)))
 
Theoremovconst2 5926 The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
𝐶 ∈ V       ((𝑅𝐴𝑆𝐵) → (𝑅((𝐴 × 𝐵) × {𝐶})𝑆) = 𝐶)
 
Theoremcaovclg 5927* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
((𝜑 ∧ (𝑥𝐶𝑦𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)       ((𝜑 ∧ (𝐴𝐶𝐵𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸)
 
Theoremcaovcld 5928* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝐶𝑦𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)    &   (𝜑𝐴𝐶)    &   (𝜑𝐵𝐷)       (𝜑 → (𝐴𝐹𝐵) ∈ 𝐸)
 
Theoremcaovcl 5929* Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
((𝑥𝑆𝑦𝑆) → (𝑥𝐹𝑦) ∈ 𝑆)       ((𝐴𝑆𝐵𝑆) → (𝐴𝐹𝐵) ∈ 𝑆)
 
Theoremcaovcomg 5930* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))       ((𝜑 ∧ (𝐴𝑆𝐵𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
 
Theoremcaovcomd 5931* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)       (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴))
 
Theoremcaovcom 5932* Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)       (𝐴𝐹𝐵) = (𝐵𝐹𝐴)
 
Theoremcaovassg 5933* Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       ((𝜑 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))
 
Theoremcaovassd 5934* Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))
 
Theoremcaovass 5935* Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
 
Theoremcaovcang 5936* Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑇𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))       ((𝜑 ∧ (𝐴𝑇𝐵𝑆𝐶𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶))
 
Theoremcaovcand 5937* Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑇𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))    &   (𝜑𝐴𝑇)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶))
 
Theoremcaovcanrd 5938* Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑇𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))    &   (𝜑𝐴𝑇)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   (𝜑𝐴𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))       (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶))
 
Theoremcaovcan 5939* Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)
𝐶 ∈ V    &   ((𝑥𝑆𝑦𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧))       ((𝐴𝑆𝐵𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶))
 
Theoremcaovordig 5940* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))       ((𝜑 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
 
Theoremcaovordid 5941* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
 
Theoremcaovordg 5942* Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))       ((𝜑 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
 
Theoremcaovordd 5943* Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
 
Theoremcaovord2d 5944* Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))       (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
 
Theoremcaovord3d 5945* Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   (𝜑𝐷𝑆)       (𝜑 → ((𝐴𝐹𝐵) = (𝐶𝐹𝐷) → (𝐴𝑅𝐶𝐷𝑅𝐵)))
 
Theoremcaovord 5946* Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑧𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))       (𝐶𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
 
Theoremcaovord2 5947* Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑧𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)       (𝐶𝑆 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
 
Theoremcaovord3 5948* Ordering law. (Contributed by NM, 29-Feb-1996.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑧𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   𝐷 ∈ V       (((𝐵𝑆𝐶𝑆) ∧ (𝐴𝐹𝐵) = (𝐶𝐹𝐷)) → (𝐴𝑅𝐶𝐷𝑅𝐵))
 
Theoremcaovdig 5949* Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
((𝜑 ∧ (𝑥𝐾𝑦𝑆𝑧𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧)))       ((𝜑 ∧ (𝐴𝐾𝐵𝑆𝐶𝑆)) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶)))
 
Theoremcaovdid 5950* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝐾𝑦𝑆𝑧𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧)))    &   (𝜑𝐴𝐾)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)       (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶)))
 
Theoremcaovdir2d 5951* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))       (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶)))
 
Theoremcaovdirg 5952* Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)))       ((𝜑 ∧ (𝐴𝑆𝐵𝑆𝐶𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))
 
Theoremcaovdird 5953* Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧)))    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝐾)       (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶)))
 
Theoremcaovdi 5954* Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))       (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶))
 
Theoremcaov32d 5955* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵))
 
Theoremcaov12d 5956* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)))
 
Theoremcaov31d 5957* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴))
 
Theoremcaov13d 5958* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))       (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)))
 
Theoremcaov4d 5959* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐷𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷)))
 
Theoremcaov411d 5960* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐷𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷)))
 
Theoremcaov42d 5961* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
(𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝜑𝐷𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵)))
 
Theoremcaov32 5962* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)
 
Theoremcaov12 5963* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))
 
Theoremcaov31 5964* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)
 
Theoremcaov13 5965* Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   (𝑥𝐹𝑦) = (𝑦𝐹𝑥)    &   ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))       (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))
 
Theoremcaovdilemd 5966* Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   (𝜑𝐷𝑆)    &   (𝜑𝐻𝑆)       (𝜑 → (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻))))
 
Theoremcaovlem2d 5967* Rearrangement of expression involving multiplication (𝐺) and addition (𝐹). (Contributed by Jim Kingdon, 3-Jan-2020.)
((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   (𝜑𝐶𝑆)    &   (𝜑𝐷𝑆)    &   (𝜑𝐻𝑆)    &   (𝜑𝑅𝑆)    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)       (𝜑 → ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))))
 
Theoremcaovimo 5968* Uniqueness of inverse element in commutative, associative operation with identity. The identity element is 𝐵. (Contributed by Jim Kingdon, 18-Sep-2019.)
𝐵𝑆    &   ((𝑥𝑆𝑦𝑆) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))    &   ((𝑥𝑆𝑦𝑆𝑧𝑆) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)))    &   (𝑥𝑆 → (𝑥𝐹𝐵) = 𝑥)       (𝐴𝑆 → ∃*𝑤(𝑤𝑆 ∧ (𝐴𝐹𝑤) = 𝐵))
 
Theoremgrprinvlem 5969* Lemma for grprinvd 5970. (Contributed by NM, 9-Aug-2013.)
((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   (𝜑𝑂𝐵)    &   ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)    &   ((𝜑𝜓) → 𝑋𝐵)    &   ((𝜑𝜓) → (𝑋 + 𝑋) = 𝑋)       ((𝜑𝜓) → 𝑋 = 𝑂)
 
Theoremgrprinvd 5970* 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.)
((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   (𝜑𝑂𝐵)    &   ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)    &   ((𝜑𝜓) → 𝑋𝐵)    &   ((𝜑𝜓) → 𝑁𝐵)    &   ((𝜑𝜓) → (𝑁 + 𝑋) = 𝑂)       ((𝜑𝜓) → (𝑋 + 𝑁) = 𝑂)
 
Theoremgrpridd 5971* 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.)
((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   (𝜑𝑂𝐵)    &   ((𝜑𝑥𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 𝑂)       ((𝜑𝑥𝐵) → (𝑥 + 𝑂) = 𝑥)
 
2.6.11  Maps-to notation
 
Theoremelmpocl 5972* If a two-parameter class is inhabited, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆𝐴𝑇𝐵))
 
Theoremelmpocl1 5973* If a two-parameter class is inhabited, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (𝑋 ∈ (𝑆𝐹𝑇) → 𝑆𝐴)
 
Theoremelmpocl2 5974* If a two-parameter class is inhabited, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (𝑋 ∈ (𝑆𝐹𝑇) → 𝑇𝐵)
 
Theoremelovmpo 5975* Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.)
𝐷 = (𝑎𝐴, 𝑏𝐵𝐶)    &   𝐶 ∈ V    &   ((𝑎 = 𝑋𝑏 = 𝑌) → 𝐶 = 𝐸)       (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋𝐴𝑌𝐵𝐹𝐸))
 
Theoremf1ocnvd 5976* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝑊)    &   ((𝜑𝑦𝐵) → 𝐷𝑋)    &   (𝜑 → ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷)))       (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
 
Theoremf1od 5977* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝑊)    &   ((𝜑𝑦𝐵) → 𝐷𝑋)    &   (𝜑 → ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷)))       (𝜑𝐹:𝐴1-1-onto𝐵)
 
Theoremf1ocnv2d 5978* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝐵)    &   ((𝜑𝑦𝐵) → 𝐷𝐴)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))       (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐹 = (𝑦𝐵𝐷)))
 
Theoremf1o2d 5979* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
𝐹 = (𝑥𝐴𝐶)    &   ((𝜑𝑥𝐴) → 𝐶𝐵)    &   ((𝜑𝑦𝐵) → 𝐷𝐴)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑥 = 𝐷𝑦 = 𝐶))       (𝜑𝐹:𝐴1-1-onto𝐵)
 
Theoremf1opw2 5980* A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 5981 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.)
(𝜑𝐹:𝐴1-1-onto𝐵)    &   (𝜑 → (𝐹𝑎) ∈ V)    &   (𝜑 → (𝐹𝑏) ∈ V)       (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹𝑏)):𝒫 𝐴1-1-onto→𝒫 𝐵)
 
Theoremf1opw 5981* 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.)
(𝐹:𝐴1-1-onto𝐵 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹𝑏)):𝒫 𝐴1-1-onto→𝒫 𝐵)
 
Theoremsuppssfv 5982* Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(𝜑 → ((𝑥𝐷𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)    &   (𝜑 → (𝐹𝑌) = 𝑍)    &   ((𝜑𝑥𝐷) → 𝐴𝑉)       (𝜑 → ((𝑥𝐷 ↦ (𝐹𝐴)) “ (V ∖ {𝑍})) ⊆ 𝐿)
 
Theoremsuppssov1 5983* Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
(𝜑 → ((𝑥𝐷𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)    &   ((𝜑𝑣𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ((𝜑𝑥𝐷) → 𝐴𝑉)    &   ((𝜑𝑥𝐷) → 𝐵𝑅)       (𝜑 → ((𝑥𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) ⊆ 𝐿)
 
2.6.12  Function operation
 
Syntaxcof 5984 Extend class notation to include mapping of an operation to a function operation.
class 𝑓 𝑅
 
Syntaxcofr 5985 Extend class notation to include mapping of a binary relation to a function relation.
class 𝑟 𝑅
 
Definitiondf-of 5986* 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.)
𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓𝑥)𝑅(𝑔𝑥))))
 
Definitiondf-ofr 5987* 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.)
𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓𝑥)𝑅(𝑔𝑥)}
 
Theoremofeq 5988 Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝑅 = 𝑆 → ∘𝑓 𝑅 = ∘𝑓 𝑆)
 
Theoremofreq 5989 Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝑅 = 𝑆 → ∘𝑟 𝑅 = ∘𝑟 𝑆)
 
Theoremofexg 5990 A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.)
(𝐴𝑉 → ( ∘𝑓 𝑅𝐴) ∈ V)
 
Theoremnfof 5991 Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
𝑥𝑅       𝑥𝑓 𝑅
 
Theoremnfofr 5992 Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
𝑥𝑅       𝑥𝑟 𝑅
 
Theoremoffval 5993* Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)    &   ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)       (𝜑 → (𝐹𝑓 𝑅𝐺) = (𝑥𝑆 ↦ (𝐶𝑅𝐷)))
 
Theoremofrfval 5994* Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐶)    &   ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐷)       (𝜑 → (𝐹𝑟 𝑅𝐺 ↔ ∀𝑥𝑆 𝐶𝑅𝐷))
 
Theoremofvalg 5995 Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)    &   ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)    &   ((𝜑𝑋𝑆) → (𝐶𝑅𝐷) ∈ 𝑈)       ((𝜑𝑋𝑆) → ((𝐹𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷))
 
Theoremofrval 5996 Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝑆    &   ((𝜑𝑋𝐴) → (𝐹𝑋) = 𝐶)    &   ((𝜑𝑋𝐵) → (𝐺𝑋) = 𝐷)       ((𝜑𝐹𝑟 𝑅𝐺𝑋𝑆) → 𝐶𝑅𝐷)
 
Theoremofmresval 5997 Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
(𝜑𝐹𝐴)    &   (𝜑𝐺𝐵)       (𝜑 → (𝐹( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹𝑓 𝑅𝐺))
 
Theoremoff 5998* The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐺:𝐵𝑇)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝐶       (𝜑 → (𝐹𝑓 𝑅𝐺):𝐶𝑈)
 
Theoremoffeq 5999* Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Jim Kingdon, 26-Nov-2023.)
((𝜑 ∧ (𝑥𝑆𝑦𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)    &   (𝜑𝐹:𝐴𝑆)    &   (𝜑𝐺:𝐵𝑇)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝐶    &   (𝜑𝐻:𝐶𝑈)    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐷)    &   ((𝜑𝑥𝐵) → (𝐺𝑥) = 𝐸)    &   ((𝜑𝑥𝐶) → (𝐷𝑅𝐸) = (𝐻𝑥))       (𝜑 → (𝐹𝑓 𝑅𝐺) = 𝐻)
 
Theoremofres 6000 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 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝐴𝐵) = 𝐶       (𝜑 → (𝐹𝑓 𝑅𝐺) = ((𝐹𝐶) ∘𝑓 𝑅(𝐺𝐶)))
    < Previous  Next >

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-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13424
  Copyright terms: Public domain < Previous  Next >