![]() |
Metamath
Proof Explorer Theorem List (p. 49 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-uni 4801* | Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, ∪ {{1, 3}, {1, 8}} = {1, 3, 8} (ex-uni 28211). This is similar to the union of two classes df-un 3886. (Contributed by NM, 23-Aug-1993.) |
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | dfuni2 4802* | Alternate definition of class union. (Contributed by NM, 28-Jun-1998.) |
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | ||
Theorem | eluni 4803* | Membership in class union. (Contributed by NM, 22-May-1994.) |
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | eluni2 4804* | Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.) |
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | elunii 4805 | Membership in class union. (Contributed by NM, 24-Mar-1995.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) | ||
Theorem | nfunid 4806 | Deduction version of nfuni 4807. (Contributed by NM, 18-Feb-2013.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfuni 4807 | Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∪ 𝐴 | ||
Theorem | uniss 4808 | Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | unissi 4809 | Subclass relationship for subclass union. Inference form of uniss 4808. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 | ||
Theorem | unissd 4810 | Subclass relationship for subclass union. Deduction form of uniss 4808. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | unieq 4811 | Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by BJ, 13-Apr-2024.) |
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | unieqOLD 4812 | Obsolete version of unieq 4811 as of 13-Apr-2024. (Contributed by NM, 10-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) 29-Jun-2011.) |
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | unieqi 4813 | Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝐴 = ∪ 𝐵 | ||
Theorem | unieqd 4814 | Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | eluniab 4815* | Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | elunirab 4816* | Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.) |
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | unipr 4817 | The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵) | ||
Theorem | uniprg 4818 | The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)) | ||
Theorem | unisng 4819 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.) |
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) | ||
Theorem | unisn 4820 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ {𝐴} = 𝐴 | ||
Theorem | unisn3 4821* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴) | ||
Theorem | dfnfc2 4822* | An alternative statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) | ||
Theorem | uniun 4823 | The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.) |
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) | ||
Theorem | uniin 4824 | The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 8360 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵) | ||
Theorem | ssuni 4825 | Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) | ||
Theorem | uni0b 4826 | The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.) |
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆ {∅}) | ||
Theorem | uni0c 4827* | The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.) |
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅) | ||
Theorem | uni0 4828 | The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Contributed by NM, 16-Sep-1993.) Remove use of ax-nul 5174. (Revised by Eric Schmidt, 4-Apr-2007.) |
⊢ ∪ ∅ = ∅ | ||
Theorem | csbuni 4829 | Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 22-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | elssuni 4830 | An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | unissel 4831 | Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.) |
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵) | ||
Theorem | unissb 4832* | Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) |
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) | ||
Theorem | uniss2 4833* | A subclass condition on the members of two classes that implies a subclass relation on their unions. Proposition 8.6 of [TakeutiZaring] p. 59. See iunss2 4936 for a generalization to indexed unions. (Contributed by NM, 22-Mar-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | unidif 4834* | If the difference 𝐴 ∖ 𝐵 contains the largest members of 𝐴, then the union of the difference is the union of 𝐴. (Contributed by NM, 22-Mar-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝑥 ⊆ 𝑦 → ∪ (𝐴 ∖ 𝐵) = ∪ 𝐴) | ||
Theorem | ssunieq 4835* | Relationship implying union. (Contributed by NM, 10-Nov-1999.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵) | ||
Theorem | unimax 4836* | Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002.) |
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴) | ||
Theorem | pwuni 4837 | A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) |
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 | ||
Syntax | cint 4838 | Extend class notation to include the intersection of a class. Read: "intersection (of) 𝐴". |
class ∩ 𝐴 | ||
Definition | df-int 4839* | Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44. For example, ∩ {{1, 3}, {1, 8}} = {1}. Compare this with the intersection of two classes, df-in 3888. (Contributed by NM, 18-Aug-1993.) |
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfint2 4840* | Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998.) |
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | ||
Theorem | inteq 4841 | Equality law for intersection. (Contributed by NM, 13-Sep-1999.) |
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | ||
Theorem | inteqi 4842 | Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩ 𝐴 = ∩ 𝐵 | ||
Theorem | inteqd 4843 | Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) | ||
Theorem | elint 4844* | Membership in class intersection. (Contributed by NM, 21-May-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) | ||
Theorem | elint2 4845* | Membership in class intersection. (Contributed by NM, 14-Oct-1999.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | elintg 4846* | Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) | ||
Theorem | elinti 4847 | Membership in class intersection. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶)) | ||
Theorem | nfint 4848 | Bound-variable hypothesis builder for intersection. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∩ 𝐴 | ||
Theorem | elintab 4849* | Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) | ||
Theorem | elintrab 4850* | Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)) | ||
Theorem | elintrabg 4851* | Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | int0 4852 | The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ ∩ ∅ = V | ||
Theorem | intss1 4853 | An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.) |
⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴) | ||
Theorem | ssint 4854* | Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.) |
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) | ||
Theorem | ssintab 4855* | Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥)) | ||
Theorem | ssintub 4856* | Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.) |
⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} | ||
Theorem | ssmin 4857* | Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006.) |
⊢ 𝐴 ⊆ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} | ||
Theorem | intmin 4858* | Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝐴 ∈ 𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} = 𝐴) | ||
Theorem | intss 4859 | Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) | ||
Theorem | intssuni 4860 | The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴) | ||
Theorem | ssintrab 4861* | Subclass of the intersection of a restricted class abstraction. (Contributed by NM, 30-Jan-2015.) |
⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥)) | ||
Theorem | unissint 4862 | If the union of a class is included in its intersection, the class is either the empty set or a singleton (uniintsn 4875). (Contributed by NM, 30-Oct-2010.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∪ 𝐴 ⊆ ∩ 𝐴 ↔ (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴)) | ||
Theorem | intssuni2 4863 | Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | intminss 4864* | Under subset ordering, the intersection of a restricted class abstraction is less than or equal to any of its members. (Contributed by NM, 7-Sep-2013.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐴) | ||
Theorem | intmin2 4865* | Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴 | ||
Theorem | intmin3 4866* | Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝜑} ⊆ 𝐴) | ||
Theorem | intmin4 4867* | Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006.) |
⊢ (𝐴 ⊆ ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | intab 4868* | The intersection of a special case of a class abstraction. 𝑦 may be free in 𝜑 and 𝐴, which can be thought of a 𝜑(𝑦) and 𝐴(𝑦). Typically, abrexex2 7652 or abexssex 7653 can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.) |
⊢ 𝐴 ∈ V & ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V ⇒ ⊢ ∩ {𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} | ||
Theorem | int0el 4869 | The intersection of a class containing the empty set is empty. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅) | ||
Theorem | intun 4870 | The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. (Contributed by NM, 22-Sep-2002.) |
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵) | ||
Theorem | intpr 4871 | The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. (Contributed by NM, 14-Oct-1999.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵) | ||
Theorem | intprg 4872 | The intersection of a pair is the intersection of its members. Closed form of intpr 4871. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵)) | ||
Theorem | intsng 4873 | Intersection of a singleton. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴) | ||
Theorem | intsn 4874 | The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. (Contributed by NM, 29-Sep-2002.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝐴} = 𝐴 | ||
Theorem | uniintsn 4875* | Two ways to express "𝐴 is a singleton." See also en1 8559, en1b 8560, card1 9381, and eusn 4626. (Contributed by NM, 2-Aug-2010.) |
⊢ (∪ 𝐴 = ∩ 𝐴 ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | uniintab 4876 | The union and the intersection of a class abstraction are equal exactly when there is a unique satisfying value of 𝜑(𝑥). (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥𝜑 ↔ ∪ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | intunsn 4877 | Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ∩ (𝐴 ∪ {𝐵}) = (∩ 𝐴 ∩ 𝐵) | ||
Theorem | rint0 4878 | Relative intersection of an empty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴) | ||
Theorem | elrint 4879* | Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) | ||
Theorem | elrint2 4880* | Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) | ||
Syntax | ciun 4881 | Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∪ 𝑥 ∈ 𝐴𝐵, with the same union symbol as cuni 4800. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol ∪ instead of ∪ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change. |
class ∪ 𝑥 ∈ 𝐴 𝐵 | ||
Syntax | ciin 4882 | Extend class notation to include indexed intersection. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∩ 𝑥 ∈ 𝐴𝐵, with the same intersection symbol as cint 4838. Although that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses a distinguished symbol ∩ instead of ∩ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change. |
class ∩ 𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-iun 4883* | Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, 𝐴 is independent of 𝑥 (although this is not required by the definition), and 𝐵 depends on 𝑥 i.e. can be read informally as 𝐵(𝑥). We call 𝑥 the index, 𝐴 the index set, and 𝐵 the indexed set. In most books, 𝑥 ∈ 𝐴 is written as a subscript or underneath a union symbol ∪. We use a special union symbol ∪ to make it easier to distinguish from plain class union. In many theorems, you will see that 𝑥 and 𝐴 are in the same distinct variable group (meaning 𝐴 cannot depend on 𝑥) and that 𝐵 and 𝑥 do not share a distinct variable group (meaning that can be thought of as 𝐵(𝑥) i.e. can be substituted with a class expression containing 𝑥). An alternate definition tying indexed union to ordinary union is dfiun2 4920. Theorem uniiun 4945 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6984 and funiunfv 6985 are useful when 𝐵 is a function. (Contributed by NM, 27-Jun-1998.) |
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | ||
Definition | df-iin 4884* | Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4883. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4921. Theorem intiin 4946 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.) |
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | ||
Theorem | eliun 4885* | Membership in indexed union. (Contributed by NM, 3-Sep-2003.) |
⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) | ||
Theorem | eliin 4886* | Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | eliuni 4887* | Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ 𝐶) → 𝐸 ∈ ∪ 𝑥 ∈ 𝐷 𝐵) | ||
Theorem | iuncom 4888* | Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.) |
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 | ||
Theorem | iuncom4 4889 | Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014.) |
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵 | ||
Theorem | iunconst 4890* | Indexed union of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by NM, 5-Sep-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐵) | ||
Theorem | iinconst 4891* | Indexed intersection of a constant class, i.e. where 𝐵 does not depend on 𝑥. (Contributed by Mario Carneiro, 6-Feb-2015.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐵) | ||
Theorem | iuneqconst 4892* | Indexed union of identical classes. (Contributed by AV, 5-Mar-2024.) |
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶) | ||
Theorem | iuniin 4893* | Law combining indexed union with indexed intersection. Eq. 14 in [KuratowskiMostowski] p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 | ||
Theorem | iinssiun 4894* | An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021.) |
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | iunss1 4895* | Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iinss1 4896* | Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012.) |
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq1 4897* | Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.) |
⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iineq1 4898* | Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998.) |
⊢ (𝐴 = 𝐵 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ss2iun 4899 | Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | iuneq2 4900 | Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |