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
Theorem	f1imaenfi 9201	If a function is one-to-one, then the image of a finite subset of its domain under it is equinumerous to the subset. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1imaeng 9013). (Contributed by BTernaryTau, 29-Sep-2024.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	ssdomfi 9202	A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8999). (Contributed by BTernaryTau, 12-Nov-2024.)
⊢ (𝐵 ∈ Fin → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))
Theorem	ssdomfi2 9203	A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8999). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ≼ 𝐵)
Theorem	sbthfilem 9204*	Lemma for sbthfi 9205. (Contributed by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbthfi 9205	Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 9096). (Contributed by BTernaryTau, 4-Nov-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	domnsymfi 9206	If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike domnsym 9102). (Contributed by BTernaryTau, 22-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ≺ 𝐴)
Theorem	sdomdomtrfi 9207	Transitivity of strict dominance and dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 9113). (Contributed by BTernaryTau, 25-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	domsdomtrfi 9208	Transitivity of dominance and strict dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 9115). (Contributed by BTernaryTau, 25-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sucdom2 9209	Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5364. (Revised by BTernaryTau, 4-Dec-2024.)
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵)
2.4.33  Pigeonhole Principle
Theorem	phplem1 9210	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 5364. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2 9211	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 5364. (Revised by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵))
Theorem	nneneq 9212	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 5364. (Revised by BTernaryTau, 11-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	php 9213	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 9210, phplem2 9211, nneneq 9212, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5364. (Revised by BTernaryTau, 18-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2 9214	Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5364. (Revised by BTernaryTau, 20-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3 9215	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 5364. (Revised by BTernaryTau, 26-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php4 9216	Corollary of the Pigeonhole Principle php 9213: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴)
Theorem	php5 9217	Corollary of the Pigeonhole Principle php 9213: 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 9218	Corollary of the Pigeonhole Principle using equality. Strengthening of php 9213 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomog 9219	Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9236 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9236. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5364. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	phplem1OLD 9220	Obsolete lemma for php 9213. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2OLD 9221	Obsolete lemma for php 9213. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem3OLD 9222	Obsolete version of phplem1 9210 as of 23-Sep-2024. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem4OLD 9223	Obsolete version of phplem2 9211 as of 4-Nov-2024. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵))
Theorem	nneneqOLD 9224	Obsolete version of nneneq 9212 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	phpOLD 9225	Obsolete version of php 9213 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2OLD 9226	Obsolete version of php2 9214 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3OLD 9227	Obsolete version of php3 9215 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	phpeqdOLD 9228	Obsolete version of phpeqd 9218 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomogOLD 9229	Obsolete version of nndomog 9219 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9236. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	snnen2oOLD 9230	Obsolete version of snnen2o 9240 as of 18-Nov-2024. (Contributed by AV, 6-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ {𝐴} ≈ 2o
2.4.34  Finite sets (cont.)
Theorem	onomeneq 9231	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 5364. (Revised by BTernaryTau, 2-Dec-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onomeneqOLD 9232	Obsolete version of onomeneq 9231 as of 29-Nov-2024. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onfin 9233	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	onfin2 9234	A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ ω = (On ∩ Fin)
Theorem	nnfiOLD 9235	Obsolete version of nnfi 9170 as of 23-Sep-2024. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)
Theorem	nndomo 9236	Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	nnsdomo 9237	Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	sucdom 9238	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 5364. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	sucdomOLD 9239	Obsolete version of sucdom 9238 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	snnen2o 9240	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 5364, ax-un 7728. (Revised by BTernaryTau, 1-Dec-2024.)
⊢ ¬ {𝐴} ≈ 2o
Theorem	0sdom1dom 9241	Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7728, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7728. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	0sdom1domALT 9242	Alternate proof of 0sdom1dom 9241, shorter but requiring ax-un 7728. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	1sdom2 9243	Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7728, see 1sdom2ALT 9244. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7728. (Revised by BTernaryTau, 8-Dec-2024.)
⊢ 1o ≺ 2o
Theorem	1sdom2ALT 9244	Alternate proof of 1sdom2 9243, shorter but requiring ax-un 7728. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1o ≺ 2o
Theorem	sdom1 9245	A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5364, ax-un 7728. (Revised by BTernaryTau, 12-Dec-2024.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	sdom1OLD 9246	Obsolete version of sdom1 9245 as of 12-Dec-2024. (Contributed by Stefan O'Rear, 28-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	modom 9247	Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o)
Theorem	modom2 9248*	Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o)
Theorem	rex2dom 9249*	A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴)
Theorem	1sdom2dom 9250	Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴)
Theorem	1sdom 9251*	A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 9033.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7728. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	1sdomOLD 9252*	Obsolete version of 1sdom 9251 as of 30-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	unxpdomlem1 9253*	Lemma for unxpdom 9256. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
Theorem	unxpdomlem2 9254*	Lemma for unxpdom 9256. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    &   ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏))    &   ⊢ (𝜑 → ¬ 𝑚 = 𝑛)    &   ⊢ (𝜑 → ¬ 𝑠 = 𝑡)    ⇒   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
Theorem	unxpdomlem3 9255*	Lemma for unxpdom 9256. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
Theorem	unxpdom 9256	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 9257	Corollary of unxpdom 9256. (Contributed by NM, 16-Sep-2004.)
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴))
Theorem	sucxpdom 9258	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 9259	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 9260	A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵)
Theorem	ominf 9261	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5364. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ ¬ ω ∈ Fin
Theorem	ominfOLD 9262	Obsolete version of ominf 9261 as of 2-Jan-2025. (Contributed by NM, 2-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ω ∈ Fin
Theorem	isinf 9263*	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 5364. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	isinfOLD 9264*	Obsolete version of isinf 9263 as of 2-Jan-2025. (Contributed by Mario Carneiro, 15-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	fineqvlem 9265	Lemma for fineqv 9266. (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 9266	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	enfiiOLD 9267	Obsolete version of enfii 9192 as of 23-Sep-2024. (Contributed by Mario Carneiro, 12-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
Theorem	pssnnOLD 9268*	Obsolete version of pssnn 9171 as of 31-Jul-2024. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)
Theorem	xpfir 9269	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 9270	A subset of a finite set is finite, deduction version of ssfi 9176. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	infi 9271	The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin)
Theorem	rabfi 9272*	A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin)
Theorem	finresfin 9273	The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin)
Theorem	f1finf1o 9274	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 5364. (Revised by BTernaryTau, 4-Jan-2025.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))
Theorem	f1finf1oOLD 9275	Obsolete version of f1finf1o 9274 as of 4-Jan-2025. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))
Theorem	nfielex 9276*	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 9277	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) Avoid ax-pow 5364, ax-un 7728. (Revised by BTernaryTau, 4-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴})
Theorem	en1eqsnOLD 9278	Obsolete version of en1eqsn 9277 as of 4-Jan-2025. (Contributed by FL, 18-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴})
Theorem	en1eqsnbi 9279	A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20542. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴}))
Theorem	dif1ennnALT 9280	Alternate proof of dif1ennn 9164 using ax-pow 5364. (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 9281	Lemma for uses of enp1i 9282. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 𝑇 = ({𝑥} ∪ 𝑆)    ⇒   ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇))
Theorem	enp1i 9282*	Proof induction for en2 9284 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) Generalize to all ordinals and avoid ax-pow 5364, ax-un 7728. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ Ord 𝑀    &   ⊢ 𝑁 = suc 𝑀    &   ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑)    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓)
Theorem	enp1iOLD 9283*	Obsolete version of enp1i 9282 as of 6-Jan-2025. (Contributed by Mario Carneiro, 5-Jan-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 ∈ ω    &   ⊢ 𝑁 = suc 𝑀    &   ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑)    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓)
Theorem	en2 9284*	A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦})
Theorem	en3 9285*	A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧})
Theorem	en4 9286*	A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤}))
Theorem	findcard2OLD 9287*	Obsolete version of findcard2 9167 as of 6-Aug-2024. (Contributed by Jeff Madsen, 8-Jul-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard3 9288*	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 5364. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard3OLD 9289*	Obsolete version of findcard3 9288 as of 7-Jan-2025. (Contributed by Mario Carneiro, 13-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	ac6sfi 9290*	A version of ac6s 10482 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	frfi 9291	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 9292*	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 9293*	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 9294*	Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)))
Theorem	wofi 9295	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 9296	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 9297	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 9298*	Lemma for unbnn 9302. 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 9299*	Lemma for unbnn 9302. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴))
Theorem	unblem3 9300*	Lemma for unbnn 9302. The value of the function 𝐹 is less than its value at a successor. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ (𝐹‘suc 𝑧)))