Date  Label  Description 
Theorem 

17Mar2023  finct 6848 
A finite set is countable. (Contributed by Jim Kingdon,
17Mar2023.)

⊔ 

16Mar2023  ctmlemr 6844 
Lemma for ctm 6845. One of the directions of the biconditional.
(Contributed by Jim Kingdon, 16Mar2023.)

⊔ 

15Mar2023  caseinl 6836 
Applying the "case" construction to a left injection. (Contributed
by
Jim Kingdon, 15Mar2023.)

case inl


13Mar2023  enumct 6847 
A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen],
p. 73 (except that our definition of countable does not require the set
to be inhabited). "Finitely enumerable" is defined as
per Definition 8.1.4 of
[AczelRathjen], p. 71 and
"countable" is defined as
⊔
per [BauerSwan], p. 14:3.
(Contributed by Jim Kingdon, 13Mar2023.)

⊔ 

13Mar2023  enumctlemm 6846 
Lemma for enumct 6847. The case where is greater than zero.
(Contributed by Jim Kingdon, 13Mar2023.)



13Mar2023  ctm 6845 
Two equivalent definitions of countable for an inhabited set. Remark of
[BauerSwan], p. 14:3. (Contributed by
Jim Kingdon, 13Mar2023.)

⊔ 

13Mar2023  0ct 6843 
The empty set is countable. Remark of [BauerSwan], p. 14:3 which also
has the definition of countable used here. (Contributed by Jim Kingdon,
13Mar2023.)

⊔ 

13Mar2023  ctex 6524 
A class dominated by is a set. (Contributed by Thierry Arnoux,
29Dec2016.) (Proof shortened by Jim Kingdon, 13Mar2023.)



12Mar2023  cls0 11894 
The closure of the empty set. (Contributed by NM, 2Oct2007.) (Proof
shortened by Jim Kingdon, 12Mar2023.)



12Mar2023  algrp1 11367 
The value of the algorithm iterator at .
(Contributed by Paul Chapman, 31Mar2011.) (Revised by Jim Kingdon,
12Mar2023.)



12Mar2023  ialgr0 11365 
The value of the algorithm iterator at is the
initial state
. (Contributed
by Paul Chapman, 31Mar2011.) (Revised by Jim
Kingdon, 12Mar2023.)



11Mar2023  ntreq0 11893 
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3Oct2007.) (Revised by Jim Kingdon, 11Mar2023.)



11Mar2023  clstop 11888 
The closure of a topology's underlying set is the entire set.
(Contributed by NM, 5Oct2007.) (Proof shortened by Jim Kingdon,
11Mar2023.)



11Mar2023  ntrss 11880 
Subset relationship for interior. (Contributed by NM, 3Oct2007.)
(Revised by Jim Kingdon, 11Mar2023.)



10Mar2023  iuncld 11876 
A finite indexed union of closed sets is closed. (Contributed by Mario
Carneiro, 19Sep2015.) (Revised by Jim Kingdon, 10Mar2023.)



5Mar2023  2basgeng 11843 
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8May2007.) (Revised by Jim Kingdon,
5Mar2023.)



5Mar2023  exmidsssn 4040 
Excluded middle is equivalent to the biconditionalized version of
sssnr 3603 for sets. (Contributed by Jim Kingdon,
5Mar2023.)

EXMID


5Mar2023  exmidn0m 4039 
Excluded middle is equivalent to any set being empty or inhabited.
(Contributed by Jim Kingdon, 5Mar2023.)

EXMID 

4Mar2023  eltg3 11818 
Membership in a topology generated by a basis. (Contributed by NM,
15Jul2006.) (Revised by Jim Kingdon, 4Mar2023.)



4Mar2023  tgvalex 11811 
The topology generated by a basis is a set. (Contributed by Jim
Kingdon, 4Mar2023.)



16Feb2023  ixp0 6502 
The infinite Cartesian product of a family with an empty
member is empty. (Contributed by NM, 1Oct2006.) (Revised by Jim
Kingdon, 16Feb2023.)



