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	dif1ennn 9201	If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9311. (Contributed by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	dif1enOLD 9202	Obsolete version of dif1en 9200 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	findcard 9203*	Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ Fin → (∀𝑧 ∈ 𝑦 𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard2 9204*	Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.) Avoid ax-pow 5365. (Revised by BTernaryTau, 26-Aug-2024.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard2s 9205*	Variation of findcard2 9204 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard2d 9206*	Deduction version of findcard2 9204. (Contributed by SO, 16-Jul-2018.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	nnfi 9207	Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)
Theorem	pssnn 9208*	A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) Avoid ax-pow 5365. (Revised by BTernaryTau, 31-Jul-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)
Theorem	ssnnfi 9209	A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	0finOLD 9210	Obsolete version of 0fi 9082 as of 13-Jan-2025. (Contributed by FL, 14-Jul-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∅ ∈ Fin
Theorem	unfi 9211	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Aug-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
Theorem	unfid 9212	The union of two finite sets is finite. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ Fin)
Theorem	ssfi 9213	A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5365, see ssfiALT 9214. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 12-Aug-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	ssfiALT 9214	Shorter proof of ssfi 9213 using ax-pow 5365. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	diffi 9215	If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.)
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin)
Theorem	cnvfi 9216	If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5365. (Revised by BTernaryTau, 9-Sep-2024.)
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin)
Theorem	pwssfi 9217	Every element of the power set of 𝐴 is finite if and only if 𝐴 is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin))
Theorem	fnfi 9218	A version of fnex 7237 for finite sets that does not require Replacement or Power Sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin)
Theorem	f1oenfi 9219	If the domain of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1oeng 9011). (Contributed by BTernaryTau, 8-Sep-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1oenfirn 9220	If the range of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. (Contributed by BTernaryTau, 9-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1domfi 9221	If the codomain of a one-to-one function is finite, then the function's domain is dominated by its codomain. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1domg 9012). (Contributed by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1domfi2 9222	If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike f1dom2g 9010). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	enreffi 9223	Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 9024). (Contributed by BTernaryTau, 8-Sep-2024.)
⊢ (𝐴 ∈ Fin → 𝐴 ≈ 𝐴)
Theorem	ensymfib 9224	Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 9042). (Contributed by BTernaryTau, 9-Sep-2024.)
⊢ (𝐴 ∈ Fin → (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴))
Theorem	entrfil 9225	Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9046). (Contributed by BTernaryTau, 10-Sep-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	enfii 9226	A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
Theorem	enfi 9227	Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5365, see enfiALT 9228. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
Theorem	enfiALT 9228	Shorter proof of enfi 9227 using ax-pow 5365. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
Theorem	domfi 9229	A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006.) (Revised by Mario Carneiro, 12-Mar-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin)
Theorem	entrfi 9230	Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9046). (Contributed by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	entrfir 9231	Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9046). (Contributed by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	domtrfil 9232	Transitivity of dominance relation when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domtr 9047). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domtrfi 9233	Transitivity of dominance relation when 𝐵 is finite, proved without using the Axiom of Power Sets (unlike domtr 9047). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domtrfir 9234	Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 9047). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	f1imaenfi 9235	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 9054). (Contributed by BTernaryTau, 29-Sep-2024.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	ssdomfi 9236	A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 9040). (Contributed by BTernaryTau, 12-Nov-2024.)
⊢ (𝐵 ∈ Fin → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))
Theorem	ssdomfi2 9237	A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 9040). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ≼ 𝐵)
Theorem	sbthfilem 9238*	Lemma for sbthfi 9239. (Contributed by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbthfi 9239	Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 9133). (Contributed by BTernaryTau, 4-Nov-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	domnsymfi 9240	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 9139). (Contributed by BTernaryTau, 22-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ≺ 𝐴)
Theorem	sdomdomtrfi 9241	Transitivity of strict dominance and dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 9150). (Contributed by BTernaryTau, 25-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	domsdomtrfi 9242	Transitivity of dominance and strict dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 9152). (Contributed by BTernaryTau, 25-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sucdom2 9243	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 5365. (Revised by BTernaryTau, 4-Dec-2024.)
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵)
2.4.33  Pigeonhole Principle
Theorem	phplem1 9244	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 5365. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2 9245	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 5365. (Revised by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵))
Theorem	nneneq 9246	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 5365. (Revised by BTernaryTau, 11-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	php 9247	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 9244, phplem2 9245, nneneq 9246, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 18-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2 9248	Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 20-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3 9249	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 5365. (Revised by BTernaryTau, 26-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php4 9250	Corollary of the Pigeonhole Principle php 9247: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴)
Theorem	php5 9251	Corollary of the Pigeonhole Principle php 9247: 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 9252	Corollary of the Pigeonhole Principle using equality. Strengthening of php 9247 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow 5365. (Revised by BTernaryTau, 28-Nov-2024.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomog 9253	Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9269 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9269. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5365. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	phplem1OLD 9254	Obsolete lemma for php 9247 as of 22-Nov-2024. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2OLD 9255	Obsolete lemma for php 9247 as of 22-Nov-2024. (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 9256	Obsolete version of phplem1 9244 as of 4-Nov-2024. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem4OLD 9257	Obsolete version of phplem2 9245 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 9258	Obsolete version of nneneq 9246 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	phpOLD 9259	Obsolete version of php 9247 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2OLD 9260	Obsolete version of php2 9248 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3OLD 9261	Obsolete version of php3 9249 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	phpeqdOLD 9262	Obsolete version of phpeqd 9252 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomogOLD 9263	Obsolete version of nndomog 9253 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9269. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	snnen2oOLD 9264	Obsolete version of snnen2o 9273 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 9265	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 5365. (Revised by BTernaryTau, 2-Dec-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onomeneqOLD 9266	Obsolete version of onomeneq 9265 as of 29-Nov-2024. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onfin 9267	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 9268	A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ ω = (On ∩ Fin)
Theorem	nndomo 9269	Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	nnsdomo 9270	Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	sucdom 9271	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 5365. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	sucdomOLD 9272	Obsolete version of sucdom 9271 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	snnen2o 9273	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 5365, ax-un 7755. (Revised by BTernaryTau, 1-Dec-2024.)
⊢ ¬ {𝐴} ≈ 2o
Theorem	0sdom1dom 9274	Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7755, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7755. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	0sdom1domALT 9275	Alternate proof of 0sdom1dom 9274, shorter but requiring ax-un 7755. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	1sdom2 9276	Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7755, see 1sdom2ALT 9277. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7755. (Revised by BTernaryTau, 8-Dec-2024.)
⊢ 1o ≺ 2o
Theorem	1sdom2ALT 9277	Alternate proof of 1sdom2 9276, shorter but requiring ax-un 7755. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1o ≺ 2o
Theorem	sdom1 9278	A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 12-Dec-2024.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	sdom1OLD 9279	Obsolete version of sdom1 9278 as of 12-Dec-2024. (Contributed by Stefan O'Rear, 28-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	modom 9280	Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o)
Theorem	modom2 9281*	Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o)
Theorem	rex2dom 9282*	A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴)
Theorem	1sdom2dom 9283	Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴)
Theorem	1sdom 9284*	A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 9070.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7755. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	1sdomOLD 9285*	Obsolete version of 1sdom 9284 as of 30-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	unxpdomlem1 9286*	Lemma for unxpdom 9289. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
Theorem	unxpdomlem2 9287*	Lemma for unxpdom 9289. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    &   ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏))    &   ⊢ (𝜑 → ¬ 𝑚 = 𝑛)    &   ⊢ (𝜑 → ¬ 𝑠 = 𝑡)    ⇒   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
Theorem	unxpdomlem3 9288*	Lemma for unxpdom 9289. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
Theorem	unxpdom 9289	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 9290	Corollary of unxpdom 9289. (Contributed by NM, 16-Sep-2004.)
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴))
Theorem	sucxpdom 9291	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 9292	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 9293	A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵)
Theorem	ominf 9294	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ ¬ ω ∈ Fin
Theorem	ominfOLD 9295	Obsolete version of ominf 9294 as of 2-Jan-2025. (Contributed by NM, 2-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ω ∈ Fin
Theorem	isinf 9296*	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 5365. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	isinfOLD 9297*	Obsolete version of isinf 9296 as of 2-Jan-2025. (Contributed by Mario Carneiro, 15-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	fineqvlem 9298	Lemma for fineqv 9299. (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 9299	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 9300	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))