Theorem List for Intuitionistic Logic Explorer - 3901-4000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | ciin 3901 |
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 3858. 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 3902* |
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 3934. Theorem uniiun 3954 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27-Jun-1998.)
|
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
|
Definition | df-iin 3903* |
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union df-iun 3902. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3935. Theorem intiin 3955 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27-Jun-1998.)
|
⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
|
Theorem | eliun 3904* |
Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
|
⊢ (𝐴 ∈ ∪
𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) |
|
Theorem | eliin 3905* |
Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩
𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
|
Theorem | iuncom 3906* |
Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪
𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iuncom4 3907 |
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18-Jan-2014.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪
∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | iunconstm 3908* |
Indexed union of a constant class, i.e. where 𝐵 does not depend on
𝑥. (Contributed by Jim Kingdon,
15-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∪
𝑥 ∈ 𝐴 𝐵 = 𝐵) |
|
Theorem | iinconstm 3909* |
Indexed intersection of a constant class, i.e. where 𝐵 does not
depend on 𝑥. (Contributed by Jim Kingdon,
19-Dec-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 𝐵 = 𝐵) |
|
Theorem | iuniin 3910* |
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 3911* |
Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iinss1 3912* |
Subclass theorem for indexed union. (Contributed by NM,
24-Jan-2012.)
|
⊢ (𝐴 ⊆ 𝐵 → ∩
𝑥 ∈ 𝐵 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq1 3913* |
Equality theorem for indexed union. (Contributed by NM,
27-Jun-1998.)
|
⊢ (𝐴 = 𝐵 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iineq1 3914* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27-Jun-1998.)
|
⊢ (𝐴 = 𝐵 → ∩
𝑥 ∈ 𝐴 𝐶 = ∩
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ss2iun 3915 |
Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2 3916 |
Equality theorem for indexed union. (Contributed by NM,
22-Oct-2003.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iineq2 3917 |
Equality theorem for indexed intersection. (Contributed by NM,
22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2i 3918 |
Equality inference for indexed union. (Contributed by NM,
22-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iineq2i 3919 |
Equality inference for indexed intersection. (Contributed by NM,
22-Oct-2003.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶 |
|
Theorem | iineq2d 3920 |
Equality deduction for indexed intersection. (Contributed by NM,
7-Dec-2011.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq2dv 3921* |
Equality deduction for indexed union. (Contributed by NM,
3-Aug-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iineq2dv 3922* |
Equality deduction for indexed intersection. (Contributed by NM,
3-Aug-2004.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iuneq1d 3923* |
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22-Oct-2015.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐶) |
|
Theorem | iuneq12d 3924* |
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22-Oct-2015.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐶 = ∪
𝑥 ∈ 𝐵 𝐷) |
|
Theorem | iuneq2d 3925* |
Equality deduction for indexed union. (Contributed by Drahflow,
22-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | nfiunxy 3926* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiinxy 3927* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiunya 3928* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiinya 3929* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfiu1 3930 |
Bound-variable hypothesis builder for indexed union. (Contributed by
NM, 12-Oct-2003.)
|
⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfii1 3931 |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by NM, 15-Oct-2003.)
|
⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
|
Theorem | dfiun2g 3932* |
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 3933* |
Alternate definition of indexed intersection when 𝐵 is a set.
(Contributed by Jeff Hankins, 27-Aug-2009.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
|
Theorem | dfiun2 3934* |
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 3935* |
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 3936* |
Define double indexed union. (Contributed by FL, 6-Nov-2013.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 ∈ 𝐶} |
|
Theorem | cbviun 3937* |
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 3938* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbviunv 3939* |
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 3940* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩
𝑦 ∈ 𝐴 𝐶 |
|
Theorem | iunss 3941* |
Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
|
Theorem | ssiun 3942* |
Subset implication for an indexed union. (Contributed by NM,
3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∃𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | ssiun2 3943 |
Identity law for subset of an indexed union. (Contributed by NM,
12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | ssiun2s 3944* |
Subset relationship for an indexed union. (Contributed by NM,
26-Oct-2003.)
|
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | iunss2 3945* |
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 3854. (Contributed by NM, 9-Dec-2004.)
|
⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 ⊆ 𝐷 → ∪
𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑦 ∈ 𝐵 𝐷) |
|
Theorem | iunssd 3946* |
Subset theorem for an indexed union. (Contributed by Glauco Siliprandi,
8-Apr-2021.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∪
𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
|
Theorem | iunab 3947* |
The indexed union of a class abstraction. (Contributed by NM,
27-Dec-2004.)
|
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
|
Theorem | iunrab 3948* |
The indexed union of a restricted class abstraction. (Contributed by
NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|
⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝐴 𝜑} |
|
Theorem | iunxdif2 3949* |
Indexed union with a class difference as its index. (Contributed by NM,
10-Dec-2004.)
|
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ (𝐴 ∖ 𝐵)𝐶 ⊆ 𝐷 → ∪
𝑦 ∈ (𝐴 ∖ 𝐵)𝐷 = ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ssiinf 3950 |
Subset theorem for an indexed intersection. (Contributed by FL,
15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) |
|
Theorem | ssiin 3951* |
Subset theorem for an indexed intersection. (Contributed by NM,
15-Oct-2003.)
|
⊢ (𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵) |
|
Theorem | iinss 3952* |
Subset implication for an indexed intersection. (Contributed by NM,
15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩
𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
|
Theorem | iinss2 3953 |
An indexed intersection is included in any of its members. (Contributed
by FL, 15-Oct-2012.)
|
⊢ (𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵) |
|
Theorem | uniiun 3954* |
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28-Jun-1998.)
|
⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 |
|
Theorem | intiin 3955* |
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28-Jun-1998.)
|
⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥 |
|
Theorem | iunid 3956* |
An indexed union of singletons recovers the index set. (Contributed by
NM, 6-Sep-2005.)
|
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
|
Theorem | iun0 3957 |
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 3958 |
An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
|
Theorem | 0iin 3959 |
An empty indexed intersection is the universal class. (Contributed by
NM, 20-Oct-2005.)
|
⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V |
|
Theorem | viin 3960* |
Indexed intersection with a universal index class. (Contributed by NM,
11-Sep-2008.)
|
⊢ ∩ 𝑥 ∈ V 𝐴 = {𝑦 ∣ ∀𝑥 𝑦 ∈ 𝐴} |
|
Theorem | iunn0m 3961* |
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 3962* |
Indexed intersection of a class builder. (Contributed by NM,
6-Dec-2011.)
|
⊢ ∩ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝜑} = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝜑} |
|
Theorem | iinrabm 3963* |
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
|
Theorem | iunin2 3964* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3954 to recover
Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iunin1 3965* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3954 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∪
𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) |
|
Theorem | iundif2ss 3966* |
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 3967* |
Rearrange indexed unions over intersection. (Contributed by NM,
18-Dec-2008.)
|
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 (𝐶 ∩ 𝐷) = (∪
𝑥 ∈ 𝐴 𝐶 ∩ ∪
𝑦 ∈ 𝐵 𝐷) |
|
Theorem | iindif2m 3968* |
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 3969* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∩
𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | iinin1m 3970* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∩
𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵) = (∩
𝑥 ∈ 𝐴 𝐶 ∩ 𝐵)) |
|
Theorem | elriin 3971* |
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
⊢ (𝐵 ∈ (𝐴 ∩ ∩
𝑥 ∈ 𝑋 𝑆) ↔ (𝐵 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝑋 𝐵 ∈ 𝑆)) |
|
Theorem | riin0 3972* |
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3-Apr-2015.)
|
⊢ (𝑋 = ∅ → (𝐴 ∩ ∩
𝑥 ∈ 𝑋 𝑆) = 𝐴) |
|
Theorem | riinm 3973* |
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
⊢ ((∀𝑥 ∈ 𝑋 𝑆 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝑋) → (𝐴 ∩ ∩
𝑥 ∈ 𝑋 𝑆) = ∩
𝑥 ∈ 𝑋 𝑆) |
|
Theorem | iinxsng 3974* |
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 3975* |
Indexed intersection with an unordered pair index. (Contributed by NM,
25-Jan-2012.)
|
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)
& ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∩ 𝐸)) |
|
Theorem | iunxsng 3976* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.)
|
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∪
𝑥 ∈ {𝐴}𝐵 = 𝐶) |
|
Theorem | iunxsn 3977* |
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 3978* |
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 3979 |
Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.)
(Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∪ 𝐶) = (∪
𝑥 ∈ 𝐴 𝐵 ∪ ∪
𝑥 ∈ 𝐴 𝐶) |
|
Theorem | iunxun 3980 |
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 3981* |
A pair index picks out two instances of an indexed union's argument.
(Contributed by Alexander van der Vekens, 2-Feb-2018.)
|
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)
& ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ {𝐴, 𝐵}𝐶 = (𝐷 ∪ 𝐸)) |
|
Theorem | iunxiun 3982* |
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵𝐶 = ∪
𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 |
|
Theorem | iinuniss 3983* |
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 3984* |
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 3985 |
Subclass relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵) |
|
Theorem | pwssb 3986* |
Two ways to express a collection of subclasses. (Contributed by NM,
19-Jul-2006.)
|
⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
|
Theorem | elpwpw 3987 |
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 3988* |
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.)
|
⊢ 𝒫 𝒫 𝐴 = {𝑥 ∣ ∪ 𝑥 ⊆ 𝐴} |
|
Theorem | pwpwssunieq 3989* |
The class of sets whose union is equal to a given class is included in
the double power class of that class. (Contributed by BJ,
29-Apr-2021.)
|
⊢ {𝑥 ∣ ∪ 𝑥 = 𝐴} ⊆ 𝒫 𝒫 𝐴 |
|
Theorem | elpwuni 3990 |
Relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
⊢ (𝐵 ∈ 𝐴 → (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 = 𝐵)) |
|
Theorem | iinpw 3991* |
The power class of an intersection in terms of indexed intersection.
Exercise 24(a) of [Enderton] p. 33.
(Contributed by NM,
29-Nov-2003.)
|
⊢ 𝒫 ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝒫 𝑥 |
|
Theorem | iunpwss 3992* |
Inclusion of an indexed union of a power class in the power class of the
union of its index. Part of Exercise 24(b) of [Enderton] p. 33.
(Contributed by NM, 25-Nov-2003.)
|
⊢ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ⊆ 𝒫 ∪ 𝐴 |
|
Theorem | rintm 3993* |
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
⊢ ((𝑋 ⊆ 𝒫 𝐴 ∧ ∃𝑥 𝑥 ∈ 𝑋) → (𝐴 ∩ ∩ 𝑋) = ∩ 𝑋) |
|
2.1.21 Disjointness
|
|
Syntax | wdisj 3994 |
Extend wff notation to include the statement that a family of classes
𝐵(𝑥), for 𝑥 ∈ 𝐴, is a disjoint family.
|
wff Disj 𝑥 ∈ 𝐴 𝐵 |
|
Definition | df-disj 3995* |
A collection of classes 𝐵(𝑥) is disjoint when for each element
𝑦, it is in 𝐵(𝑥) for at most one 𝑥.
(Contributed by
Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.)
|
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
|
Theorem | dfdisj2 3996* |
Alternate definition for disjoint classes. (Contributed by NM,
17-Jun-2017.)
|
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
|
Theorem | disjss2 3997 |
If each element of a collection is contained in a disjoint collection,
the original collection is also disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐶 → Disj 𝑥 ∈ 𝐴 𝐵)) |
|
Theorem | disjeq2 3998 |
Equality theorem for disjoint collection. (Contributed by Mario Carneiro,
14-Nov-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | disjeq2dv 3999* |
Equality deduction for disjoint collection. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) |
|
Theorem | disjss1 4000* |
A subset of a disjoint collection is disjoint. (Contributed by Mario
Carneiro, 14-Nov-2016.)
|
⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) |