Theorem List for Intuitionistic Logic Explorer - 3801-3900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | intsn 3801 |
The intersection of a singleton is its member. Theorem 70 of [Suppes]
p. 41. (Contributed by NM, 29-Sep-2002.)
|
|
|
Theorem | uniintsnr 3802* |
The union and intersection of a singleton are equal. See also eusn 3592.
(Contributed by Jim Kingdon, 14-Aug-2018.)
|
|
|
Theorem | uniintabim 3803 |
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 3804 |
Theorem joining a singleton to an intersection. (Contributed by NM,
29-Sep-2002.)
|
|
|
Theorem | rint0 3805 |
Relative intersection of an empty set. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
|
|
Theorem | elrint 3806* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
|
|
Theorem | elrint2 3807* |
Membership in a restricted intersection. (Contributed by Stefan O'Rear,
3-Apr-2015.)
|
|
|
2.1.20 Indexed union and
intersection
|
|
Syntax | ciun 3808 |
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 3731. 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.
|
|
|
Syntax | ciin 3809 |
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 3766. 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.
|
|
|
Definition | df-iun 3810* |
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 3842. Theorem uniiun 3861 provides
a definition of ordinary union in terms of indexed union. (Contributed
by NM, 27-Jun-1998.)
|
|
|
Definition | df-iin 3811* |
Define indexed intersection. Definition of [Stoll] p. 45. See the
remarks for its sibling operation of indexed union df-iun 3810. An
alternate definition tying indexed intersection to ordinary intersection
is dfiin2 3843. Theorem intiin 3862 provides a definition of ordinary
intersection in terms of indexed intersection. (Contributed by NM,
27-Jun-1998.)
|
|
|
Theorem | eliun 3812* |
Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
|
|
|
Theorem | eliin 3813* |
Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
|
|
|
Theorem | iuncom 3814* |
Commutation of indexed unions. (Contributed by NM, 18-Dec-2008.)
|
|
|
Theorem | iuncom4 3815 |
Commutation of union with indexed union. (Contributed by Mario
Carneiro, 18-Jan-2014.)
|
|
|
Theorem | iunconstm 3816* |
Indexed union of a constant class, i.e. where does not depend on
. (Contributed
by Jim Kingdon, 15-Aug-2018.)
|
|
|
Theorem | iinconstm 3817* |
Indexed intersection of a constant class, i.e. where does not
depend on .
(Contributed by Jim Kingdon, 19-Dec-2018.)
|
|
|
Theorem | iuniin 3818* |
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 3819* |
Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | iinss1 3820* |
Subclass theorem for indexed union. (Contributed by NM,
24-Jan-2012.)
|
|
|
Theorem | iuneq1 3821* |
Equality theorem for indexed union. (Contributed by NM,
27-Jun-1998.)
|
|
|
Theorem | iineq1 3822* |
Equality theorem for restricted existential quantifier. (Contributed by
NM, 27-Jun-1998.)
|
|
|
Theorem | ss2iun 3823 |
Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | iuneq2 3824 |
Equality theorem for indexed union. (Contributed by NM,
22-Oct-2003.)
|
|
|
Theorem | iineq2 3825 |
Equality theorem for indexed intersection. (Contributed by NM,
22-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | iuneq2i 3826 |
Equality inference for indexed union. (Contributed by NM,
22-Oct-2003.)
|
|
|
Theorem | iineq2i 3827 |
Equality inference for indexed intersection. (Contributed by NM,
22-Oct-2003.)
|
|
|
Theorem | iineq2d 3828 |
Equality deduction for indexed intersection. (Contributed by NM,
7-Dec-2011.)
|
|
|
Theorem | iuneq2dv 3829* |
Equality deduction for indexed union. (Contributed by NM,
3-Aug-2004.)
|
|
|
Theorem | iineq2dv 3830* |
Equality deduction for indexed intersection. (Contributed by NM,
3-Aug-2004.)
|
|
|
Theorem | iuneq1d 3831* |
Equality theorem for indexed union, deduction version. (Contributed by
Drahflow, 22-Oct-2015.)
|
|
|
Theorem | iuneq12d 3832* |
Equality deduction for indexed union, deduction version. (Contributed
by Drahflow, 22-Oct-2015.)
|
|
|
Theorem | iuneq2d 3833* |
Equality deduction for indexed union. (Contributed by Drahflow,
22-Oct-2015.)
|
|
|
Theorem | nfiunxy 3834* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiinxy 3835* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiunya 3836* |
Bound-variable hypothesis builder for indexed union. (Contributed by
Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiinya 3837* |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by Mario Carneiro, 25-Jan-2014.)
|
|
|
Theorem | nfiu1 3838 |
Bound-variable hypothesis builder for indexed union. (Contributed by
NM, 12-Oct-2003.)
|
|
|
Theorem | nfii1 3839 |
Bound-variable hypothesis builder for indexed intersection.
(Contributed by NM, 15-Oct-2003.)
|
|
|
Theorem | dfiun2g 3840* |
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 3841* |
Alternate definition of indexed intersection when is a set.
(Contributed by Jeff Hankins, 27-Aug-2009.)
|
|
|
Theorem | dfiun2 3842* |
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.)
|
|
|
Theorem | dfiin2 3843* |
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.)
|
|
|
Theorem | dfiunv2 3844* |
Define double indexed union. (Contributed by FL, 6-Nov-2013.)
|
|
|
Theorem | cbviun 3845* |
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 3846* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | cbviunv 3847* |
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 3848* |
Change bound variables in an indexed intersection. (Contributed by Jeff
Hankins, 26-Aug-2009.)
|
|
|
Theorem | iunss 3849* |
Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ssiun 3850* |
Subset implication for an indexed union. (Contributed by NM,
3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ssiun2 3851 |
Identity law for subset of an indexed union. (Contributed by NM,
12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | ssiun2s 3852* |
Subset relationship for an indexed union. (Contributed by NM,
26-Oct-2003.)
|
|
|
Theorem | iunss2 3853* |
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 3762. (Contributed by NM, 9-Dec-2004.)
|
|
|
Theorem | iunab 3854* |
The indexed union of a class abstraction. (Contributed by NM,
27-Dec-2004.)
|
|
|
Theorem | iunrab 3855* |
The indexed union of a restricted class abstraction. (Contributed by
NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|
|
|
Theorem | iunxdif2 3856* |
Indexed union with a class difference as its index. (Contributed by NM,
10-Dec-2004.)
|
|
|
Theorem | ssiinf 3857 |
Subset theorem for an indexed intersection. (Contributed by FL,
15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
|
|
|
Theorem | ssiin 3858* |
Subset theorem for an indexed intersection. (Contributed by NM,
15-Oct-2003.)
|
|
|
Theorem | iinss 3859* |
Subset implication for an indexed intersection. (Contributed by NM,
15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | iinss2 3860 |
An indexed intersection is included in any of its members. (Contributed
by FL, 15-Oct-2012.)
|
|
|
Theorem | uniiun 3861* |
Class union in terms of indexed union. Definition in [Stoll] p. 43.
(Contributed by NM, 28-Jun-1998.)
|
|
|
Theorem | intiin 3862* |
Class intersection in terms of indexed intersection. Definition in
[Stoll] p. 44. (Contributed by NM,
28-Jun-1998.)
|
|
|
Theorem | iunid 3863* |
An indexed union of singletons recovers the index set. (Contributed by
NM, 6-Sep-2005.)
|
|
|
Theorem | iun0 3864 |
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 3865 |
An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.)
(Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
|
|
Theorem | 0iin 3866 |
An empty indexed intersection is the universal class. (Contributed by
NM, 20-Oct-2005.)
|
|
|
Theorem | viin 3867* |
Indexed intersection with a universal index class. (Contributed by NM,
11-Sep-2008.)
|
|
|
Theorem | iunn0m 3868* |
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 3869* |
Indexed intersection of a class builder. (Contributed by NM,
6-Dec-2011.)
|
|
|
Theorem | iinrabm 3870* |
Indexed intersection of a restricted class builder. (Contributed by Jim
Kingdon, 16-Aug-2018.)
|
|
|
Theorem | iunin2 3871* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3861 to recover
Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
|
|
|
Theorem | iunin1 3872* |
Indexed union of intersection. Generalization of half of theorem
"Distributive laws" in [Enderton] p. 30. Use uniiun 3861 to recover
Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
|
|
|
Theorem | iundif2ss 3873* |
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 3874* |
Rearrange indexed unions over intersection. (Contributed by NM,
18-Dec-2008.)
|
|
|
Theorem | iindif2m 3875* |
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 3876* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
|
|
Theorem | iinin1m 3877* |
Indexed intersection of intersection. Compare to Theorem "Distributive
laws" in [Enderton] p. 30.
(Contributed by Jim Kingdon,
17-Aug-2018.)
|
|
|
Theorem | elriin 3878* |
Elementhood in a relative intersection. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
|
|
Theorem | riin0 3879* |
Relative intersection of an empty family. (Contributed by Stefan
O'Rear, 3-Apr-2015.)
|
|
|
Theorem | riinm 3880* |
Relative intersection of an inhabited family. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
|
|
Theorem | iinxsng 3881* |
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 3882* |
Indexed intersection with an unordered pair index. (Contributed by NM,
25-Jan-2012.)
|
|
|
Theorem | iunxsng 3883* |
A singleton index picks out an instance of an indexed union's argument.
(Contributed by Mario Carneiro, 25-Jun-2016.)
|
|
|
Theorem | iunxsn 3884* |
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.)
|
|
|
Theorem | iunxsngf 3885* |
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 3886 |
Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.)
(Proof shortened by Mario Carneiro, 17-Nov-2016.)
|
|
|
Theorem | iunxun 3887 |
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 3888* |
A pair index picks out two instances of an indexed union's argument.
(Contributed by Alexander van der Vekens, 2-Feb-2018.)
|
|
|
Theorem | iunxiun 3889* |
Separate an indexed union in the index of an indexed union.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
|
|
Theorem | iinuniss 3890* |
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 3891* |
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 3892 |
Subclass relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
|
|
Theorem | pwssb 3893* |
Two ways to express a collection of subclasses. (Contributed by NM,
19-Jul-2006.)
|
|
|
Theorem | elpwpw 3894 |
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.)
|
|
|
Theorem | pwpwab 3895* |
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 3896* |
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 3897 |
Relationship for power class and union. (Contributed by NM,
18-Jul-2006.)
|
|
|
Theorem | iinpw 3898* |
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 3899* |
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 3900* |
Relative intersection of an inhabited class. (Contributed by Jim
Kingdon, 19-Aug-2018.)
|
|