P. 93 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
2.4.33  Pigeonhole Principle
Theorem	phplem1 9201	Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2 9202	Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) Avoid ax-pow 5334. (Revised by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵))
Theorem	nneneq 9203	Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. (Contributed by NM, 28-May-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 11-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	php 9204	Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of phplem1 9201, phplem2 9202, nneneq 9203, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 18-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2 9205	Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 20-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3 9206	Corollary of Pigeonhole Principle. If 𝐴 is finite and 𝐵 is a proper subset of 𝐴, the 𝐵 is strictly less numerous than 𝐴. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5334. (Revised by BTernaryTau, 26-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php4 9207	Corollary of the Pigeonhole Principle php 9204: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴)
Theorem	php5 9208	Corollary of the Pigeonhole Principle php 9204: a natural number is not equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring] p. 90. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ ω → ¬ 𝐴 ≈ suc 𝐴)
Theorem	phpeqd 9209	Corollary of the Pigeonhole Principle using equality. Strengthening of php 9204 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow 5334. (Revised by BTernaryTau, 28-Nov-2024.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomog 9210	Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9215 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9215. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5334. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2.4.34  Finite sets (cont.)
Theorem	onomeneq 9211	An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of [TakeutiZaring] p. 90 and its converse. (Contributed by NM, 26-Jul-2004.) Avoid ax-pow 5334. (Revised by BTernaryTau, 2-Dec-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onfin 9212	An ordinal number is finite iff it is a natural number. Proposition 10.32 of [TakeutiZaring] p. 92. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ On → (𝐴 ∈ Fin ↔ 𝐴 ∈ ω))
Theorem	ordfin 9213	A generalization of onfin 9212 to include the class of all ordinals. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (Ord 𝐴 → (𝐴 ∈ Fin ↔ 𝐴 ∈ ω))
Theorem	onfin2 9214	A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ ω = (On ∩ Fin)
Theorem	nndomo 9215	Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	nnsdomo 9216	Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	sucdom 9217	Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-pow 5334. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	snnen2o 9218	A singleton {𝐴} is never equinumerous with the ordinal number 2. This holds for proper singletons (𝐴 ∈ V) as well as for singletons being the empty set (𝐴 ∉ V). (Contributed by AV, 6-Aug-2019.) Avoid ax-pow 5334, ax-un 7739. (Revised by BTernaryTau, 1-Dec-2024.)
⊢ ¬ {𝐴} ≈ 2o
Theorem	0sdom1dom 9219	Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7739, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7739. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	0sdom1domALT 9220	Alternate proof of 0sdom1dom 9219, shorter but requiring ax-un 7739. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	1sdom2 9221	Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7739, see 1sdom2ALT 9222. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7739. (Revised by BTernaryTau, 8-Dec-2024.)
⊢ 1o ≺ 2o
Theorem	1sdom2ALT 9222	Alternate proof of 1sdom2 9221, shorter but requiring ax-un 7739. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1o ≺ 2o
Theorem	sdom1 9223	A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5334, ax-un 7739. (Revised by BTernaryTau, 12-Dec-2024.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	modom 9224	Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o)
Theorem	modom2 9225*	Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o)
Theorem	rex2dom 9226*	A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴)
Theorem	1sdom2dom 9227	Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴)
Theorem	1sdom 9228*	A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 9040.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7739. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	unxpdomlem1 9229*	Lemma for unxpdom 9232. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
Theorem	unxpdomlem2 9230*	Lemma for unxpdom 9232. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    &   ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏))    &   ⊢ (𝜑 → ¬ 𝑚 = 𝑛)    &   ⊢ (𝜑 → ¬ 𝑠 = 𝑡)    ⇒   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
Theorem	unxpdomlem3 9231*	Lemma for unxpdom 9232. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
Theorem	unxpdom 9232	Cartesian product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 13-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
⊢ ((1o ≺ 𝐴 ∧ 1o ≺ 𝐵) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐵))
Theorem	unxpdom2 9233	Corollary of unxpdom 9232. (Contributed by NM, 16-Sep-2004.)
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴))
Theorem	sucxpdom 9234	Cartesian product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
⊢ (1o ≺ 𝐴 → suc 𝐴 ≼ (𝐴 × 𝐴))
Theorem	pssinf 9235	A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.)
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵) → ¬ 𝐵 ∈ Fin)
Theorem	fisseneq 9236	A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵)
Theorem	ominf 9237	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ ¬ ω ∈ Fin
Theorem	isinf 9238*	Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.) Avoid ax-pow 5334. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	fineqvlem 9239	Lemma for fineqv 9240. (Contributed by Mario Carneiro, 20-Jan-2013.) (Proof shortened by Stefan O'Rear, 3-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝒫 𝒫 𝐴)
Theorem	fineqv 9240	If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 3-Jan-2015.)
⊢ (¬ ω ∈ V ↔ Fin = V)
Theorem	xpfir 9241	The components of a nonempty finite Cartesian product are finite. (Contributed by Paul Chapman, 11-Apr-2009.) (Proof shortened by Mario Carneiro, 29-Apr-2015.)
⊢ (((𝐴 × 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	ssfid 9242	A subset of a finite set is finite, deduction version of ssfi 9170. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	infi 9243	The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin)
Theorem	rabfi 9244*	A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin)
Theorem	finresfin 9245	The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin)
Theorem	f1finf1o 9246	Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) Avoid ax-pow 5334. (Revised by BTernaryTau, 4-Jan-2025.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))
Theorem	nfielex 9247*	If a class is not finite, then it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ (¬ 𝐴 ∈ Fin → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	en1eqsn 9248	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) Avoid ax-pow 5334, ax-un 7739. (Revised by BTernaryTau, 4-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴})
Theorem	en1eqsnbi 9249	A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20322. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴}))
Theorem	dif1ennnALT 9250	Alternate proof of dif1ennn 9160 using ax-pow 5334. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	enp1ilem 9251	Lemma for uses of enp1i 9252. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 𝑇 = ({𝑥} ∪ 𝑆)    ⇒   ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇))
Theorem	enp1i 9252*	Proof induction for en2 9253 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) Generalize to all ordinals and avoid ax-pow 5334, ax-un 7739. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ Ord 𝑀    &   ⊢ 𝑁 = suc 𝑀    &   ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑)    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓)
Theorem	en2 9253*	A set equinumerous to ordinal 2 is an unordered pair. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦})
Theorem	en3 9254*	A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧})
Theorem	en4 9255*	A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤}))
Theorem	findcard3 9256*	Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) Avoid ax-pow 5334. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	ac6sfi 9257*	A version of ac6s 10489 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	frfi 9258	A partial order is well-founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)
Theorem	fimax2g 9259*	A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦)
Theorem	fimaxg 9260*	A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑦𝑅𝑥))
Theorem	fisupg 9261*	Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)))
Theorem	wofi 9262	A total order on a finite set is a well-order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴)
Theorem	ordunifi 9263	The maximum of a finite collection of ordinals is in the set. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)
Theorem	nnunifi 9264	The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝑆 ⊆ ω ∧ 𝑆 ∈ Fin) → ∪ 𝑆 ∈ ω)
Theorem	unblem1 9265*	Lemma for unbnn 9269. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003.)
⊢ (((𝐵 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦) ∧ 𝐴 ∈ 𝐵) → ∩ (𝐵 ∖ suc 𝐴) ∈ 𝐵)
Theorem	unblem2 9266*	Lemma for unbnn 9269. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴))
Theorem	unblem3 9267*	Lemma for unbnn 9269. The value of the function 𝐹 is less than its value at a successor. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ (𝐹‘suc 𝑧)))
Theorem	unblem4 9268*	Lemma for unbnn 9269. The function 𝐹 maps the set of natural numbers one-to-one to the set of unbounded natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → 𝐹:ω–1-1→𝐴)
Theorem	unbnn 9269*	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of [Suppes] p. 151. See unbnn3 9641 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.)
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	unbnn2 9270*	Version of unbnn 9269 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.)
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω)
Theorem	isfinite2 9271	Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does not require the Axiom of Infinity. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
Theorem	nnsdomg 9272	Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of Infinity, we include it as part of the antecedent. See nnsdom 9636 for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998.) Avoid ax-pow 5334. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω)
Theorem	isfiniteg 9273	A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ (ω ∈ V → (𝐴 ∈ Fin ↔ 𝐴 ≺ ω))
Theorem	infsdomnn 9274	An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5334. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴)
Theorem	infn0 9275	An infinite set is not empty. For a shorter proof using ax-un 7739, see infn0ALT 9276. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7739. (Revised by BTernaryTau, 8-Jan-2025.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	infn0ALT 9276	Shorter proof of infn0 9275 using ax-un 7739. (Contributed by NM, 23-Oct-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	fin2inf 9277	This (useless) theorem, which was proved without the Axiom of Infinity, demonstrates an artifact of our definition of binary relation, which is meaningful only when its arguments exist. In particular, the antecedent cannot be satisfied unless ω exists. (Contributed by NM, 13-Nov-2003.)
⊢ (𝐴 ≺ ω → ω ∈ V)
Theorem	unfilem1 9278*	Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))    ⇒   ⊢ ran 𝐹 = ((𝐴 +o 𝐵) ∖ 𝐴)
Theorem	unfilem2 9279*	Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))    ⇒   ⊢ 𝐹:𝐵–1-1-onto→((𝐴 +o 𝐵) ∖ 𝐴)
Theorem	unfilem3 9280	Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 16-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ≈ ((𝐴 +o 𝐵) ∖ 𝐴))
Theorem	unfir 9281	If a union is finite, the operands are finite. Converse of unfi 9168. (Contributed by FL, 3-Aug-2009.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfib 9282	A union is finite if and only if the operands are finite. (Contributed by AV, 10-May-2025.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfi2 9283	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 9168 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9277). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω)
Theorem	difinf 9284	An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin)
Theorem	fodomfi 9285	An onto function implies dominance of domain over range, for finite sets. Unlike fodomg 10527 for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) Avoid ax-pow 5334. (Revised by BTernaryTau, 20-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
Theorem	fofi 9286	If an onto function has a finite domain, its codomain/range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)
Theorem	f1fi 9287	If a 1-to-1 function has a finite codomain its domain is finite. (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ∈ Fin)
Theorem	imafi 9288	Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	pwfir 9289	If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024.)
⊢ (𝒫 𝐵 ∈ Fin → 𝐵 ∈ Fin)
Theorem	pwfilem 9290*	Lemma for pwfi 9291. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5334. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))    ⇒   ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)
Theorem	pwfi 9291	The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5334. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
Theorem	xpfi 9292	The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5334. (Revised by BTernaryTau, 10-Jan-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Theorem	3xpfi 9293	The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin)
Theorem	domunfican 9294	A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴) ∧ ((𝐴 ∩ 𝑋) = ∅ ∧ (𝐵 ∩ 𝑌) = ∅)) → ((𝐴 ∪ 𝑋) ≼ (𝐵 ∪ 𝑌) ↔ 𝑋 ≼ 𝑌))
Theorem	infcntss 9295*	Every infinite set has a denumerable subset. Similar to Exercise 8 of [TakeutiZaring] p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) (Contributed by NM, 23-Oct-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω))
Theorem	prfi 9296	An unordered pair is finite. For a shorter proof using ax-un 7739, see prfiALT 9297. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2194, ax-un 7739. (Revised by BTernaryTau, 13-Jan-2025.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	prfiALT 9297	Shorter proof of prfi 9296 using ax-un 7739. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	tpfi 9298	An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.)
⊢ {𝐴, 𝐵, 𝐶} ∈ Fin
Theorem	fiint 9299*	Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of 𝐴 is in 𝐴". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.) Use a separate setvar for the right-hand side and avoid ax-pow 5334. (Revised by BTernaryTau, 14-Jan-2025.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
Theorem	fodomfir 9300*	There exists a mapping from a finite set onto any nonempty set that it dominates, proved without using the Axiom of Power Sets (unlike fodomr 9129). (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)