P. 91 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dif1enlemOLD 9001	Obsolete version of dif1enlem 9000 as of 5-Jan-2025. (Contributed by BTernaryTau, 18-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc 𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀)
Theorem	rexdif1en 9002*	If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals and avoid ax-un 7630. (Revised by BTernaryTau, 5-Jan-2025.)
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀)
Theorem	rexdif1enOLD 9003*	Obsolete version of rexdif1en 9002 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀)
Theorem	dif1en 9004	If a set 𝐴 is equinumerous to the successor of an ordinal 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5303. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	dif1ennn 9005	If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9121. (Contributed by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	dif1enOLD 9006	Obsolete version of dif1en 9004 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5303. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	findcard 9007*	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 9008*	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 5303. (Revised by BTernaryTau, 26-Aug-2024.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard2s 9009*	Variation of findcard2 9008 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 9010*	Deduction version of findcard2 9008. (Contributed by SO, 16-Jul-2018.)
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	nnfi 9011	Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5303. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)
Theorem	pssnn 9012*	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 5303. (Revised by BTernaryTau, 31-Jul-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)
Theorem	ssnnfi 9013	A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	ssnnfiOLD 9014	Obsolete version of ssnnfi 9013 as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	0fin 9015	The empty set is finite. (Contributed by FL, 14-Jul-2008.)
⊢ ∅ ∈ Fin
Theorem	unfi 9016	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 5303. (Revised by BTernaryTau, 7-Aug-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
Theorem	ssfi 9017	A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5303, see ssfiALT 9018. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5303. (Revised by BTernaryTau, 12-Aug-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	ssfiALT 9018	Shorter proof of ssfi 9017 using ax-pow 5303. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)
Theorem	imafi 9019	Images of finite sets are finite. For a shorter proof using ax-pow 5303, see imafiALT 9189. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5303. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	pwfir 9020	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 9021*	Lemma for pwfi 9022. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5303. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))    ⇒   ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)
Theorem	pwfi 9022	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 5303. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
Theorem	diffi 9023	If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.)
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin)
Theorem	cnvfi 9024	If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5303. (Revised by BTernaryTau, 9-Sep-2024.)
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin)
Theorem	fnfi 9025	A version of fnex 7133 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 9026	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 8811). (Contributed by BTernaryTau, 8-Sep-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1oenfirn 9027	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 9028	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 8812). (Contributed by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1domfi2 9029	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 8809). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	enreffi 9030	Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 8824). (Contributed by BTernaryTau, 8-Sep-2024.)
⊢ (𝐴 ∈ Fin → 𝐴 ≈ 𝐴)
Theorem	ensymfib 9031	Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 8842). (Contributed by BTernaryTau, 9-Sep-2024.)
⊢ (𝐴 ∈ Fin → (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴))
Theorem	entrfil 9032	Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8846). (Contributed by BTernaryTau, 10-Sep-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	enfii 9033	A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5303. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin)
Theorem	enfi 9034	Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5303, see enfiALT 9035. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5303. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
Theorem	enfiALT 9035	Shorter proof of enfi 9034 using ax-pow 5303. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin))
Theorem	domfi 9036	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 9037	Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8846). (Contributed by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	entrfir 9038	Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8846). (Contributed by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	domtrfil 9039	Transitivity of dominance relation when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domtr 8847). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domtrfi 9040	Transitivity of dominance relation when 𝐵 is finite, proved without using the Axiom of Power Sets (unlike domtr 8847). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domtrfir 9041	Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 8847). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	f1imaenfi 9042	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 8854). (Contributed by BTernaryTau, 29-Sep-2024.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	ssdomfi 9043	A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8840). (Contributed by BTernaryTau, 12-Nov-2024.)
⊢ (𝐵 ∈ Fin → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵))
Theorem	ssdomfi2 9044	A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8840). (Contributed by BTernaryTau, 24-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ≼ 𝐵)
Theorem	sbthfilem 9045*	Lemma for sbthfi 9046. (Contributed by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbthfi 9046	Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 8937). (Contributed by BTernaryTau, 4-Nov-2024.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	domnsymfi 9047	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 8943). (Contributed by BTernaryTau, 22-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ≺ 𝐴)
Theorem	sdomdomtrfi 9048	Transitivity of strict dominance and dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 8954). (Contributed by BTernaryTau, 25-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	domsdomtrfi 9049	Transitivity of dominance and strict dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 8956). (Contributed by BTernaryTau, 25-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sucdom2 9050	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 5303. (Revised by BTernaryTau, 4-Dec-2024.)
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵)
2.4.30  Pigeonhole Principle
Theorem	phplem1 9051	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 5303. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2 9052	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 5303. (Revised by BTernaryTau, 4-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵))
Theorem	nneneq 9053	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 5303. (Revised by BTernaryTau, 11-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	php 9054	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 9051, phplem2 9052, nneneq 9053, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5303. (Revised by BTernaryTau, 18-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2 9055	Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5303. (Revised by BTernaryTau, 20-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3 9056	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 5303. (Revised by BTernaryTau, 26-Nov-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php4 9057	Corollary of the Pigeonhole Principle php 9054: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴)
Theorem	php5 9058	Corollary of the Pigeonhole Principle php 9054: 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 9059	Corollary of the Pigeonhole Principle using equality. Strengthening of php 9054 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomog 9060	Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9077 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9077. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5303. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	phplem1OLD 9061	Obsolete lemma for php 9054. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵}))
Theorem	phplem2OLD 9062	Obsolete lemma for php 9054. (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 9063	Obsolete version of phplem1 9051 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 9064	Obsolete version of phplem2 9052 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 9065	Obsolete version of nneneq 9053 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	phpOLD 9066	Obsolete version of php 9054 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)
Theorem	php2OLD 9067	Obsolete version of php2 9055 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	php3OLD 9068	Obsolete version of php3 9056 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴)
Theorem	phpeqdOLD 9069	Obsolete version of phpeqd 9059 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	nndomogOLD 9070	Obsolete version of nndomog 9060 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9077. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	snnen2oOLD 9071	Obsolete version of snnen2o 9081 as of 18-Nov-2024. (Contributed by AV, 6-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ {𝐴} ≈ 2o
2.4.31  Finite sets (cont.)
Theorem	onomeneq 9072	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 5303. (Revised by BTernaryTau, 2-Dec-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onomeneqOLD 9073	Obsolete version of onomeneq 9072 as of 29-Nov-2024. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	onfin 9074	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 9075	A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ ω = (On ∩ Fin)
Theorem	nnfiOLD 9076	Obsolete version of nnfi 9011 as of 23-Sep-2024. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)
Theorem	nndomo 9077	Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	nnsdomo 9078	Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵))
Theorem	sucdom 9079	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 5303. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	sucdomOLD 9080	Obsolete version of sucdom 9079 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵))
Theorem	snnen2o 9081	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 5303, ax-un 7630. (Revised by BTernaryTau, 1-Dec-2024.)
⊢ ¬ {𝐴} ≈ 2o
Theorem	0sdom1dom 9082	Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7630, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7630. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	0sdom1domALT 9083	Alternate proof of 0sdom1dom 9082, shorter but requiring ax-un 7630. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴)
Theorem	1sdom2 9084	Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7630, see 1sdom2ALT 9085. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7630. (Revised by BTernaryTau, 8-Dec-2024.)
⊢ 1o ≺ 2o
Theorem	1sdom2ALT 9085	Alternate proof of 1sdom2 9084, shorter but requiring ax-un 7630. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1o ≺ 2o
Theorem	sdom1 9086	A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5303, ax-un 7630. (Revised by BTernaryTau, 12-Dec-2024.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	sdom1OLD 9087	Obsolete version of sdom1 9086 as of 12-Dec-2024. (Contributed by Stefan O'Rear, 28-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅)
Theorem	modom 9088	Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o)
Theorem	modom2 9089*	Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o)
Theorem	rex2dom 9090*	A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴)
Theorem	1sdom2dom 9091	Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴)
Theorem	1sdom 9092*	A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8874.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7630. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	1sdomOLD 9093*	Obsolete version of 1sdom 9092 as of 30-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦))
Theorem	unxpdomlem1 9094*	Lemma for unxpdom 9097. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩))
Theorem	unxpdomlem2 9095*	Lemma for unxpdom 9097. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    &   ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏))    &   ⊢ (𝜑 → ¬ 𝑚 = 𝑛)    &   ⊢ (𝜑 → ¬ 𝑠 = 𝑡)    ⇒   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))
Theorem	unxpdomlem3 9096*	Lemma for unxpdom 9097. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺)    &   ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩)    ⇒   ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))
Theorem	unxpdom 9097	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 9098	Corollary of unxpdom 9097. (Contributed by NM, 16-Sep-2004.)
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴))
Theorem	sucxpdom 9099	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 9100	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)