Home | Metamath
Proof Explorer Theorem List (p. 66 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | f1oiso 6501* | Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.) |
⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑆 = {〈𝑧, 𝑤〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑧 = (𝐻‘𝑥) ∧ 𝑤 = (𝐻‘𝑦)) ∧ 𝑥𝑅𝑦)}) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | f1oiso2 6502* | Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (◡𝐻‘𝑥)𝑅(◡𝐻‘𝑦))} ⇒ ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | f1owe 6503* | Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | weniso 6504 | A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴)) | ||
Theorem | weisoeq 6505 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7044. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺) | ||
Theorem | weisoeq2 6506 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7045. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ (((𝑆 We 𝐵 ∧ 𝑆 Se 𝐵) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺) | ||
Theorem | knatar 6507* | The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice 𝒫 𝐴. (Contributed by Mario Carneiro, 11-Jun-2015.) |
⊢ 𝑋 = ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ⊆ 𝐴 ∧ (𝐹‘𝑋) = 𝑋)) | ||
Theorem | canth 6508 | No set 𝐴 is equinumerous to its power set (Cantor's theorem), i.e. no function can map 𝐴 it onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 7998. Note that 𝐴 must be a set: this theorem does not hold when 𝐴 is too large to be a set; see ncanth 6509 for a counterexample. (Use nex 1722 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴 | ||
Theorem | ncanth 6509 | Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 4724). Specifically, the identity function maps the universe onto its power class. Compare canth 6508 that works for sets. See also the remark in ru 3401 about NF, in which Cantor's theorem fails for sets that are "too large." This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004.) |
⊢ I :V–onto→𝒫 V | ||
Syntax | crio 6510 | Extend class notation with restricted description binder. |
class (℩𝑥 ∈ 𝐴 𝜑) | ||
Definition | df-riota 6511 | Define restricted description binder. In case there is no unique 𝑥 such that (𝑥 ∈ 𝐴 ∧ 𝜑) holds, it evaluates to the empty set. See also comments for df-iota 5768. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | riotaeqdv 6512* | Formula-building deduction rule for iota. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | riotabidv 6513* | Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | riotaeqbidv 6514* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | riotaex 6515 | Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V | ||
Theorem | riotav 6516 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑) | ||
Theorem | riotauni 6517 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | nfriota1 6518* | The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑) | ||
Theorem | nfriotad 6519 | Deduction version of nfriota 6520. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | nfriota 6520* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑) | ||
Theorem | cbvriota 6521* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvriotav 6522* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | csbriota 6523* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) | ||
Theorem | riotacl2 6524 |
Membership law for "the unique element in 𝐴 such that 𝜑."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | riotacl 6525* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
Theorem | riotasbc 6526 | Substitution law for descriptions. Compare iotasbc 37642. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑) | ||
Theorem | riotabidva 6527* | Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 3163 analog.) (Contributed by NM, 17-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | riotabiia 6528 | Equivalent wff's yield equal restricted iotas (inference rule). (rabbiia 3161 analog.) (Contributed by NM, 16-Jan-2012.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓) | ||
Theorem | riota1 6529* | Property of restricted iota. Compare iota1 5782. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥)) | ||
Theorem | riota1a 6530 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥)) | ||
Theorem | riota2df 6531* | A deduction version of riota2f 6532. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)) | ||
Theorem | riota2f 6532* | This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) | ||
Theorem | riota2 6533* | This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) | ||
Theorem | riotaprop 6534* | Properties of a restricted definite description operator. TODO (df-riota 6511 update): can some uses of riota2f 6532 be shortened with this? (Contributed by NM, 23-Nov-2013.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 𝜑) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜓)) | ||
Theorem | riota5f 6535* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) | ||
Theorem | riota5 6536* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) | ||
Theorem | riotass2 6537* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | riotass 6538* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | moriotass 6539* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | snriota 6540 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {(℩𝑥 ∈ 𝐴 𝜑)}) | ||
Theorem | riotaxfrd 6541* | Change the variable 𝑥 in the expression for "the unique 𝑥 such that 𝜓 " to another variable 𝑦 contained in expression 𝐵. Use reuhypd 4821 to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝐶 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ (℩𝑦 ∈ 𝐴 𝜒) ∈ 𝐴) → 𝐶 ∈ 𝐴) & ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = (℩𝑦 ∈ 𝐴 𝜒) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐴 𝑥 = 𝐵) ⇒ ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐶) | ||
Theorem | eusvobj2 6542* | Specify the same property in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | eusvobj1 6543* | Specify the same object in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (℩𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) = (℩𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | f1ofveu 6544* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃!𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶) | ||
Theorem | f1ocnvfv3 6545* | Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) = (℩𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶)) | ||
Theorem | riotaund 6546* | Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.) |
⊢ (¬ ∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∅) | ||
Theorem | riotassuni 6547* | The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (℩𝑥 ∈ 𝐴 𝜑) ⊆ (𝒫 ∪ 𝐴 ∪ ∪ 𝐴) | ||
Theorem | riotaclb 6548* | Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) (Revised by NM, 13-Sep-2018.) |
⊢ (¬ ∅ ∈ 𝐴 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)) | ||
Syntax | co 6549 | Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 10146.) |
class (𝐴𝐹𝐵) | ||
Syntax | coprab 6550 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Syntax | cmpt2 6551 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Definition | df-ov 6552 | Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 11037). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6582 and ovprc2 6583. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7478. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6553. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | ||
Definition | df-oprab 6553* | Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 6552 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpt2 6694. (Contributed by NM, 12-Mar-1995.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} | ||
Definition | df-mpt2 6554* | Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐶(𝑥, 𝑦)." An extension of df-mpt 4645 for two arguments. (Contributed by NM, 17-Feb-2008.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | ||
Theorem | oveq 6555 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) | ||
Theorem | oveq1 6556 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) | ||
Theorem | oveq2 6557 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵)) | ||
Theorem | oveq12 6558 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveq1i 6559 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶) | ||
Theorem | oveq2i 6560 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵) | ||
Theorem | oveq12i 6561 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) | ||
Theorem | oveqi 6562 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷) | ||
Theorem | oveq123i 6563 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 & ⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷) | ||
Theorem | oveq1d 6564 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) | ||
Theorem | oveq2d 6565 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵)) | ||
Theorem | oveqd 6566 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷)) | ||
Theorem | oveq12d 6567 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveqan12d 6568 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveqan12rd 6569 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveq123d 6570 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷)) | ||
Theorem | ovrspc2v 6571* | If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶) → (𝑋𝐹𝑌) ∈ 𝐶) | ||
Theorem | oveqrspc2v 6572* | Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐹𝑌) = (𝑋𝐺𝑌)) | ||
Theorem | oveqdr 6573 | Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) | ||
Theorem | nfovd 6574 | Deduction version of bound-variable hypothesis builder nfov 6575. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐹) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵)) | ||
Theorem | nfov 6575 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴𝐹𝐵) | ||
Theorem | oprabid 6576 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ (〈〈𝑥, 𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) | ||
Theorem | ovex 6577 | The result of an operation is a set. (Contributed by NM, 13-Mar-1995.) |
⊢ (𝐴𝐹𝐵) ∈ V | ||
Theorem | ovexi 6578 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = (𝐵𝐹𝐶) ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | ovssunirn 6579 | The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝑋𝐹𝑌) ⊆ ∪ ran 𝐹 | ||
Theorem | 0ov 6580 | Operation value of the empty set. (Contributed by AV, 15-May-2021.) |
⊢ (𝐴∅𝐵) = ∅ | ||
Theorem | ovprc 6581 | The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ovprc1 6582 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ovprc2 6583 | The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅) | ||
Theorem | ovrcl 6584 | Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.) |
⊢ Rel dom 𝐹 ⇒ ⊢ (𝐶 ∈ (𝐴𝐹𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | csbov123 6585 | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵⦋𝐴 / 𝑥⦌𝐹⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbov 6586* | Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵⦋𝐴 / 𝑥⦌𝐹𝐶) | ||
Theorem | csbov12g 6587* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | csbov1g 6588* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹𝐶)) | ||
Theorem | csbov2g 6589* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | rspceov 6590* | A frequently used special case of rspc2ev 3295 for operation values. (Contributed by NM, 21-Mar-2007.) |
⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ 𝑆 = (𝐶𝐹𝐷)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑆 = (𝑥𝐹𝑦)) | ||
Theorem | elovimad 6591 | Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐶 × 𝐷) ⊆ dom 𝐹) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ (𝐹 “ (𝐶 × 𝐷))) | ||
Theorem | fnotovb 6592 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6147. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐶𝐹𝐷) = 𝑅 ↔ 〈𝐶, 𝐷, 𝑅〉 ∈ 𝐹)) | ||
Theorem | opabbrex 6593 | A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by BJ/AV, 20-Jun-2019.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ ((∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝜑) ∧ {〈𝑥, 𝑦〉 ∣ 𝜑} ∈ 𝑉) → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | fvmptopab1 6594* | The function value of a mapping 𝑀 to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function 𝐹 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) & ⊢ 𝑀 = (𝑧 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)}) ⇒ ⊢ (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) | ||
Theorem | fvmptopab2 6595* | The function value of a mapping 𝑀 to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function 𝐹 restricted by the conditions 𝜓 and 𝜏. (Contributed by AV, 31-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) & ⊢ 𝑀 = (𝑧 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒 ∧ 𝜃)}) & ⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓 ∧ 𝜏)}) | ||
Theorem | 0neqopab 6596 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | brabv 6597 | If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ (𝑋{〈𝑥, 𝑦〉 ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | ||
Theorem | brfvopab 6598 | The classes involved in a binary relation of a function value which is an ordered-pair class abstraction are sets. (Contributed by AV, 7-Jan-2021.) |
⊢ (𝑋 ∈ V → (𝐹‘𝑋) = {〈𝑦, 𝑧〉 ∣ 𝜑}) ⇒ ⊢ (𝐴(𝐹‘𝑋)𝐵 → (𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | dfoprab2 6599* | Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | ||
Theorem | reloprab 6600* | An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.) |
⊢ Rel {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |