Theorem List for Intuitionistic Logic Explorer - 3801-3900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | int0el 3801 |
The intersection of a class containing the empty set is empty.
(Contributed by NM, 24-Apr-2004.)
|
⊢ (∅ ∈ 𝐴 → ∩ 𝐴 = ∅) |
|
Theorem | intun 3802 |
The class intersection of the union of two classes. Theorem 78 of
[Suppes] p. 42. (Contributed by NM,
22-Sep-2002.)
|
⊢ ∩ (𝐴 ∪ 𝐵) = (∩ 𝐴 ∩ ∩ 𝐵) |
|
Theorem | intpr 3803 |
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 3804 |
The intersection of a pair is the intersection of its members. Closed
form of intpr 3803. Theorem 71 of [Suppes] p. 42. (Contributed by FL,
27-Apr-2008.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
{𝐴, 𝐵} = (𝐴 ∩ 𝐵)) |
|
Theorem | intsng 3805 |
Intersection of a singleton. (Contributed by Stefan O'Rear,
22-Feb-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴) |
|
Theorem | intsn 3806 |
The intersection of a singleton is its member. Theorem 70 of [Suppes]
p. 41. (Contributed by NM, 29-Sep-2002.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∩
{𝐴} = 𝐴 |
|
Theorem | uniintsnr 3807* |
The union and intersection of a singleton are equal. See also eusn 3597.
(Contributed by Jim Kingdon, 14-Aug-2018.)
|
⊢ (∃𝑥 𝐴 = {𝑥} → ∪ 𝐴 = ∩
𝐴) |
|
Theorem | uniintabim 3808 |
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 3809 |
Theorem joining a singleton to an intersection. (Contributed by NM,
29-Sep-2002.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ ∩
(𝐴 ∪ {𝐵}) = (∩ 𝐴
∩ 𝐵) |
|
Theorem | rint0 3810 |
Relative intersection of an empty set. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩ 𝑋) = 𝐴) |
|
Theorem | elrint 3811* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
⊢ (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) |
|
Theorem | elrint2 3812* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
⊢ (𝑋 ∈ 𝐴 → (𝑋 ∈ (𝐴 ∩ ∩ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ 𝑦)) |
|
2.1.20 Indexed union and
intersection
|
|
Syntax | ciun 3813 |
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 3736. 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 3814 |
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 3771. 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 3815* |
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 disjoint variable group (meaning 𝐴 cannot depend on 𝑥) and
that 𝐵 and 𝑥 do not share a disjoint
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 3847. Theorem uniiun 3866 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27-Jun-1998.)
|
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
|
Definition | df-iin 3816* |
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union df-iun 3815. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3848. Theorem intiin 3867 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27-Jun-1998.)
|
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
|
Theorem | eliun 3817* |
Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
|
⊢ (𝐴 ∈ ∪
𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
|
Theorem | eliin 3818* |
Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩
𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
|
Theorem | iuncom 3819* |
Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪
𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iuncom4 3820 |
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18-Jan-2014.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪
∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | iunconstm 3821* |
Indexed union of a constant class, i.e. where 𝐵 does not depend on
𝑥. (Contributed by Jim Kingdon,
15-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∪
𝑥 ∈ 𝐴 𝐵 = 𝐵) |
|
Theorem | iinconstm 3822* |
Indexed intersection of a constant class, i.e. where 𝐵 does not
depend on 𝑥. (Contributed by Jim Kingdon,
19-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 𝐵 = 𝐵) |
|
Theorem | iuniin 3823* |
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 3824* |
Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iinss1 3825* |
Subclass theorem for indexed union. (Contributed by NM,
24-Jan-2012.)
|
⊢ (𝐴 ⊆ 𝐵 → ∩
𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq1 3826* |
Equality theorem for indexed union. (Contributed by NM,
27-Jun-1998.)
|
⊢ (𝐴 = 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iineq1 3827* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27-Jun-1998.)
|
⊢ (𝐴 = 𝐵 → ∩
𝑥 ∈ 𝐴 𝐶 = ∩
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ss2iun 3828 |
Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2 3829 |
Equality theorem for indexed union. (Contributed by NM,
22-Oct-2003.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iineq2 3830 |
Equality theorem for indexed intersection. (Contributed by NM,
22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2i 3831 |
Equality inference for indexed union. (Contributed by NM,
22-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iineq2i 3832 |
Equality inference for indexed intersection. (Contributed by NM,
22-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iineq2d 3833 |
Equality deduction for indexed intersection. (Contributed by NM,
7-Dec-2011.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2dv 3834* |
Equality deduction for indexed union. (Contributed by NM,
3-Aug-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iineq2dv 3835* |
Equality deduction for indexed intersection. (Contributed by NM,
3-Aug-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq1d 3836* |
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22-Oct-2015.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iuneq12d 3837* |
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22-Oct-2015.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐷) |
|
Theorem | iuneq2d 3838* |
Equality deduction for indexed union. (Contributed by Drahflow,
22-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | nfiunxy 3839* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiinxy 3840* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiunya 3841* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiinya 3842* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiu1 3843 |
Bound-variable hypothesis builder for indexed union. (Contributed by
NM, 12-Oct-2003.)
|
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfii1 3844 |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by NM, 15-Oct-2003.)
|
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | dfiun2g 3845* |
Alternate definition of indexed union when 𝐵 is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 23-Mar-2006.) (Proof
shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
|
Theorem | dfiin2g 3846* |
Alternate definition of indexed intersection when 𝐵 is a set.
(Contributed by Jeff Hankins, 27-Aug-2009.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
|
Theorem | dfiun2 3847* |
Alternate definition of indexed union when 𝐵 is a set. Definition
15(a) of [Suppes] p. 44. (Contributed by
NM, 27-Jun-1998.) (Revised by
David Abernethy, 19-Jun-2012.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
|
Theorem | dfiin2 3848* |
Alternate definition of indexed intersection when 𝐵 is a set.
Definition 15(b) of [Suppes] p. 44.
(Contributed by NM, 28-Jun-1998.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
|
Theorem | dfiunv2 3849* |
Define double indexed union. (Contributed by FL, 6-Nov-2013.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶} |
|
Theorem | cbviun 3850* |
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbviin 3851* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbviunv 3852* |
Rule used to change the bound variables in an indexed union, with the
substitution specified implicitly by the hypothesis. (Contributed by
NM, 15-Sep-2003.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbviinv 3853* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑦 ∈ 𝐴 𝐶 |
|
Theorem | iunss 3854* |
Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
|
Theorem | ssiun 3855* |
Subset implication for an indexed union. (Contributed by NM,
3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | ssiun2 3856 |
Identity law for subset of an indexed union. (Contributed by NM,
12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | ssiun2s 3857* |
Subset relationship for an indexed union. (Contributed by NM,
26-Oct-2003.)
|
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | iunss2 3858* |
A subclass condition on the members of two indexed classes 𝐶(𝑥)
and 𝐷(𝑦) that implies a subclass relation on
their indexed
unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59.
Compare uniss2 3767. (Contributed by NM, 9-Dec-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 ⊆ 𝐷 → ∪
𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ 𝐵 𝐷) |
|
Theorem | iunab 3859* |
The indexed union of a class abstraction. (Contributed by NM,
27-Dec-2004.)
|
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
|
Theorem | iunrab 3860* |
The indexed union of a restricted class abstraction. (Contributed by
NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
|
Theorem | iunxdif2 3861* |
Indexed union with a class difference as its index. (Contributed by NM,
10-Dec-2004.)
|
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝐶 ⊆ 𝐷 → ∪
𝑦 ∈ (𝐴 ∖ 𝐵)𝐷 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ssiinf 3862 |
Subset theorem for an indexed intersection. (Contributed by FL,
15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) |
|
Theorem | ssiin 3863* |
Subset theorem for an indexed intersection. (Contributed by NM,
15-Oct-2003.)
|
⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) |
|
Theorem | iinss 3864* |
Subset implication for an indexed intersection. (Contributed by NM,
15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
|
Theorem | iinss2 3865 |
An indexed intersection is included in any of its members. (Contributed
by FL, 15-Oct-2012.)
|
⊢ (𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵) |
|
Theorem | uniiun 3866* |
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28-Jun-1998.)
|
⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 |
|
Theorem | intiin 3867* |
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28-Jun-1998.)
|
⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥 |
|
Theorem | iunid 3868* |
An indexed union of singletons recovers the index set. (Contributed by
NM, 6-Sep-2005.)
|
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
|
Theorem | iun0 3869 |
An indexed union of the empty set is empty. (Contributed by NM,
26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅ |
|
Theorem | 0iun 3870 |
An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
|
Theorem | 0iin 3871 |
An empty indexed intersection is the universal class. (Contributed by
NM, 20-Oct-2005.)
|
⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V |
|
Theorem | viin 3872* |
Indexed intersection with a universal index class. (Contributed by NM,
11-Sep-2008.)
|
⊢ ∩ 𝑥 ∈ V 𝐴 = {𝑦 ∣ ∀𝑥 𝑦 ∈ 𝐴} |
|
Theorem | iunn0m 3873* |
There is an inhabited class in an indexed collection 𝐵(𝑥) iff the
indexed union of them is inhabited. (Contributed by Jim Kingdon,
16-Aug-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ 𝐵 ↔ ∃𝑦 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
|
Theorem | iinab 3874* |
Indexed intersection of a class builder. (Contributed by NM,
6-Dec-2011.)
|
⊢ ∩ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝜑} |
|
Theorem | iinrabm 3875* |
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
|
Theorem | iunin2 3876* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3866 to recover
Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iunin1 3877* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3866 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪
𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) |
|
Theorem | iundif2ss 3878* |
Indexed union of class difference. Compare to theorem "De Morgan's
laws" in [Enderton] p. 31.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) ⊆ (𝐵 ∖ ∩ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | 2iunin 3879* |
Rearrange indexed unions over intersection. (Contributed by NM,
18-Dec-2008.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪
𝑥 ∈ 𝐴 𝐶 ∩ ∪
𝑦 ∈ 𝐵 𝐷) |
|
Theorem | iindif2m 3880* |
Indexed intersection of class difference. Compare to Theorem "De
Morgan's laws" in [Enderton] p.
31. (Contributed by Jim Kingdon,
17-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | iinin2m 3881* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩
𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | iinin1m 3882* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩
𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)) |
|
Theorem | elriin 3883* |
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
⊢ (𝐵 ∈ (𝐴 ∩ ∩
𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆)) |
|
Theorem | riin0 3884* |
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3-Apr-2015.)
|
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩
𝑥 ∈ 𝑋 𝑆) = 𝐴) |
|
Theorem | riinm 3885* |
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝑋) → (𝐴 ∩ ∩
𝑥 ∈ 𝑋 𝑆) = ∩
𝑥 ∈ 𝑋 𝑆) |
|
Theorem | iinxsng 3886* |
A singleton index picks out an instance of an indexed intersection's
argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario
Carneiro, 17-Nov-2016.)
|
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∩
𝑥 ∈ {𝐴}𝐵 = 𝐶) |
|
Theorem | iinxprg 3887* |
Indexed intersection with an unordered pair index. (Contributed by NM,
25-Jan-2012.)
|
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)
& ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸)) |
|
Theorem | iunxsng 3888* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.)
|
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪
𝑥 ∈ {𝐴}𝐵 = 𝐶) |
|
Theorem | iunxsn 3889* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro,
25-Jun-2016.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 |
|
Theorem | iunxsngf 3890* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.) (Revised by Thierry
Arnoux, 2-May-2020.)
|
⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪
𝑥 ∈ {𝐴}𝐵 = 𝐶) |
|
Theorem | iunun 3891 |
Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.)
(Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪
𝑥 ∈ 𝐴 𝐵 ∪ ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iunxun 3892 |
Separate a union in the index of an indexed union. (Contributed by NM,
26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪
𝑥 ∈ 𝐴 𝐶 ∪ ∪
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iunxprg 3893* |
A pair index picks out two instances of an indexed union's argument.
(Contributed by Alexander van der Vekens, 2-Feb-2018.)
|
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)
& ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸)) |
|
Theorem | iunxiun 3894* |
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪
𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 |
|
Theorem | iinuniss 3895* |
A relationship involving union and indexed intersection. Exercise 23 of
[Enderton] p. 33 but with equality
changed to subset. (Contributed by
Jim Kingdon, 19-Aug-2018.)
|
⊢ (𝐴 ∪ ∩ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) |
|
Theorem | iununir 3896* |
A relationship involving union and indexed union. Exercise 25 of
[Enderton] p. 33 but with biconditional
changed to implication.
(Contributed by Jim Kingdon, 19-Aug-2018.)
|
⊢ ((𝐴 ∪ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) → (𝐵 = ∅ → 𝐴 = ∅)) |
|
Theorem | sspwuni 3897 |
Subclass relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
|
Theorem | pwssb 3898* |
Two ways to express a collection of subclasses. (Contributed by NM,
19-Jul-2006.)
|
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
|
Theorem | elpwpw 3899 |
Characterization of the elements of a double power class: they are exactly
the sets whose union is included in that class. (Contributed by BJ,
29-Apr-2021.)
|
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ ∪ 𝐴
⊆ 𝐵)) |
|
Theorem | pwpwab 3900* |
The double power class written as a class abstraction: the class of sets
whose union is included in the given class. (Contributed by BJ,
29-Apr-2021.)
|
⊢ 𝒫 𝒫 𝐴 = {𝑥 ∣ ∪ 𝑥 ⊆ 𝐴} |