P. 72 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	infm 7101*	An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.)
⊢ (ω ≼ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	infn0 7102	An infinite set is not empty. (Contributed by NM, 23-Oct-2004.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	inffiexmid 7103*	If any given set is either finite or infinite, excluded middle follows. For another example, 𝒫 1o is not infinite, by pw1ninf 16650, but also cannot be shown to be finite by pw1fin 7107. (Contributed by Jim Kingdon, 15-Jun-2022.)
⊢ (𝑥 ∈ Fin ∨ ω ≼ 𝑥)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
Theorem	en2eqpr 7104	Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵}))
Theorem	exmidpw 7105	Excluded middle is equivalent to the power set of 1o having two elements. Remark of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 30-Jun-2022.)
⊢ (EXMID ↔ 𝒫 1o ≈ 2o)
Theorem	exmidpweq 7106	Excluded middle is equivalent to the power set of 1o being 2o. (Contributed by Jim Kingdon, 28-Jul-2024.)
⊢ (EXMID ↔ 𝒫 1o = 2o)
Theorem	pw1fin 7107	Excluded middle is equivalent to the power set of 1o being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
⊢ (EXMID ↔ 𝒫 1o ∈ Fin)
Theorem	pw1dc0el 7108	Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
⊢ (EXMID ↔ ∀𝑥 ∈ 𝒫 1oDECID ∅ ∈ 𝑥)
Theorem	exmidpw2en 7109	The power set of a set being equinumerous to set exponentiation with a base of ordinal 2o is equivalent to excluded middle. This is Metamath 100 proof #52. The forward direction uses excluded middle expressed as EXMID to show this equinumerosity. The reverse direction is the one which establishes that power set being equinumerous to set exponentiation implies excluded middle. This resolves the question of whether we will be able to prove this equinumerosity theorem in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.)
⊢ (EXMID ↔ ∀𝑥𝒫 𝑥 ≈ (2o ↑𝑚 𝑥))
Theorem	ss1o0el1o 7110	Reformulation of ss1o0el1 4289 using 1o instead of {∅}. (Contributed by BJ, 9-Aug-2024.)
⊢ (𝐴 ⊆ 1o → (∅ ∈ 𝐴 ↔ 𝐴 = 1o))
Theorem	pw1dc1 7111	If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.)
⊢ (EXMID ↔ ∀𝑥 ∈ 𝒫 1oDECID 𝑥 = 1o)
Theorem	fientri3 7112	Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴))
Theorem	nnwetri 7113*	A natural number is well-ordered by E. More specifically, this order both satisfies We and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.)
⊢ (𝐴 ∈ ω → ( E We 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)))
Theorem	onunsnss 7114	Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.)
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ⊆ 𝐴)
Theorem	unfiexmid 7115*	If the union of any two finite sets is finite, excluded middle follows. Remark 8.1.17 of [AczelRathjen], p. 74. (Contributed by Mario Carneiro and Jim Kingdon, 5-Mar-2022.)
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑥 ∪ 𝑦) ∈ Fin)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
Theorem	unsnfi 7116	Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∪ {𝐵}) ∈ Fin)
Theorem	unsnfidcex 7117	The 𝐵 ∈ 𝑉 condition in unsnfi 7116. This is intended to show that unsnfi 7116 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵 ∈ V)
Theorem	unsnfidcel 7118	The ¬ 𝐵 ∈ 𝐴 condition in unsnfi 7116. This is intended to show that unsnfi 7116 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵 ∈ 𝐴)
Theorem	unfidisj 7119	The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ Fin)
Theorem	undifdcss 7120*	Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.)
⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵))
Theorem	undifdc 7121*	Union of complementary parts into whole. This is a case where we can strengthen undifss 3574 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
Theorem	undiffi 7122	Union of complementary parts into whole. This is a case where we can strengthen undifss 3574 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)))
Theorem	unfiin 7123	The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
Theorem	prfidisj 7124	A pair is finite if it consists of two unequal sets. For the case where 𝐴 = 𝐵, see snfig 6994. For the cases where one or both is a proper class, see prprc1 3781, prprc2 3782, or prprc 3783. (Contributed by Jim Kingdon, 31-May-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ Fin)
Theorem	prfidceq 7125*	A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 DECID 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin)
Theorem	tpfidisj 7126	A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin)
Theorem	tpfidceq 7127*	A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 DECID 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin)
Theorem	fiintim 7128*	If a class is closed under pairwise intersections, then it is closed under nonempty finite intersections. The converse would appear to require an additional condition, such as 𝑥 and 𝑦 not being equal, or 𝐴 having decidable equality. This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
Theorem	xpfi 7129	The Cartesian product of two finite sets is finite. Lemma 8.1.16 of [AczelRathjen], p. 74. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Theorem	imaf1fi 7130	The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	3xpfi 7131	The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin)
Theorem	fisseneq 7132	A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵)
Theorem	phpeqd 7133	Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 7057 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	ssfirab 7134*	A subset of a finite set is finite if it is defined by a decidable property. (Contributed by Jim Kingdon, 27-May-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 DECID 𝜓)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ Fin)
Theorem	ssfidc 7135*	A subset of a finite set is finite if membership in the subset is decidable. (Contributed by Jim Kingdon, 27-May-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin)
Theorem	exmidssfi 7136*	Excluded middle is equivalent to any subset of a finite set being finite. Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 20-Mar-2026.)
⊢ (EXMID ↔ ∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin))
Theorem	opabfi 7137*	Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 DECID 𝜓)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Fin)
Theorem	infidc 7138*	The intersection of two sets is finite if one of them is and the other is decidable. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵) → (𝐴 ∩ 𝐵) ∈ Fin)
Theorem	snon0 7139	An ordinal which is a singleton is {∅}. (Contributed by Jim Kingdon, 19-Oct-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ∈ On) → 𝐴 = ∅)
Theorem	fnfi 7140	A version of fnex 5879 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin)
Theorem	fundmfi 7141	The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐴) → dom 𝐴 ∈ Fin)
Theorem	fundmfibi 7142	A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin))
Theorem	resfnfinfinss 7143	The restriction of a function to a finite subset of its domain is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) ∈ Fin)
Theorem	residfi 7144	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)
Theorem	relcnvfi 7145	If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.)
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ◡𝐴 ∈ Fin)
Theorem	funrnfi 7146	The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.)
⊢ ((Rel 𝐴 ∧ Fun ◡𝐴 ∧ 𝐴 ∈ Fin) → ran 𝐴 ∈ Fin)
Theorem	f1ofi 7147	If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐵 ∈ Fin)
Theorem	f1dmvrnfibi 7148	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 7149. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	f1vrnfibi 7149	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 7148. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	iunfidisj 7150*	The finite union of disjoint finite sets is finite. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin ∧ Disj 𝑥 ∈ 𝐴 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	f1finf1o 7151	Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))
Theorem	en1eqsn 7152	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴})
Theorem	en1eqsnbi 7153	A set containing an element has exactly one element iff it is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴}))
Theorem	snexxph 7154*	A case where the antecedent of snexg 4276 is not needed. The class {𝑥 ∣ 𝜑} is from dcextest 4681. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.)
⊢ {{𝑥 ∣ 𝜑}} ∈ V
Theorem	preimaf1ofi 7155	The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.)
⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin)
Theorem	fidcenumlemim 7156*	Lemma for fidcenum 7160. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.)
⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴))
Theorem	fidcenumlemrks 7157*	Lemma for fidcenum 7160. Induction step for fidcenumlemrk 7158. (Contributed by Jim Kingdon, 20-Oct-2022.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)    &   ⊢ (𝜑 → 𝐽 ∈ ω)    &   ⊢ (𝜑 → suc 𝐽 ⊆ 𝑁)    &   ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐽)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽)))
Theorem	fidcenumlemrk 7158*	Lemma for fidcenum 7160. (Contributed by Jim Kingdon, 20-Oct-2022.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → 𝐾 ⊆ 𝑁)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾)))
Theorem	fidcenumlemr 7159*	Lemma for fidcenum 7160. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    ⇒   ⊢ (𝜑 → 𝐴 ∈ Fin)
Theorem	fidcenum 7160*	A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as ∃𝑛 ∈ ω∃𝑓𝑓:𝑛–onto→𝐴 is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.)
⊢ (𝐴 ∈ Fin ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴))
2.6.32  Schroeder-Bernstein Theorem
Theorem	sbthlem1 7161*	Lemma for isbth 7171. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))))
Theorem	sbthlem2 7162*	Lemma for isbth 7171. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷)
Theorem	sbthlemi3 7163*	Lemma for isbth 7171. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ ((EXMID ∧ ran 𝑔 ⊆ 𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷))
Theorem	sbthlemi4 7164*	Lemma for isbth 7171. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷)))
Theorem	sbthlemi5 7165*	Lemma for isbth 7171. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴)) → dom 𝐻 = 𝐴)
Theorem	sbthlemi6 7166*	Lemma for isbth 7171. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ (((EXMID ∧ ran 𝑓 ⊆ 𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵)
Theorem	sbthlem7 7167*	Lemma for isbth 7171. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻)
Theorem	sbthlemi8 7168*	Lemma for isbth 7171. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ (((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻)
Theorem	sbthlemi9 7169*	Lemma for isbth 7171. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	sbthlemi10 7170*	Lemma for isbth 7171. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((EXMID ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵)
Theorem	isbth 7171	Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set 𝐴 is smaller (has lower cardinality) than 𝐵 and vice-versa, then 𝐴 and 𝐵 are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 7161 through sbthlemi10 7170; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 7170. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. The proof does require the law of the excluded middle which cannot be avoided as shown at exmidsbthr 16690. (Contributed by NM, 8-Jun-1998.)
⊢ ((EXMID ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵)
2.6.33  Finite intersections
Syntax	cfi 7172	Extend class notation with the function whose value is the class of finite intersections of the elements of a given set.
class fi
Definition	df-fi 7173*	Function whose value is the class of finite intersections of the elements of the argument. Note that the empty intersection being the universal class, hence a proper class, it cannot be an element of that class. Therefore, the function value is the class of nonempty finite intersections of elements of the argument (see elfi2 7176). (Contributed by FL, 27-Apr-2008.)
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})
Theorem	fival 7174*	The set of all the finite intersections of the elements of 𝐴. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥})
Theorem	elfi 7175*	Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥))
Theorem	elfi2 7176*	The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥))
Theorem	elfir 7177	Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵))
Theorem	ssfii 7178	Any element of a set 𝐴 is the intersection of a finite subset of 𝐴. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴))
Theorem	fi0 7179	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (fi‘∅) = ∅
Theorem	fieq0 7180	A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ ↔ (fi‘𝐴) = ∅))
Theorem	fiss 7181	Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵))
Theorem	fiuni 7182	The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪ (fi‘𝐴))
Theorem	fipwssg 7183	If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝒫 𝑋) → (fi‘𝐴) ⊆ 𝒫 𝑋)
Theorem	fifo 7184*	Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴))
Theorem	dcfi 7185*	Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑)
2.6.34  Supremum and infimum
Syntax	csup 7186	Extend class notation to include supremum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers.
class sup(𝐴, 𝐵, 𝑅)
Syntax	cinf 7187	Extend class notation to include infimum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers.
class inf(𝐴, 𝐵, 𝑅)
Definition	df-sup 7188*	Define the supremum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the supremum exists. (Contributed by NM, 22-May-1999.)
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
Definition	df-inf 7189	Define the infimum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the infimum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020.)
⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)
Theorem	supeq1 7190	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Theorem	supeq1d 7191	Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Theorem	supeq1i 7192	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
Theorem	supeq2 7193	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅))
Theorem	supeq3 7194	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆))
Theorem	supeq123d 7195	Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹))
Theorem	nfsup 7196	Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅)
Theorem	supmoti 7197*	Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 8264) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.)
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    ⇒   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
Theorem	supeuti 7198*	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by Jim Kingdon, 23-Nov-2021.)
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
Theorem	supval2ti 7199*	Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.)
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
Theorem	eqsupti 7200*	Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.)
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶))