Theorem List for Intuitionistic Logic Explorer - 6001-6100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ovmpodv 6001* |
Alternate deduction version of ovmpo 6004, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
|
Theorem | ovmpodv2 6002* |
Alternate deduction version of ovmpo 6004, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉)
& ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = 𝑆)) |
|
Theorem | ovmpog 6003* |
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 6004* |
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 6005* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro,
29-Dec-2014.)
|
⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → 𝑆 ∈ (𝐻 × 𝐻)) & ⊢ (((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) ∧ (𝑢 = 𝐶 ∧ 𝑓 = 𝐷)) → 𝑅 = 𝑆)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (𝐻 × 𝐻) ∧ 𝑦 ∈ (𝐻 × 𝐻)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 𝑅))} ⇒ ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ 𝐻)) → (〈𝐴, 𝐵〉𝐹〈𝐶, 𝐷〉) = 𝑆) |
|
Theorem | ov6g 6006* |
The value of an operation class abstraction. Special case.
(Contributed by NM, 13-Nov-2006.)
|
⊢ (〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → 𝑅 = 𝑆)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (〈𝑥, 𝑦〉 ∈ 𝐶 ∧ 𝑧 = 𝑅)} ⇒ ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻 ∧ 〈𝐴, 𝐵〉 ∈ 𝐶) ∧ 𝑆 ∈ 𝐽) → (𝐴𝐹𝐵) = 𝑆) |
|
Theorem | ovg 6007* |
The value of an operation class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑)
& ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ⇒ ⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) |
|
Theorem | ovres 6008 |
The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵)) |
|
Theorem | ovresd 6009 |
Lemma for converting metric theorems to metric space theorems.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑋)
& ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵)) |
|
Theorem | oprssov 6010 |
The value of a member of the domain of a subclass of an operation.
(Contributed by NM, 23-Aug-2007.)
|
⊢ (((Fun 𝐹 ∧ 𝐺 Fn (𝐶 × 𝐷) ∧ 𝐺 ⊆ 𝐹) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) |
|
Theorem | fovcdm 6011 |
An operation's value belongs to its codomain. (Contributed by NM,
27-Aug-2006.)
|
⊢ ((𝐹:(𝑅 × 𝑆)⟶𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | fovcdmda 6012 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | fovcdmd 6013 |
An operation's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑅)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐶) |
|
Theorem | fnrnov 6014* |
The range of an operation expressed as a collection of the operation's
values. (Contributed by NM, 29-Oct-2006.)
|
⊢ (𝐹 Fn (𝐴 × 𝐵) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦)}) |
|
Theorem | foov 6015* |
An onto mapping of an operation expressed in terms of operation values.
(Contributed by NM, 29-Oct-2006.)
|
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑧 ∈ 𝐶 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥𝐹𝑦))) |
|
Theorem | fnovrn 6016 |
An operation's value belongs to its range. (Contributed by NM,
10-Feb-2007.)
|
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶𝐹𝐷) ∈ ran 𝐹) |
|
Theorem | ovelrn 6017* |
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 6018* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|
⊢ ((Fun 𝐹 ∧ (𝐴 × 𝐵) ⊆ dom 𝐹) → ((𝐹 “ (𝐴 × 𝐵)) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶)) |
|
Theorem | ovelimab 6019* |
Operation value in an image. (Contributed by Mario Carneiro,
23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|
⊢ ((𝐹 Fn 𝐴 ∧ (𝐵 × 𝐶) ⊆ 𝐴) → (𝐷 ∈ (𝐹 “ (𝐵 × 𝐶)) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝐷 = (𝑥𝐹𝑦))) |
|
Theorem | ovconst2 6020 |
The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵) → (𝑅((𝐴 × 𝐵) × {𝐶})𝑆) = 𝐶) |
|
Theorem | caovclg 6021* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 26-May-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) → (𝐴𝐹𝐵) ∈ 𝐸) |
|
Theorem | caovcld 6022* |
Convert an operation closure law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥𝐹𝑦) ∈ 𝐸)
& ⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝐸) |
|
Theorem | caovcl 6023* |
Convert an operation closure law to class notation. (Contributed by NM,
4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) |
|
Theorem | caovcomg 6024* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) |
|
Theorem | caovcomd 6025* |
Convert an operation commutative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐵𝐹𝐴)) |
|
Theorem | caovcom 6026* |
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 6027* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro,
26-May-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) |
|
Theorem | caovassd 6028* |
Convert an operation associative law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) |
|
Theorem | caovass 6029* |
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 6030* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | caovcand 6031* |
Convert an operation cancellation law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))
& ⊢ (𝜑 → 𝐴 ∈ 𝑇)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | caovcanrd 6032* |
Commute the arguments of an operation cancellation law. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) ↔ 𝑦 = 𝑧))
& ⊢ (𝜑 → 𝐴 ∈ 𝑇)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → ((𝐵𝐹𝐴) = (𝐶𝐹𝐴) ↔ 𝐵 = 𝐶)) |
|
Theorem | caovcan 6033* |
Convert an operation cancellation law to class notation. (Contributed
by NM, 20-Aug-1995.)
|
⊢ 𝐶 ∈ V & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥𝐹𝑦) = (𝑥𝐹𝑧) → 𝑦 = 𝑧)) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) = (𝐴𝐹𝐶) → 𝐵 = 𝐶)) |
|
Theorem | caovordig 6034* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovordid 6035* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 → (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 → (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovordg 6036* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovordd 6037* |
Convert an operation ordering law to class notation. (Contributed by
Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovord2d 6038* |
Operation ordering law with commuted arguments. (Contributed by Mario
Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) |
|
Theorem | caovord3d 6039* |
Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ (𝜑 → 𝐷 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵) = (𝐶𝐹𝐷) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵))) |
|
Theorem | caovord 6040* |
Convert an operation ordering law to class notation. (Contributed by
NM, 19-Feb-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵))) |
|
Theorem | caovord2 6041* |
Operation ordering law with commuted arguments. (Contributed by NM,
27-Feb-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥) ⇒ ⊢ (𝐶 ∈ 𝑆 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶))) |
|
Theorem | caovord3 6042* |
Ordering law. (Contributed by NM, 29-Feb-1996.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑧 ∈ 𝑆 → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦))) & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ 𝐷 ∈ V ⇒ ⊢ (((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) ∧ (𝐴𝐹𝐵) = (𝐶𝐹𝐷)) → (𝐴𝑅𝐶 ↔ 𝐷𝑅𝐵)) |
|
Theorem | caovdig 6043* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) |
|
Theorem | caovdid 6044* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐻(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝐾)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐻(𝐴𝐺𝐶))) |
|
Theorem | caovdir2d 6045* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐶))) |
|
Theorem | caovdirg 6046* |
Convert an operation reverse distributive law to class notation.
(Contributed by Mario Carneiro, 19-Oct-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐾)) → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) |
|
Theorem | caovdird 6047* |
Convert an operation distributive law to class notation. (Contributed
by Mario Carneiro, 30-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐻(𝑦𝐺𝑧))) & ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐻(𝐵𝐺𝐶))) |
|
Theorem | caovdi 6048* |
Convert an operation distributive law to class notation. (Contributed
by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐺(𝑦𝐹𝑧)) = ((𝑥𝐺𝑦)𝐹(𝑥𝐺𝑧)) ⇒ ⊢ (𝐴𝐺(𝐵𝐹𝐶)) = ((𝐴𝐺𝐵)𝐹(𝐴𝐺𝐶)) |
|
Theorem | caov32d 6049* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵)) |
|
Theorem | caov12d 6050* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))) |
|
Theorem | caov31d 6051* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴)) |
|
Theorem | caov13d 6052* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) ⇒ ⊢ (𝜑 → (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴))) |
|
Theorem | caov4d 6053* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐵𝐹𝐷))) |
|
Theorem | caov411d 6054* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹𝐵)𝐹(𝐴𝐹𝐷))) |
|
Theorem | caov42d 6055* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro,
30-Dec-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴𝐹𝐵)𝐹(𝐶𝐹𝐷)) = ((𝐴𝐹𝐶)𝐹(𝐷𝐹𝐵))) |
|
Theorem | caov32 6056* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐴𝐹𝐶)𝐹𝐵) |
|
Theorem | caov12 6057* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶)) |
|
Theorem | caov31 6058* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐶𝐹𝐵)𝐹𝐴) |
|
Theorem | caov13 6059* |
Rearrange arguments in a commutative, associative operation.
(Contributed by NM, 26-Aug-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
& ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧)) ⇒ ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐶𝐹(𝐵𝐹𝐴)) |
|
Theorem | caovdilemd 6060* |
Lemma used by real number construction. (Contributed by Jim Kingdon,
16-Sep-2019.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ (𝜑 → 𝐻 ∈ 𝑆) ⇒ ⊢ (𝜑 → (((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻) = ((𝐴𝐺(𝐶𝐺𝐻))𝐹(𝐵𝐺(𝐷𝐺𝐻)))) |
|
Theorem | caovlem2d 6061* |
Rearrangement of expression involving multiplication (𝐺) and
addition (𝐹). (Contributed by Jim Kingdon,
3-Jan-2020.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐺𝑧) = ((𝑥𝐺𝑧)𝐹(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐺𝑦) ∈ 𝑆)
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑆)
& ⊢ (𝜑 → 𝐶 ∈ 𝑆)
& ⊢ (𝜑 → 𝐷 ∈ 𝑆)
& ⊢ (𝜑 → 𝐻 ∈ 𝑆)
& ⊢ (𝜑 → 𝑅 ∈ 𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((((𝐴𝐺𝐶)𝐹(𝐵𝐺𝐷))𝐺𝐻)𝐹(((𝐴𝐺𝐷)𝐹(𝐵𝐺𝐶))𝐺𝑅)) = ((𝐴𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(𝐵𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))))) |
|
Theorem | caovimo 6062* |
Uniqueness of inverse element in commutative, associative operation with
identity. The identity element is 𝐵. (Contributed by Jim Kingdon,
18-Sep-2019.)
|
⊢ 𝐵 ∈ 𝑆
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
& ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))) & ⊢ (𝑥 ∈ 𝑆 → (𝑥𝐹𝐵) = 𝑥) ⇒ ⊢ (𝐴 ∈ 𝑆 → ∃*𝑤(𝑤 ∈ 𝑆 ∧ (𝐴𝐹𝑤) = 𝐵)) |
|
2.6.12 Maps-to notation
|
|
Theorem | elmpocl 6063* |
If a two-parameter class is inhabited, constrain the implicit pair.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐵)) |
|
Theorem | elmpocl1 6064* |
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.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑆 ∈ 𝐴) |
|
Theorem | elmpocl2 6065* |
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.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝑋 ∈ (𝑆𝐹𝑇) → 𝑇 ∈ 𝐵) |
|
Theorem | elovmpo 6066* |
Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear,
21-Jan-2015.)
|
⊢ 𝐷 = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵 ↦ 𝐶)
& ⊢ 𝐶 ∈ V & ⊢ ((𝑎 = 𝑋 ∧ 𝑏 = 𝑌) → 𝐶 = 𝐸) ⇒ ⊢ (𝐹 ∈ (𝑋𝐷𝑌) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹 ∈ 𝐸)) |
|
Theorem | f1ocnvd 6067* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋)
& ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) |
|
Theorem | f1od 6068* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑋)
& ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
|
Theorem | f1ocnv2d 6069* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 30-Apr-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) |
|
Theorem | f1o2d 6070* |
Describe an implicit one-to-one onto function. (Contributed by Mario
Carneiro, 12-May-2014.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)
& ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
|
Theorem | f1opw2 6071* |
A one-to-one mapping induces a one-to-one mapping on power sets. This
version of f1opw 6072 avoids the Axiom of Replacement.
(Contributed by
Mario Carneiro, 26-Jun-2015.)
|
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
& ⊢ (𝜑 → (◡𝐹 “ 𝑎) ∈ V) & ⊢ (𝜑 → (𝐹 “ 𝑏) ∈ V) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝒫 𝐴 ↦ (𝐹 “ 𝑏)):𝒫 𝐴–1-1-onto→𝒫 𝐵) |
|
Theorem | f1opw 6072* |
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→𝒫 𝐵) |
|
Theorem | suppssfv 6073* |
Formula building theorem for support restriction, on a function which
preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
Theorem | suppssov1 6074* |
Formula building theorem for support restrictions: operator with left
annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ 𝐴) “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) ⇒ ⊢ (𝜑 → (◡(𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
2.6.13 Function operation
|
|
Syntax | cof 6075 |
Extend class notation to include mapping of an operation to a function
operation.
|
class ∘𝑓 𝑅 |
|
Syntax | cofr 6076 |
Extend class notation to include mapping of a binary relation to a
function relation.
|
class ∘𝑟 𝑅 |
|
Definition | df-of 6077* |
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 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) |
|
Definition | df-ofr 6078* |
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 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} |
|
Theorem | ofeq 6079 |
Equality theorem for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝑅 = 𝑆 → ∘𝑓 𝑅 = ∘𝑓
𝑆) |
|
Theorem | ofreq 6080 |
Equality theorem for function relation. (Contributed by Mario Carneiro,
28-Jul-2014.)
|
⊢ (𝑅 = 𝑆 → ∘𝑟 𝑅 = ∘𝑟
𝑆) |
|
Theorem | ofexg 6081 |
A function operation restricted to a set is a set. (Contributed by NM,
28-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → ( ∘𝑓 𝑅 ↾ 𝐴) ∈ V) |
|
Theorem | nfof 6082 |
Hypothesis builder for function operation. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘𝑓
𝑅 |
|
Theorem | nfofr 6083 |
Hypothesis builder for function relation. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘𝑟
𝑅 |
|
Theorem | offval 6084* |
Value of an operation applied to two functions. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) |
|
Theorem | ofrfval 6085* |
Value of a relation applied to two functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) |
|
Theorem | ofvalg 6086 |
Evaluate a function operation at a point. (Contributed by Mario
Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐶𝑅𝐷) ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) |
|
Theorem | ofrval 6087 |
Exhibit a function relation at a point. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝑆
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶)
& ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘𝑟 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) |
|
Theorem | ofmresval 6088 |
Value of a restriction of the function operation map. (Contributed by
NM, 20-Oct-2014.)
|
⊢ (𝜑 → 𝐹 ∈ 𝐴)
& ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘𝑓 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘𝑓 𝑅𝐺)) |
|
Theorem | off 6089* |
The function operation produces a function. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺):𝐶⟶𝑈) |
|
Theorem | offeq 6090* |
Convert an identity of the operation to the analogous identity on
the function operation. (Contributed by Jim Kingdon,
26-Nov-2023.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐵⟶𝑇)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶
& ⊢ (𝜑 → 𝐻:𝐶⟶𝑈)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐸)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷𝑅𝐸) = (𝐻‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = 𝐻) |
|
Theorem | ofres 6091 |
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 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = ((𝐹 ↾ 𝐶) ∘𝑓 𝑅(𝐺 ↾ 𝐶))) |
|
Theorem | offval2 6092* |
The function operation expressed as a mapping. (Contributed by Mario
Carneiro, 20-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) |
|
Theorem | ofrfval2 6093* |
The function relation acting on maps. (Contributed by Mario Carneiro,
20-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) |
|
Theorem | suppssof1 6094* |
Formula building theorem for support restrictions: vector operation with
left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ (𝜑 → (◡𝐴 “ (V ∖ {𝑌})) ⊆ 𝐿)
& ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)
& ⊢ (𝜑 → 𝐴:𝐷⟶𝑉)
& ⊢ (𝜑 → 𝐵:𝐷⟶𝑅)
& ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (◡(𝐴 ∘𝑓 𝑂𝐵) “ (V ∖ {𝑍})) ⊆ 𝐿) |
|
Theorem | ofco 6095 |
The composition of a function operation with another function.
(Contributed by Mario Carneiro, 19-Dec-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐵)
& ⊢ (𝜑 → 𝐻:𝐷⟶𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐷 ∈ 𝑋)
& ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘𝑓 𝑅(𝐺 ∘ 𝐻))) |
|
Theorem | offveqb 6096* |
Equivalent expressions for equality with a function operation.
(Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro,
5-Dec-2016.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐴)
& ⊢ (𝜑 → 𝐻 Fn 𝐴)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) ⇒ ⊢ (𝜑 → (𝐻 = (𝐹 ∘𝑓 𝑅𝐺) ↔ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐵𝑅𝐶))) |
|
Theorem | ofc12 6097 |
Function operation on two constant functions. (Contributed by Mario
Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) |
|
Theorem | caofref 6098* |
Transfer a reflexive law to the function relation. (Contributed by
Mario Carneiro, 28-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘𝑟 𝑅𝐹) |
|
Theorem | caofinvl 6099* |
Transfer a left inverse law to the function operation. (Contributed
by NM, 22-Oct-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝑁:𝑆⟶𝑆)
& ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘𝑓 𝑅𝐹) = (𝐴 × {𝐵})) |
|
Theorem | caofcom 6100* |
Transfer a commutative law to the function operation. (Contributed by
Mario Carneiro, 26-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)
& ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝐺 ∘𝑓 𝑅𝐹)) |