16Feb2023  ixpm 6501 
If an infinite Cartesian product of a family is inhabited,
every is inhabited. (Contributed by Mario Carneiro,
22Jun2016.) (Revised by Jim Kingdon, 16Feb2023.)



16Feb2023  exmidundifim 4044 
Excluded middle is equivalent to every subset having a complement.
Variation of exmidundif 4043 with an implication rather than a
biconditional. (Contributed by Jim Kingdon, 16Feb2023.)

EXMID


15Feb2023  ixpintm 6496 
The intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 3Feb2015.) (Revised by Jim Kingdon,
15Feb2023.)



15Feb2023  ixpiinm 6495 
The indexed intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 6Feb2015.) (Revised by Jim Kingdon,
15Feb2023.)



15Feb2023  ixpexgg 6493 
The existence of an infinite Cartesian product. is normally a
freevariable parameter in . Remark in Enderton p. 54.
(Contributed by NM, 28Sep2006.) (Revised by Jim Kingdon,
15Feb2023.)



15Feb2023  nfixpxy 6488 
Boundvariable hypothesis builder for indexed Cartesian product.
(Contributed by Mario Carneiro, 15Oct2016.) (Revised by Jim Kingdon,
15Feb2023.)



13Feb2023  topnpropgd 11727 
The topology extractor function depends only on the base and topology
components. (Contributed by NM, 18Jul2006.) (Revised by Jim Kingdon,
13Feb2023.)

TopSet TopSet 

12Feb2023  slotex 11582 
Existence of slot value. A corollary of slotslfn 11581. (Contributed by
Jim Kingdon, 12Feb2023.)

Slot


11Feb2023  topnvalg 11725 
Value of the topology extractor function. (Contributed by Mario
Carneiro, 13Aug2015.) (Revised by Jim Kingdon, 11Feb2023.)

TopSet
↾_{t} 

10Feb2023  slotslfn 11581 
A slot is a function on sets, treated as structures. (Contributed by
Mario Carneiro, 22Sep2015.) (Revised by Jim Kingdon, 10Feb2023.)

Slot 

9Feb2023  pleslid 11712 
Slot property of .
(Contributed by Jim Kingdon, 9Feb2023.)

Slot 

9Feb2023  topgrptsetd 11709 
The topology of a constructed topological group. (Contributed by Mario
Carneiro, 29Aug2015.) (Revised by Jim Kingdon, 9Feb2023.)

TopSet
TopSet 

9Feb2023  topgrpplusgd 11708 
The additive operation of a constructed topological group. (Contributed
by Mario Carneiro, 29Aug2015.) (Revised by Jim Kingdon,
9Feb2023.)

TopSet


9Feb2023  topgrpbasd 11707 
The base set of a constructed topological group. (Contributed by Mario
Carneiro, 29Aug2015.) (Revised by Jim Kingdon, 9Feb2023.)

TopSet


9Feb2023  topgrpstrd 11706 
A constructed topological group is a structure. (Contributed by Mario
Carneiro, 29Aug2015.) (Revised by Jim Kingdon, 9Feb2023.)

TopSet
Struct 

9Feb2023  tsetslid 11705 
Slot property of TopSet. (Contributed by Jim Kingdon,
9Feb2023.)

TopSet Slot
TopSet TopSet


8Feb2023  ipsipd 11702 
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon,
8Feb2023.)

Scalar


8Feb2023  ipsvscad 11701 
The scalar product operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon,
8Feb2023.)

Scalar


8Feb2023  ipsscad 11700 
The set of scalars of a constructed inner product space. (Contributed
by Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon,
8Feb2023.)

Scalar
Scalar 

7Feb2023  ipsmulrd 11699 
The multiplicative operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon,
7Feb2023.)

Scalar


7Feb2023  ipsaddgd 11698 
The additive operation of a constructed inner product space.
(Contributed by Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon,
7Feb2023.)

Scalar


7Feb2023  ipsbased 11697 
The base set of a constructed inner product space. (Contributed by
Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon, 7Feb2023.)

Scalar


7Feb2023  ipsstrd 11696 
A constructed inner product space is a structure. (Contributed by
Stefan O'Rear, 27Nov2014.) (Revised by Jim Kingdon, 7Feb2023.)

Scalar
Struct 

7Feb2023  ipslid 11695 
Slot property of .
(Contributed by Jim Kingdon, 7Feb2023.)

Slot 

7Feb2023  lmodvscad 11692 
The scalar product operation of a constructed left vector space.
(Contributed by Mario Carneiro, 2Oct2013.) (Revised by Jim Kingdon,
7Feb2023.)

Scalar


6Feb2023  lmodscad 11691 
The set of scalars of a constructed left vector space. (Contributed by
Mario Carneiro, 2Oct2013.) (Revised by Jim Kingdon, 6Feb2023.)

Scalar
Scalar 

6Feb2023  lmodplusgd 11690 
The additive operation of a constructed left vector space. (Contributed
by Mario Carneiro, 2Oct2013.) (Revised by Jim Kingdon,
6Feb2023.)

Scalar


6Feb2023  lmodbased 11689 
The base set of a constructed left vector space. (Contributed by Mario
Carneiro, 2Oct2013.) (Revised by Jim Kingdon, 6Feb2023.)

Scalar


5Feb2023  lmodstrd 11688 
A constructed left module or left vector space is a structure.
(Contributed by Mario Carneiro, 1Oct2013.) (Revised by Jim Kingdon,
5Feb2023.)

Scalar
Struct 

5Feb2023  vscaslid 11687 
Slot property of .
(Contributed by Jim Kingdon, 5Feb2023.)

Slot 

5Feb2023  scaslid 11684 
Slot property of Scalar. (Contributed by Jim Kingdon,
5Feb2023.)

Scalar Slot
Scalar Scalar


5Feb2023  srngplusgd 11679 
The addition operation of a constructed star ring. (Contributed by
Mario Carneiro, 20Jun2015.) (Revised by Jim Kingdon, 5Feb2023.)



5Feb2023  srngbased 11678 
The base set of a constructed star ring. (Contributed by Mario
Carneiro, 18Nov2013.) (Revised by Jim Kingdon, 5Feb2023.)



5Feb2023  srngstrd 11677 
A constructed star ring is a structure. (Contributed by Mario Carneiro,
18Nov2013.) (Revised by Jim Kingdon, 5Feb2023.)

Struct 

5Feb2023  opelstrsl 11651 
The slot of a structure which contains an ordered pair for that slot.
(Contributed by Jim Kingdon, 5Feb2023.)

Slot Struct 

4Feb2023  starvslid 11676 
Slot property of . (Contributed by Jim
Kingdon, 4Feb2023.)

Slot


3Feb2023  rngbaseg 11671 
The base set of a constructed ring. (Contributed by Mario Carneiro,
2Oct2013.) (Revised by Jim Kingdon, 3Feb2023.)



3Feb2023  rngstrg 11670 
A constructed ring is a structure. (Contributed by Mario Carneiro,
28Sep2013.) (Revised by Jim Kingdon, 3Feb2023.)

Struct 

3Feb2023  mulrslid 11667 
Slot property of .
(Contributed by Jim Kingdon, 3Feb2023.)

Slot 

3Feb2023  plusgslid 11650 
Slot property of . (Contributed by Jim Kingdon, 3Feb2023.)

Slot 

2Feb2023  2strop1g 11660 
The other slot of a constructed twoslot structure. Version of
2stropg 11657 not depending on the hardcoded index value
of the base set.
(Contributed by AV, 22Sep2020.) (Revised by Jim Kingdon,
2Feb2023.)

Slot


2Feb2023  2strbas1g 11659 
The base set of a constructed twoslot structure. Version of 2strbasg 11656
not depending on the hardcoded index value of the base set.
(Contributed by AV, 22Sep2020.) (Revised by Jim Kingdon,
2Feb2023.)



2Feb2023  2strstr1g 11658 
A constructed twoslot structure. Version of 2strstrg 11655 not depending
on the hardcoded index value of the base set. (Contributed by AV,
22Sep2020.) (Revised by Jim Kingdon, 2Feb2023.)

Struct


31Jan2023  baseslid 11611 
The base set extractor is a slot. (Contributed by Jim Kingdon,
31Jan2023.)

Slot 

31Jan2023  strsl0 11603 
All components of the empty set are empty sets. (Contributed by Stefan
O'Rear, 27Nov2014.) (Revised by Jim Kingdon, 31Jan2023.)

Slot 

31Jan2023  strslss 11602 
Propagate component extraction to a structure from a subset
structure .
(Contributed by Mario Carneiro, 11Oct2013.)
(Revised by Jim Kingdon, 31Jan2023.)

Slot


31Jan2023  strslssd 11601 
Deduction version of strslss 11602. (Contributed by Mario Carneiro,
15Nov2014.) (Revised by Mario Carneiro, 30Apr2015.) (Revised by
Jim Kingdon, 31Jan2023.)

Slot


30Jan2023  strslfv3 11600 
Variant on strslfv 11599 for large structures. (Contributed by Mario
Carneiro, 10Jan2017.) (Revised by Jim Kingdon, 30Jan2023.)

Struct
Slot


30Jan2023  strslfv 11599 
Extract a structure component (such as the base set) from a
structure with
a component extractor
(such as the base set
extractor dfbase 11561). By virtue of ndxslid 11580, this can be done
without having to refer to the hardcoded numeric index of .
(Contributed by Mario Carneiro, 6Oct2013.) (Revised by Jim Kingdon,
30Jan2023.)

Struct Slot


30Jan2023  strslfv2 11598 
A variation on strslfv 11599 to avoid asserting that itself is a
function, which involves sethood of all the ordered pair components of
. (Contributed
by Mario Carneiro, 30Apr2015.) (Revised by Jim
Kingdon, 30Jan2023.)

Slot


30Jan2023  strslfv2d 11597 
Deduction version of strslfv 11599. (Contributed by Mario Carneiro,
30Apr2015.) (Revised by Jim Kingdon, 30Jan2023.)

Slot


30Jan2023  strslfvd 11596 
Deduction version of strslfv 11599. (Contributed by Mario Carneiro,
15Nov2014.) (Revised by Jim Kingdon, 30Jan2023.)

Slot


30Jan2023  strsetsid 11588 
Value of the structure replacement function. (Contributed by AV,
14Mar2020.) (Revised by Jim Kingdon, 30Jan2023.)

Slot Struct
sSet 

30Jan2023  funresdfunsndc 6279 
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2Dec2018.) (Revised by Jim Kingdon,
30Jan2023.)

DECID


29Jan2023  ndxslid 11580 
A structure component extractor is defined by its own index. That the
index is a natural number will also be needed in quite a few contexts so
it is included in the conclusion of this theorem which can be used as a
hypothesis of theorems like strslfv 11599. (Contributed by Jim Kingdon,
29Jan2023.)

Slot Slot 

29Jan2023  fnsnsplitdc 6278 
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27Feb2015.) (Revised by Jim Kingdon, 29Jan2023.)

DECID 

28Jan2023  2stropg 11657 
The other slot of a constructed twoslot structure. (Contributed by
Mario Carneiro, 29Aug2015.) (Revised by Jim Kingdon, 28Jan2023.)

Slot 

28Jan2023  2strbasg 11656 
The base set of a constructed twoslot structure. (Contributed by Mario
Carneiro, 29Aug2015.) (Revised by Jim Kingdon, 28Jan2023.)

Slot 

28Jan2023  2strstrg 11655 
A constructed twoslot structure. (Contributed by Mario Carneiro,
29Aug2015.) (Revised by Jim Kingdon, 28Jan2023.)

Slot Struct 

28Jan2023  1strstrg 11653 
A constructed oneslot structure. (Contributed by AV, 27Mar2020.)
(Revised by Jim Kingdon, 28Jan2023.)

Struct 

27Jan2023  strle2g 11646 
Make a structure from a pair. (Contributed by Mario Carneiro,
29Aug2015.) (Revised by Jim Kingdon, 27Jan2023.)

Struct 

27Jan2023  strle1g 11645 
Make a structure from a singleton. (Contributed by Mario Carneiro,
29Aug2015.) (Revised by Jim Kingdon, 27Jan2023.)

Struct 

27Jan2023  strleund 11643 
Combine two structures into one. (Contributed by Mario Carneiro,
29Aug2015.) (Revised by Jim Kingdon, 27Jan2023.)

Struct
Struct Struct 

26Jan2023  ressid2 11614 
General behavior of trivial restriction. (Contributed by Stefan O'Rear,
29Nov2014.) (Revised by Jim Kingdon, 26Jan2023.)

↾_{s}


24Jan2023  setsslnid 11606 
Value of the structure replacement function at an untouched index.
(Contributed by Mario Carneiro, 1Dec2014.) (Revised by Jim Kingdon,
24Jan2023.)

Slot
sSet 

24Jan2023  setsslid 11605 
Value of the structure replacement function at a replaced index.
(Contributed by Mario Carneiro, 1Dec2014.) (Revised by Jim Kingdon,
24Jan2023.)

Slot sSet


22Jan2023  setsabsd 11594 
Replacing the same components twice yields the same as the second
setting only. (Contributed by Mario Carneiro, 2Dec2014.) (Revised by
Jim Kingdon, 22Jan2023.)

sSet
sSet
sSet 

22Jan2023  setsresg 11593 
The structure replacement function does not affect the value of away
from .
(Contributed by Mario Carneiro, 1Dec2014.) (Revised by
Jim Kingdon, 22Jan2023.)

sSet 

22Jan2023  setsex 11587 
Applying the structure replacement function yields a set. (Contributed by
Jim Kingdon, 22Jan2023.)

sSet 

22Jan2023  2zsupmax 10718 
Two ways to express the maximum of two integers. Because order of
integers is decidable, we have more flexibility than for real numbers.
(Contributed by Jim Kingdon, 22Jan2023.)



22Jan2023  elpwpwel 4310 
A class belongs to a double power class if and only if its union belongs
to the power class. (Contributed by BJ, 22Jan2023.)



21Jan2023  funresdfunsnss 5514 
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value of
the element results in a subset of the function itself. (Contributed by
AV, 2Dec2018.) (Revised by Jim Kingdon, 21Jan2023.)



20Jan2023  setsvala 11586 
Value of the structure replacement function. (Contributed by Mario
Carneiro, 1Dec2014.) (Revised by Jim Kingdon, 20Jan2023.)

sSet 

20Jan2023  fnsnsplitss 5510 
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27Feb2015.) (Revised by Jim Kingdon, 20Jan2023.)



19Jan2023  strfvssn 11577 
A structure component extractor produces a value which is contained in a
set dependent on , but not .
This is sometimes useful for
showing sethood. (Contributed by Mario Carneiro, 15Aug2015.)
(Revised by Jim Kingdon, 19Jan2023.)

Slot 

19Jan2023  strnfvn 11576 
Value of a structure component extractor . Normally, is a
defined constant symbol such as (dfbase 11561) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section,
because it requires hardcoded index values. Instead, use strslfv 11599.
(Contributed by NM, 9Sep2011.) (Revised by Jim Kingdon, 19Jan2023.)
(New usage is discouraged.)

Slot 

19Jan2023  strnfvnd 11575 
Deduction version of strnfvn 11576. (Contributed by Mario Carneiro,
15Nov2014.) (Revised by Jim Kingdon, 19Jan2023.)

Slot 

18Jan2023  isstructr 11570 
The property of being a structure with components in .
(Contributed by Mario Carneiro, 29Aug2015.) (Revised by Jim Kingdon,
18Jan2023.)

Struct 

18Jan2023  isstructim 11569 
The property of being a structure with components in .
(Contributed by Mario Carneiro, 29Aug2015.) (Revised by Jim Kingdon,
18Jan2023.)

Struct
