Theorem List for Intuitionistic Logic Explorer - 3601-3700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
2.1.18 The union of a class
|
|
Syntax | cuni 3601 |
Extend class notation to include the union of a class (read: 'union
𝐴')
|
class ∪ 𝐴 |
|
Definition | df-uni 3602* |
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 } . This is similar to
the union of two classes df-un 2977. (Contributed by NM, 23-Aug-1993.)
|
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} |
|
Theorem | dfuni2 3603* |
Alternate definition of class union. (Contributed by NM,
28-Jun-1998.)
|
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} |
|
Theorem | eluni 3604* |
Membership in class union. (Contributed by NM, 22-May-1994.)
|
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) |
|
Theorem | eluni2 3605* |
Membership in class union. Restricted quantifier version. (Contributed
by NM, 31-Aug-1999.)
|
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
|
Theorem | elunii 3606 |
Membership in class union. (Contributed by NM, 24-Mar-1995.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) |
|
Theorem | nfuni 3607 |
Bound-variable hypothesis builder for union. (Contributed by NM,
30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∪
𝐴 |
|
Theorem | nfunid 3608 |
Deduction version of nfuni 3607. (Contributed by NM, 18-Feb-2013.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) |
|
Theorem | csbunig 3609 |
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪
𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | unieq 3610 |
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.)
|
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪
𝐵) |
|
Theorem | unieqi 3611 |
Inference of equality of two class unions. (Contributed by NM,
30-Aug-1993.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪
𝐴 = ∪ 𝐵 |
|
Theorem | unieqd 3612 |
Deduction of equality of two class unions. (Contributed by NM,
21-Apr-1995.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 = ∪
𝐵) |
|
Theorem | eluniab 3613* |
Membership in union of a class abstraction. (Contributed by NM,
11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
|
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) |
|
Theorem | elunirab 3614* |
Membership in union of a class abstraction. (Contributed by NM,
4-Oct-2006.)
|
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑)) |
|
Theorem | unipr 3615 |
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 3616 |
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 | unisn 3617 |
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 30-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∪
{𝐴} = 𝐴 |
|
Theorem | unisng 3618 |
A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53.
(Contributed by NM, 13-Aug-2002.)
|
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
|
Theorem | dfnfc2 3619* |
An alternate statement of the effective freeness of a class 𝐴, when
it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
|
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) |
|
Theorem | uniun 3620 |
The class union of the union of two classes. Theorem 8.3 of [Quine]
p. 53. (Contributed by NM, 20-Aug-1993.)
|
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) |
|
Theorem | uniin 3621 |
The class union of the intersection of two classes. Exercise 4.12(n) of
[Mendelson] p. 235. (Contributed by
NM, 4-Dec-2003.) (Proof shortened
by Andrew Salmon, 29-Jun-2011.)
|
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪
𝐴 ∩ ∪ 𝐵) |
|
Theorem | uniss 3622 |
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 | ssuni 3623 |
Subclass relationship for class union. (Contributed by NM,
24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) |
|
Theorem | unissi 3624 |
Subclass relationship for subclass union. Inference form of uniss 3622.
(Contributed by David Moews, 1-May-2017.)
|
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ∪
𝐴 ⊆ ∪ 𝐵 |
|
Theorem | unissd 3625 |
Subclass relationship for subclass union. Deduction form of uniss 3622.
(Contributed by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | uni0b 3626 |
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 3627* |
The union of a set is empty iff all of its members are empty.
(Contributed by NM, 16-Aug-2006.)
|
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅) |
|
Theorem | uni0 3628 |
The union of the empty set is the empty set. Theorem 8.7 of [Quine]
p. 54. (Reproved without relying on ax-nul by Eric Schmidt.)
(Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt,
4-Apr-2007.)
|
⊢ ∪ ∅ =
∅ |
|
Theorem | elssuni 3629 |
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 3630 |
Condition turning a subclass relationship for union into an equality.
(Contributed by NM, 18-Jul-2006.)
|
⊢ ((∪ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐴) → ∪ 𝐴 = 𝐵) |
|
Theorem | unissb 3631* |
Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse.
(Contributed by NM, 20-Sep-2003.)
|
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
|
Theorem | uniss2 3632* |
A subclass condition on the members of two classes that implies a
subclass relation on their unions. Proposition 8.6 of [TakeutiZaring]
p. 59. (Contributed by NM, 22-Mar-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∪ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | unidif 3633* |
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 3634* |
Relationship implying union. (Contributed by NM, 10-Nov-1999.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝑥 ⊆ 𝐴) → 𝐴 = ∪ 𝐵) |
|
Theorem | unimax 3635* |
Any member of a class is the largest of those members that it includes.
(Contributed by NM, 13-Aug-2002.)
|
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴} = 𝐴) |
|
2.1.19 The intersection of a class
|
|
Syntax | cint 3636 |
Extend class notation to include the intersection of a class (read:
'intersect 𝐴').
|
class ∩ 𝐴 |
|
Definition | df-int 3637* |
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 2979.
(Contributed by NM, 18-Aug-1993.)
|
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)} |
|
Theorem | dfint2 3638* |
Alternate definition of class intersection. (Contributed by NM,
28-Jun-1998.)
|
⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} |
|
Theorem | inteq 3639 |
Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
|
⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩
𝐵) |
|
Theorem | inteqi 3640 |
Equality inference for class intersection. (Contributed by NM,
2-Sep-2003.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩
𝐴 = ∩ 𝐵 |
|
Theorem | inteqd 3641 |
Equality deduction for class intersection. (Contributed by NM,
2-Sep-2003.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝐴 = ∩
𝐵) |
|
Theorem | elint 3642* |
Membership in class intersection. (Contributed by NM, 21-May-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) |
|
Theorem | elint2 3643* |
Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
|
Theorem | elintg 3644* |
Membership in class intersection, with the sethood requirement expressed
as an antecedent. (Contributed by NM, 20-Nov-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
|
Theorem | elinti 3645 |
Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
(Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝐴 ∈ ∩ 𝐵 → (𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶)) |
|
Theorem | nfint 3646 |
Bound-variable hypothesis builder for intersection. (Contributed by NM,
2-Feb-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∩
𝐴 |
|
Theorem | elintab 3647* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 30-Aug-1993.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
|
Theorem | elintrab 3648* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 17-Oct-1999.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥)) |
|
Theorem | elintrabg 3649* |
Membership in the intersection of a class abstraction. (Contributed by
NM, 17-Feb-2007.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ∈ 𝑥))) |
|
Theorem | int0 3650 |
The intersection of the empty set is the universal class. Exercise 2 of
[TakeutiZaring] p. 44.
(Contributed by NM, 18-Aug-1993.)
|
⊢ ∩ ∅ =
V |
|
Theorem | intss1 3651 |
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 3652* |
Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52
and its converse. (Contributed by NM, 14-Oct-1999.)
|
⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥) |
|
Theorem | ssintab 3653* |
Subclass of the intersection of a class abstraction. (Contributed by
NM, 31-Jul-2006.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
⊢ (𝐴 ⊆ ∩
{𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ⊆ 𝑥)) |
|
Theorem | ssintub 3654* |
Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)
|
⊢ 𝐴 ⊆ ∩
{𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} |
|
Theorem | ssmin 3655* |
Subclass of the minimum value of class of supersets. (Contributed by
NM, 10-Aug-2006.)
|
⊢ 𝐴 ⊆ ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} |
|
Theorem | intmin 3656* |
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 3657 |
Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
|
⊢ (𝐴 ⊆ 𝐵 → ∩ 𝐵 ⊆ ∩ 𝐴) |
|
Theorem | intssunim 3658* |
The intersection of an inhabited set is a subclass of its union.
(Contributed by NM, 29-Jul-2006.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ ∪ 𝐴) |
|
Theorem | ssintrab 3659* |
Subclass of the intersection of a restricted class builder.
(Contributed by NM, 30-Jan-2015.)
|
⊢ (𝐴 ⊆ ∩
{𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐵 (𝜑 → 𝐴 ⊆ 𝑥)) |
|
Theorem | intssuni2m 3660* |
Subclass relationship for intersection and union. (Contributed by Jim
Kingdon, 14-Aug-2018.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | intminss 3661* |
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 3662* |
Any set is the smallest of all sets that include it. (Contributed by
NM, 20-Sep-2003.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∩
{𝑥 ∣ 𝐴 ⊆ 𝑥} = 𝐴 |
|
Theorem | intmin3 3663* |
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 3664* |
Elimination of a conjunct in a class intersection. (Contributed by NM,
31-Jul-2006.)
|
⊢ (𝐴 ⊆ ∩
{𝑥 ∣ 𝜑} → ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑}) |
|
Theorem | intab 3665* |
The intersection of a special case of a class abstraction. 𝑦 may be
free in 𝜑 and 𝐴, which can be thought of
a 𝜑(𝑦) and
𝐴(𝑦). (Contributed by NM, 28-Jul-2006.)
(Proof shortened by
Mario Carneiro, 14-Nov-2016.)
|
⊢ 𝐴 ∈ V & ⊢ {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} ∈ V ⇒ ⊢ ∩
{𝑥 ∣ ∀𝑦(𝜑 → 𝐴 ∈ 𝑥)} = {𝑥 ∣ ∃𝑦(𝜑 ∧ 𝑥 = 𝐴)} |
|
Theorem | int0el 3666 |
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24-Apr-2004.)
|
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅) |
|
Theorem | intun 3667 |
The class intersection of the union of two classes. Theorem 78 of
[Suppes] p. 42. (Contributed by NM,
22-Sep-2002.)
|
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵) |
|
Theorem | intpr 3668 |
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 3669 |
The intersection of a pair is the intersection of its members. Closed
form of intpr 3668. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27-Apr-2008.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
{𝐴, 𝐵} = (𝐴 ∩ 𝐵)) |
|
Theorem | intsng 3670 |
Intersection of a singleton. (Contributed by Stefan O'Rear,
22-Feb-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴) |
|
Theorem | intsn 3671 |
The intersection of a singleton is its member. Theorem 70 of [Suppes]
p. 41. (Contributed by NM, 29-Sep-2002.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∩
{𝐴} = 𝐴 |
|
Theorem | uniintsnr 3672* |
The union and intersection of a singleton are equal. See also eusn 3466.
(Contributed by Jim Kingdon, 14-Aug-2018.)
|
⊢ (∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) |
|
Theorem | uniintabim 3673 |
The union and the intersection of a class abstraction are equal if there
is a unique satisfying value of 𝜑(𝑥). (Contributed by Jim
Kingdon, 14-Aug-2018.)
|
⊢ (∃!𝑥𝜑 → ∪ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) |
|
Theorem | intunsn 3674 |
Theorem joining a singleton to an intersection. (Contributed by NM,
29-Sep-2002.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ ∩
(𝐴 ∪ {𝐵}) = (∩ 𝐴
∩ 𝐵) |
|
Theorem | rint0 3675 |
Relative intersection of an empty set. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴) |
|
Theorem | elrint 3676* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) |
|
Theorem | elrint2 3677* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) |
|
2.1.20 Indexed union and
intersection
|
|
Syntax | ciun 3678 |
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 3601. While that syntax was unambiguous, it
did not allow for LALR parsing of the syntax constructions in set.mm. The
new syntax uses as distinguished symbol ∪ instead of ∪ and does
allow LALR parsing. Thanks to Peter Backes for suggesting this change.
|
class ∪ 𝑥 ∈ 𝐴 𝐵 |
|
Syntax | ciin 3679 |
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 3636. 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 3680* |
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 3712. Theorem uniiun 3731 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27-Jun-1998.)
|
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
|
Definition | df-iin 3681* |
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union df-iun 3680. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3713. Theorem intiin 3732 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27-Jun-1998.)
|
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
|
Theorem | eliun 3682* |
Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
|
⊢ (𝐴 ∈ ∪
𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
|
Theorem | eliin 3683* |
Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩
𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
|
Theorem | iuncom 3684* |
Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪
𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iuncom4 3685 |
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18-Jan-2014.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪
∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | iunconstm 3686* |
Indexed union of a constant class, i.e. where 𝐵 does not depend on
𝑥. (Contributed by Jim Kingdon,
15-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∪
𝑥 ∈ 𝐴 𝐵 = 𝐵) |
|
Theorem | iinconstm 3687* |
Indexed intersection of a constant class, i.e. where 𝐵 does not
depend on 𝑥. (Contributed by Jim Kingdon,
19-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 𝐵 = 𝐵) |
|
Theorem | iuniin 3688* |
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 | iunss1 3689* |
Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iinss1 3690* |
Subclass theorem for indexed union. (Contributed by NM,
24-Jan-2012.)
|
⊢ (𝐴 ⊆ 𝐵 → ∩
𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq1 3691* |
Equality theorem for indexed union. (Contributed by NM,
27-Jun-1998.)
|
⊢ (𝐴 = 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iineq1 3692* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27-Jun-1998.)
|
⊢ (𝐴 = 𝐵 → ∩
𝑥 ∈ 𝐴 𝐶 = ∩
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ss2iun 3693 |
Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2 3694 |
Equality theorem for indexed union. (Contributed by NM,
22-Oct-2003.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iineq2 3695 |
Equality theorem for indexed intersection. (Contributed by NM,
22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2i 3696 |
Equality inference for indexed union. (Contributed by NM,
22-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iineq2i 3697 |
Equality inference for indexed intersection. (Contributed by NM,
22-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iineq2d 3698 |
Equality deduction for indexed intersection. (Contributed by NM,
7-Dec-2011.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2dv 3699* |
Equality deduction for indexed union. (Contributed by NM,
3-Aug-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iineq2dv 3700* |
Equality deduction for indexed intersection. (Contributed by NM,
3-Aug-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |