![]() |
Metamath
Proof Explorer Theorem List (p. 318 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mdsymlem8 31701* | Lemma for mdsymi 31702. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ & β’ πΆ = (π΄ β¨β π) β β’ ((π΄ β 0β β§ π΅ β 0β) β (π΅ πβ* π΄ β π΄ πβ* π΅)) | ||
Theorem | mdsymi 31702 | M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ π΅ β π΅ πβ π΄) | ||
Theorem | mdsym 31703 | M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
β’ ((π΄ β Cβ β§ π΅ β Cβ ) β (π΄ πβ π΅ β π΅ πβ π΄)) | ||
Theorem | dmdsym 31704 | Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.) |
β’ ((π΄ β Cβ β§ π΅ β Cβ ) β (π΄ πβ* π΅ β π΅ πβ* π΄)) | ||
Theorem | atdmd2 31705 | Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
β’ ((π΄ β Cβ β§ π΅ β HAtoms) β π΄ πβ* π΅) | ||
Theorem | sumdmdii 31706 | If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [MaedaMaeda] p. 139. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ ((π΄ +β π΅) = (π΄ β¨β π΅) β π΄ πβ* π΅) | ||
Theorem | cmmdi 31707 | Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πΆβ π΅ β π΄ πβ π΅) | ||
Theorem | cmdmdi 31708 | Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πΆβ π΅ β π΄ πβ* π΅) | ||
Theorem | sumdmdlem 31709 | Lemma for sumdmdi 31711. The span of vector πΆ not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ ((πΆ β β β§ Β¬ πΆ β (π΄ +β π΅)) β ((π΅ +β (spanβ{πΆ})) β© π΄) = (π΅ β© π΄)) | ||
Theorem | sumdmdlem2 31710* | Lemma for sumdmdi 31711. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (βπ₯ β HAtoms ((π₯ β¨β π΅) β© (π΄ β¨β π΅)) β (((π₯ β¨β π΅) β© π΄) β¨β π΅) β (π΄ +β π΅) = (π΄ β¨β π΅)) | ||
Theorem | sumdmdi 31711 | The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ ((π΄ +β π΅) = (π΄ β¨β π΅) β π΄ πβ* π΅) | ||
Theorem | dmdbr4ati 31712* | Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ* π΅ β βπ₯ β HAtoms ((π₯ β¨β π΅) β© (π΄ β¨β π΅)) β (((π₯ β¨β π΅) β© π΄) β¨β π΅)) | ||
Theorem | dmdbr5ati 31713* | Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ* π΅ β βπ₯ β HAtoms (π₯ β (π΄ β¨β π΅) β π₯ β (((π₯ β¨β π΅) β© π΄) β¨β π΅))) | ||
Theorem | dmdbr6ati 31714* | Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ* π΅ β βπ₯ β HAtoms ((π΄ β¨β π΅) β© π₯) = ((((π₯ β¨β π΅) β© π΄) β¨β π΅) β© π₯)) | ||
Theorem | dmdbr7ati 31715* | Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ* π΅ β βπ₯ β HAtoms ((π΄ β¨β π΅) β© π₯) β (((π₯ β¨β π΅) β© π΄) β¨β π΅)) | ||
Theorem | mdoc1i 31716 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ π΄ πβ (β₯βπ΄) | ||
Theorem | mdoc2i 31717 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (β₯βπ΄) πβ π΄ | ||
Theorem | dmdoc1i 31718 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ π΄ πβ* (β₯βπ΄) | ||
Theorem | dmdoc2i 31719 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (β₯βπ΄) πβ* π΄ | ||
Theorem | mdcompli 31720 | A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ π΅ β (π΄ β© (β₯β(π΄ β© π΅))) πβ (π΅ β© (β₯β(π΄ β© π΅)))) | ||
Theorem | dmdcompli 31721 | A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ πβ* π΅ β (π΄ β© (β₯β(π΄ β© π΅))) πβ* (π΅ β© (β₯β(π΄ β© π΅)))) | ||
Theorem | mddmdin0i 31722* | If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ & β’ βπ₯ β Cβ βπ¦ β Cβ ((π₯ πβ* π¦ β§ (π₯ β© π¦) = 0β) β π₯ πβ π¦) β β’ (π΄ πβ* π΅ β π΄ πβ π΅) | ||
Theorem | cdjreui 31723* | A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ ((πΆ β (π΄ +β π΅) β§ (π΄ β© π΅) = 0β) β β!π₯ β π΄ βπ¦ β π΅ πΆ = (π₯ +β π¦)) | ||
Theorem | cdj1i 31724* | Two ways to express "π΄ and π΅ are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (βπ€ β β (0 < π€ β§ βπ¦ β π΄ βπ£ β π΅ ((normββπ¦) + (normββπ£)) β€ (π€ Β· (normββ(π¦ +β π£)))) β βπ₯ β β (0 < π₯ β§ βπ¦ β π΄ βπ§ β π΅ ((normββπ¦) = 1 β π₯ β€ (normββ(π¦ ββ π§))))) | ||
Theorem | cdj3lem1 31725* | A property of "π΄ and π΅ are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (βπ₯ β β (0 < π₯ β§ βπ¦ β π΄ βπ§ β π΅ ((normββπ¦) + (normββπ§)) β€ (π₯ Β· (normββ(π¦ +β π§)))) β (π΄ β© π΅) = 0β) | ||
Theorem | cdj3lem2 31726* | Lemma for cdj3i 31732. Value of the first-component function π. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π§ β π΄ βπ€ β π΅ π₯ = (π§ +β π€))) β β’ ((πΆ β π΄ β§ π· β π΅ β§ (π΄ β© π΅) = 0β) β (πβ(πΆ +β π·)) = πΆ) | ||
Theorem | cdj3lem2a 31727* | Lemma for cdj3i 31732. Closure of the first-component function π. (Contributed by NM, 25-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π§ β π΄ βπ€ β π΅ π₯ = (π§ +β π€))) β β’ ((πΆ β (π΄ +β π΅) β§ (π΄ β© π΅) = 0β) β (πβπΆ) β π΄) | ||
Theorem | cdj3lem2b 31728* | Lemma for cdj3i 31732. The first-component function π is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π§ β π΄ βπ€ β π΅ π₯ = (π§ +β π€))) β β’ (βπ£ β β (0 < π£ β§ βπ₯ β π΄ βπ¦ β π΅ ((normββπ₯) + (normββπ¦)) β€ (π£ Β· (normββ(π₯ +β π¦)))) β βπ£ β β (0 < π£ β§ βπ’ β (π΄ +β π΅)(normββ(πβπ’)) β€ (π£ Β· (normββπ’)))) | ||
Theorem | cdj3lem3 31729* | Lemma for cdj3i 31732. Value of the second-component function π. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π€ β π΅ βπ§ β π΄ π₯ = (π§ +β π€))) β β’ ((πΆ β π΄ β§ π· β π΅ β§ (π΄ β© π΅) = 0β) β (πβ(πΆ +β π·)) = π·) | ||
Theorem | cdj3lem3a 31730* | Lemma for cdj3i 31732. Closure of the second-component function π. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π€ β π΅ βπ§ β π΄ π₯ = (π§ +β π€))) β β’ ((πΆ β (π΄ +β π΅) β§ (π΄ β© π΅) = 0β) β (πβπΆ) β π΅) | ||
Theorem | cdj3lem3b 31731* | Lemma for cdj3i 31732. The second-component function π is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π€ β π΅ βπ§ β π΄ π₯ = (π§ +β π€))) β β’ (βπ£ β β (0 < π£ β§ βπ₯ β π΄ βπ¦ β π΅ ((normββπ₯) + (normββπ¦)) β€ (π£ Β· (normββ(π₯ +β π¦)))) β βπ£ β β (0 < π£ β§ βπ’ β (π΄ +β π΅)(normββ(πβπ’)) β€ (π£ Β· (normββπ’)))) | ||
Theorem | cdj3i 31732* | Two ways to express "π΄ and π΅ are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π§ β π΄ βπ€ β π΅ π₯ = (π§ +β π€))) & β’ π = (π₯ β (π΄ +β π΅) β¦ (β©π€ β π΅ βπ§ β π΄ π₯ = (π§ +β π€))) & β’ (π β βπ£ β β (0 < π£ β§ βπ’ β (π΄ +β π΅)(normββ(πβπ’)) β€ (π£ Β· (normββπ’)))) & β’ (π β βπ£ β β (0 < π£ β§ βπ’ β (π΄ +β π΅)(normββ(πβπ’)) β€ (π£ Β· (normββπ’)))) β β’ (βπ£ β β (0 < π£ β§ βπ₯ β π΄ βπ¦ β π΅ ((normββπ₯) + (normββπ¦)) β€ (π£ Β· (normββ(π₯ +β π¦)))) β ((π΄ β© π΅) = 0β β§ π β§ π)) | ||
Theorem | mathbox 31733 |
(This theorem is a dummy placeholder for these guidelines. The label
of this theorem, "mathbox", is hard-coded into the Metamath
program to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm while allowing you to work independently without affecting other contributors. Even though in a sense your mathbox belongs to you, it is still part of the shared body of knowledge contained in set.mm, and occasionally other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors. If you want to preserve it the way you left it, you can keep a local copy or keep track of the GitHub commit number. Guidelines: 1. See conventions 29691 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md 29691. The Metamath program command "verify markup *" will check that you have followed many of the conventions we use. 2. If at all possible, please use only nullary class constants for new definitions, for example as in df-div 11874. 3. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The Metamath program "MM> WRITE SOURCE set.mm / REWRAP" command will take care of indentation conventions and line wrapping. 4. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 5. Mathboxes must be independent from one another (checked by "verify markup *"). If you need a theorem from another mathbox, typically it is moved to the main part of set.mm. New users should consult with more experienced users before doing this. 6. If a contributor is no longer active, we will continue the usual maintenance edits. As time goes on, often theorems will be moved to main or removed in favor of similar replacements. But we are also willing to maintain mathboxes in place, as work by others from years ago may form the foundation of future work; you could even argue that all of mathematics is like that. 7. For theorems of importance (for example, a Metamath 100 theorem or a dependency of one), we prefer to eventually move them out of mathboxes (although a mathbox is perfectly appropriate as proofs are being developed and refined). (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π β β’ π | ||
Theorem | sa-abvi 31734 | A theorem about the universal class. Inference associated with bj-abv 35878 (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008.) |
β’ π β β’ V = {π₯ β£ π} | ||
Theorem | xfree 31735 | A partial converse to 19.9t 2197. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ (βπ₯(π β βπ₯π) β βπ₯(βπ₯π β π)) | ||
Theorem | xfree2 31736 | A partial converse to 19.9t 2197. (Contributed by Stefan Allan, 21-Dec-2008.) |
β’ (βπ₯(π β βπ₯π) β βπ₯(Β¬ π β βπ₯ Β¬ π)) | ||
Theorem | addltmulALT 31737 | A proof readability experiment for addltmul 12450. (Contributed by Stefan Allan, 30-Oct-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (2 < π΄ β§ 2 < π΅)) β (π΄ + π΅) < (π΄ Β· π΅)) | ||
Theorem | bian1d 31738 | Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.) |
β’ (π β (π β (π β§ π))) β β’ (π β ((π β§ π) β (π β§ π))) | ||
Theorem | or3di 31739 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
β’ ((π β¨ (π β§ π β§ π)) β ((π β¨ π) β§ (π β¨ π) β§ (π β¨ π))) | ||
Theorem | or3dir 31740 | Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
β’ (((π β§ π β§ π) β¨ π) β ((π β¨ π) β§ (π β¨ π) β§ (π β¨ π))) | ||
Theorem | 3o1cs 31741 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
β’ ((π β¨ π β¨ π) β π) β β’ (π β π) | ||
Theorem | 3o2cs 31742 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
β’ ((π β¨ π β¨ π) β π) β β’ (π β π) | ||
Theorem | 3o3cs 31743 | Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016.) |
β’ ((π β¨ π β¨ π) β π) β β’ (π β π) | ||
Theorem | 13an22anass 31744 | Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ ((π β§ (π β§ π β§ π)) β ((π β§ π) β§ (π β§ π))) | ||
Theorem | sbc2iedf 31745* | Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ β²π₯π & β’ β²π¦π & β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β (π β π)) β β’ (π β ([π΄ / π₯][π΅ / π¦]π β π)) | ||
Theorem | rspc2daf 31746* | Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ β²π₯π & β’ β²π¦π & β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ = π΄ β§ π¦ = π΅)) β (π β π)) & β’ (π β βπ₯ β π βπ¦ β π π) β β’ (π β π) | ||
Theorem | ralcom4f 31747* | Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.) |
β’ β²π¦π΄ β β’ (βπ₯ β π΄ βπ¦π β βπ¦βπ₯ β π΄ π) | ||
Theorem | rexcom4f 31748* | Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Revised by Thierry Arnoux, 8-Mar-2017.) |
β’ β²π¦π΄ β β’ (βπ₯ β π΄ βπ¦π β βπ¦βπ₯ β π΄ π) | ||
Theorem | 19.9d2rf 31749 | A deduction version of one direction of 19.9 2198 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017.) |
β’ β²π¦π & β’ (π β β²π₯π) & β’ (π β β²π¦π) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) β β’ (π β π) | ||
Theorem | 19.9d2r 31750* | A deduction version of one direction of 19.9 2198 with two variables. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
β’ (π β β²π₯π) & β’ (π β β²π¦π) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π) β β’ (π β π) | ||
Theorem | r19.29ffa 31751* | A commonly used pattern based on r19.29 3114, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) |
β’ ((((π β§ π₯ β π΄) β§ π¦ β π΅) β§ π) β π) β β’ ((π β§ βπ₯ β π΄ βπ¦ β π΅ π) β π) | ||
Theorem | eqtrb 31752 | A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ ((π΄ = π΅ β§ π΄ = πΆ) β (π΄ = π΅ β§ π΅ = πΆ)) | ||
Theorem | eqelbid 31753* | A variable elimination law for equality within a given set π΄. See equvel 2455. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ (π β π΅ β π΄) & β’ (π β πΆ β π΄) β β’ (π β (βπ₯ β π΄ (π₯ = π΅ β π₯ = πΆ) β π΅ = πΆ)) | ||
Theorem | opsbc2ie 31754* | Conversion of implicit substitution to explicit class substitution for ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ (π = β¨π, πβ© β (π β π)) β β’ (π = β¨π₯, π¦β© β (π β [π¦ / π][π₯ / π]π)) | ||
Theorem | opreu2reuALT 31755* | Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6293 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π = β¨π, πβ© β (π β π)) β β’ ((β!π β π΄ βπ β π΅ π β§ β!π β π΅ βπ β π΄ π) β β!π β (π΄ Γ π΅)π) | ||
Syntax | w2reu 31756 | Syntax for double restricted existential uniqueness quantification. |
wff β!π₯ β π΄ , π¦ β π΅π | ||
Definition | df-2reu 31757 | Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ (β!π₯ β π΄ , π¦ β π΅π β (β!π₯ β π΄ βπ¦ β π΅ π β§ β!π¦ β π΅ βπ₯ β π΄ π)) | ||
Theorem | 2reucom 31758 | Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ (β!π₯ β π΄ , π¦ β π΅π β β!π¦ β π΅ , π₯ β π΄π) | ||
Theorem | 2reu2rex1 31759 | Double restricted existential uniqueness implies double restricted existence. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ (β!π₯ β π΄ , π¦ β π΅π β βπ₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | 2reureurex 31760 | Double restricted existential uniqueness implies restricted existential uniqueness with restricted existence. (Contributed by AV, 5-Jul-2023.) |
β’ (β!π₯ β π΄ , π¦ β π΅π β β!π₯ β π΄ βπ¦ β π΅ π) | ||
Theorem | 2reu2reu2 31761* | Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023.) |
β’ (β!π₯ β π΄ , π¦ β π΅π β β!π₯ β π΄ β!π¦ β π΅ π) | ||
Theorem | opreu2reu1 31762* | Equivalent definition of the double restricted existential uniqueness quantifier, using uniqueness of ordered pairs. (Contributed by Thierry Arnoux, 4-Jul-2023.) |
β’ (π = β¨π₯, π¦β© β (π β π)) β β’ (β!π₯ β π΄ , π¦ β π΅π β β!π β (π΄ Γ π΅)π) | ||
Theorem | sq2reunnltb 31763* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4π + 1. Double restricted existential uniqueness variant of 2sqreunnltb 26971. (Contributed by AV, 5-Jul-2023.) |
β’ (π β β β ((π mod 4) = 1 β β!π β β , π β β(π < π β§ ((πβ2) + (πβ2)) = π))) | ||
Theorem | addsqnot2reu 31764* | For each complex number πΆ, there does not uniquely exist two complex numbers π and π, with π squared and added to π resulting in the given complex number πΆ. Double restricted existential uniqueness variant of addsqn2reurex2 26955. (Contributed by AV, 5-Jul-2023.) |
β’ (πΆ β β β Β¬ β!π β β , π β β(π + (πβ2)) = πΆ) | ||
Theorem | sbceqbidf 31765 | Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
β’ β²π₯π & β’ (π β π΄ = π΅) & β’ (π β (π β π)) β β’ (π β ([π΄ / π₯]π β [π΅ / π₯]π)) | ||
Theorem | sbcies 31766* | A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.) |
β’ π΄ = (πΈβπ) & β’ (π = π΄ β (π β π)) β β’ (π€ = π β ([(πΈβπ€) / π]π β π)) | ||
Theorem | mo5f 31767* | Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017.) |
β’ β²ππ & β’ β²ππ β β’ (β*π₯π β βπβπ(([π / π₯]π β§ [π / π₯]π) β π = π)) | ||
Theorem | nmo 31768* | Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017.) |
β’ β²π¦π β β’ (Β¬ β*π₯π β βπ¦βπ₯(π β§ π₯ β π¦)) | ||
Theorem | reuxfrdf 31769* | Transfer existential uniqueness from a variable π₯ to another variable π¦ contained in expression π΄. Cf. reuxfrd 3744 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) (Revised by Thierry Arnoux, 30-Mar-2018.) |
β’ β²π¦π΅ & β’ ((π β§ π¦ β πΆ) β π΄ β π΅) & β’ ((π β§ π₯ β π΅) β β*π¦ β πΆ π₯ = π΄) β β’ (π β (β!π₯ β π΅ βπ¦ β πΆ (π₯ = π΄ β§ π) β β!π¦ β πΆ π)) | ||
Theorem | rexunirn 31770* | Restricted existential quantification over the union of the range of a function. Cf. rexrn 7088 and eluni2 4912. (Contributed by Thierry Arnoux, 19-Sep-2017.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π₯ β π΄ β π΅ β π) β β’ (βπ₯ β π΄ βπ¦ β π΅ π β βπ¦ β βͺ ran πΉπ) | ||
Theorem | rmoxfrd 31771* | Transfer "at most one" restricted quantification from a variable π₯ to another variable π¦ contained in expression π΄. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.) |
β’ ((π β§ π¦ β πΆ) β π΄ β π΅) & β’ ((π β§ π₯ β π΅) β β!π¦ β πΆ π₯ = π΄) & β’ ((π β§ π₯ = π΄) β (π β π)) β β’ (π β (β*π₯ β π΅ π β β*π¦ β πΆ π)) | ||
Theorem | rmoun 31772 | "At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ (β*π₯ β (π΄ βͺ π΅)π β (β*π₯ β π΄ π β§ β*π₯ β π΅ π)) | ||
Theorem | rmounid 31773* | A case where an "at most one" restricted existential quantifier for a union is equivalent to such a quantifier for one of the sets. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ ((π β§ π₯ β π΅) β Β¬ π) β β’ (π β (β*π₯ β (π΄ βͺ π΅)π β β*π₯ β π΄ π)) | ||
Theorem | riotaeqbidva 31774* | Equivalent wff's yield equal restricted definition binders (deduction form). (raleqbidva 3327 analog.) (Contributed by Thierry Arnoux, 29-Jan-2025.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΄) β (π β π)) β β’ (π β (β©π₯ β π΄ π) = (β©π₯ β π΅ π)) | ||
Theorem | dmrab 31775* | Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023.) |
β’ (π§ = β¨π₯, π¦β© β (π β π)) β β’ dom {π§ β (π΄ Γ π΅) β£ π} = {π₯ β π΄ β£ βπ¦ β π΅ π} | ||
Theorem | difrab2 31776 | Difference of two restricted class abstractions. Compare with difrab 4308. (Contributed by Thierry Arnoux, 3-Jan-2022.) |
β’ ({π₯ β π΄ β£ π} β {π₯ β π΅ β£ π}) = {π₯ β (π΄ β π΅) β£ π} | ||
Theorem | rabexgfGS 31777 | Separation Scheme in terms of a restricted class abstraction. To be removed in profit of Glauco's equivalent version. (Contributed by Thierry Arnoux, 11-May-2017.) |
β’ β²π₯π΄ β β’ (π΄ β π β {π₯ β π΄ β£ π} β V) | ||
Theorem | rabsnel 31778* | Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
β’ π΅ β V β β’ ({π₯ β π΄ β£ π} = {π΅} β π΅ β π΄) | ||
Theorem | eqrrabd 31779* | Deduce equality with a restricted abstraction. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
β’ (π β π΅ β π΄) & β’ ((π β§ π₯ β π΄) β (π₯ β π΅ β π)) β β’ (π β π΅ = {π₯ β π΄ β£ π}) | ||
Theorem | foresf1o 31780* | From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
β’ ((π΄ β π β§ πΉ:π΄βontoβπ΅) β βπ₯ β π« π΄(πΉ βΎ π₯):π₯β1-1-ontoβπ΅) | ||
Theorem | rabfodom 31781* | Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
β’ ((π β§ π₯ β π΄ β§ π¦ = (πΉβπ₯)) β (π β π)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βontoβπ΅) β β’ (π β {π¦ β π΅ β£ π} βΌ {π₯ β π΄ β£ π}) | ||
Theorem | abrexdomjm 31782* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π¦ β π΄ β β*π₯π) β β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π} βΌ π΄) | ||
Theorem | abrexdom2jm 31783* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π₯ = π΅} βΌ π΄) | ||
Theorem | abrexexd 31784* | Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017.) |
β’ β²π₯π΄ & β’ (π β π΄ β V) β β’ (π β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β V) | ||
Theorem | elabreximd 31785* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
β’ β²π₯π & β’ β²π₯π & β’ (π΄ = π΅ β (π β π)) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β πΆ) β π) β β’ ((π β§ π΄ β {π¦ β£ βπ₯ β πΆ π¦ = π΅}) β π) | ||
Theorem | elabreximdv 31786* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
β’ (π΄ = π΅ β (π β π)) & β’ (π β π΄ β π) & β’ ((π β§ π₯ β πΆ) β π) β β’ ((π β§ π΄ β {π¦ β£ βπ₯ β πΆ π¦ = π΅}) β π) | ||
Theorem | abrexss 31787* | A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
β’ β²π₯πΆ β β’ (βπ₯ β π΄ π΅ β πΆ β {π¦ β£ βπ₯ β π΄ π¦ = π΅} β πΆ) | ||
Theorem | elunsn 31788 | Elementhood to a union with a singleton. (Contributed by Thierry Arnoux, 14-Dec-2023.) |
β’ (π΄ β π β (π΄ β (π΅ βͺ {πΆ}) β (π΄ β π΅ β¨ π΄ = πΆ))) | ||
Theorem | nelun 31789 | Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.) |
β’ (π΄ = (π΅ βͺ πΆ) β (Β¬ π β π΄ β (Β¬ π β π΅ β§ Β¬ π β πΆ))) | ||
Theorem | snsssng 31790 | If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) (Revised by Thierry Arnoux, 11-Apr-2024.) |
β’ ((π΄ β π β§ {π΄} β {π΅}) β π΄ = π΅) | ||
Theorem | inin 31791 | Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
β’ (π΄ β© (π΄ β© π΅)) = (π΄ β© π΅) | ||
Theorem | inindif 31792 | See inundif 4478. (Contributed by Thierry Arnoux, 13-Sep-2017.) |
β’ ((π΄ β© πΆ) β© (π΄ β πΆ)) = β | ||
Theorem | difininv 31793 | Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021.) |
β’ ((((π΄ β πΆ) β© π΅) = β β§ ((πΆ β π΄) β© π΅) = β ) β (π΄ β© π΅) = (πΆ β© π΅)) | ||
Theorem | difeq 31794 | Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
β’ ((π΄ β π΅) = πΆ β ((πΆ β© π΅) = β β§ (πΆ βͺ π΅) = (π΄ βͺ π΅))) | ||
Theorem | eqdif 31795 | If both set differences of two sets are empty, those sets are equal. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ (((π΄ β π΅) = β β§ (π΅ β π΄) = β ) β π΄ = π΅) | ||
Theorem | indifbi 31796 | Two ways to express equality relative to a class π΄. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
β’ ((π΄ β© π΅) = (π΄ β© πΆ) β (π΄ β π΅) = (π΄ β πΆ)) | ||
Theorem | diffib 31797 | Case where diffi 9181 is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024.) |
β’ (π΅ β Fin β (π΄ β Fin β (π΄ β π΅) β Fin)) | ||
Theorem | difxp1ss 31798 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ ((π΄ β πΆ) Γ π΅) β (π΄ Γ π΅) | ||
Theorem | difxp2ss 31799 | Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π΄ Γ (π΅ β πΆ)) β (π΄ Γ π΅) | ||
Theorem | indifundif 31800 | A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020.) |
β’ (((π΄ β© π΅) β πΆ) βͺ (π΄ β π΅)) = (π΄ β (π΅ β© πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |