P. 356 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	scottsn 35501	Applying Scott's trick to a singleton leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ Scott {𝐴} = {𝐴}
Theorem	scott0b 35502	Applying Scott's trick yields the empty set iff it was applied to the empty set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 = ∅ ↔ Scott 𝐴 = ∅)
Theorem	rankscott 35503	The rank of a nonempty Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ (𝐴 ≠ ∅ → (rank‘Scott 𝐴) = suc ∩ (rank “ 𝐴))
Theorem	rankscottu 35504	An upper bound on the rank of a Scott's trick set. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → (rank‘Scott 𝐵) ⊆ suc (rank‘𝐴))
Theorem	scottssr1 35505	Relationship between a Scott's trick set and the cumulative hierarchy. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → Scott 𝐵 ⊆ (𝑅1‘suc (rank‘𝐴)))
Theorem	acnum 35506	The Axiom of Choice implies that any set is numerable. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (CHOICE → (𝐴 ∈ 𝑉 → 𝐴 ∈ dom card))
21.5.2.1  Finitism
Theorem	prcinf 35507*	Any proper class is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. This proof holds regardless of whether the Axiom of Infinity is accepted or negated. (Contributed by BTernaryTau, 22-Jun-2025.)
⊢ (¬ 𝐴 ∈ V → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	fineqvrep 35508*	If all sets are finite, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
Theorem	fineqvpow 35509*	If all sets are finite, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	fineqvac 35510	If all sets are finite, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5239 and ax-pow 5338, see fineqvacALT 35511. (Contributed by BTernaryTau, 21-Sep-2024.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvacALT 35511	Shorter proof of fineqvac 35510 using ax-rep 5239 and ax-pow 5338. (Contributed by BTernaryTau, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvomon 35512	If all sets are finite, then the class of all natural numbers equals the proper class of all ordinal numbers. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (Fin = V → ω = On)
Theorem	fineqvomonb 35513	All sets are finite iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (Fin = V ↔ ω = On)
Theorem	omprcomonb 35514	The class of all finite ordinals is a proper class iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (¬ ω ∈ V ↔ ω = On)
Theorem	fineqvnttrclselem1 35515*	Lemma for fineqvnttrclse 35518. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ (𝐵 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝐴 +o 𝑑) = 𝐵} ∈ ω)
Theorem	fineqvnttrclselem2 35516*	Lemma for fineqvnttrclse 35518. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵 ∧ 𝐴 ∈ suc suc 𝑁) → (𝐴 +o (𝐹‘𝐴)) = 𝐵)
Theorem	fineqvnttrclselem3 35517*	Lemma for fineqvnttrclse 35518. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    &   ⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵) → ∀𝑎 ∈ suc 𝑁(𝐹‘𝑎)𝑅(𝐹‘suc 𝑎))
Theorem	fineqvnttrclse 35518*	A counterexample demonstrating that ttrclse 9697 does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    ⇒   ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))
Theorem	fineqvinfep 35519*	A counterexample demonstrating that tz9.1 9699 does not hold when all sets are finite and an infinite descending ∈-chain exists. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ 𝐴 = {(𝐹‘∅)}    ⇒   ⊢ ((Fin = V ∧ 𝐹:ω–1-1→V ∧ ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ¬ ∃𝑦(𝐴 ⊆ 𝑦 ∧ Tr 𝑦))
21.5.2.2  Introduce ax-regs
Axiom	ax-regs 35520*	A strong version of the Axiom of Regularity. It states that if there exists a set with property 𝜑, then there must exist a set with property 𝜑 such that none of its elements have property 𝜑. This axiom can be derived from the axioms of ZF set theory as shown in axregs 35533, but this derivation relies on ax-inf2 9611 and is thus not possible in a finitist context. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	axreg 35521*	Derivation of ax-reg 9555 from ax-regs 35520 and Tarski's FOL axiom schemes. This demonstrates the sense in which ax-regs 35520 is a stronger version of ax-reg 9555. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axregscl 35522*	A version of ax-regs 35520 with a class variable instead of a wff variable. Axiom D in Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory (1940), p. 6. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴)))
Theorem	axregszf 35523*	Derivation of zfregs 9702 using ax-regs 35520. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	setindregs 35524*	Set (epsilon) induction. This version of setind 9717 replaces zfregs 9702 with axregszf 35523. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V)
Theorem	setinds2regs 35525*	Principle of set induction (or E-induction). If a property passes from all elements of 𝑥 to 𝑥 itself, then it holds for all 𝑥. (Contributed by BTernaryTau, 31-Dec-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	noinfepfnregs 35526*	There are no infinite descending ∈-chains, proven using ax-regs 35520. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ (𝐹 Fn ω → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))
Theorem	noinfepregs 35527*	There are no infinite descending ∈-chains, proven using ax-regs 35520. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)
Theorem	tz9.1regs 35528*	Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9699 depends on ax-regs 35520 instead of ax-reg 9555 and ax-inf2 9611. This suggests a possible answer to the third question posed in tz9.1 9699, namely that the missing property is that countably infinite classes must obey regularity. In ZF set theory we can prove this by showing that countably infinite classes are sets and thus ax-reg 9555 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35520 is required since countably infinite classes are proper classes. A related candidate for the missing property is the non-existence of infinite descending ∈-chains, proven as noinfep 9630 using ax-reg 9555 and ax-inf2 9611 and as noinfepregs 35527 using ax-regs 35520. If all sets are finite, then the existence of such a chain implies there is a set which does not have a transitive closure, as shown in fineqvinfep 35519. (Contributed by BTernaryTau, 31-Dec-2025.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
Theorem	unir1regs 35529	The cumulative hierarchy of sets covers the universe. This version of unir1 9786 replaces setind 9717 with setindregs 35524. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ ∪ (𝑅1 “ On) = V
Theorem	trssfir1omregs 35530	If every element in a transitive class is finite, then every element is also hereditarily finite. This version of trssfir1om 35488 replaces setinds2 9721 with setinds2regs 35525. (Contributed by BTernaryTau, 20-Jan-2026.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ ∪ (𝑅1 “ ω))
Theorem	r1omhfbregs 35531*	The class of all hereditarily finite sets is the only class with the property that all sets are members of it iff they are finite and all of their elements are members of it. This version of r1omhfb 35489 replaces setinds2 9721 with setinds2regs 35525 and trssfir1om 35488 with trssfir1omregs 35530. (Contributed by BTernaryTau, 21-Jan-2026.)
⊢ (𝐻 = ∪ (𝑅1 “ ω) ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻)))
Theorem	fineqvr1ombregs 35532	All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (Fin = V ↔ ∪ (𝑅1 “ ω) = V)
21.5.2.3  Derive ax-regs
Theorem	axregs 35533*	Derivation of ax-regs 35520 from the axioms of ZF set theory. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.5.2.4  ZFC axioms with reduced distinct variable conditions
Theorem	axsepg2 35534*	A generalization of ax-sep 5258 in which 𝑥 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5258 with the degenerate instance ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 21-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3 35535*	A generalization of ax-sep 5258 in which 𝑦 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5258 with the degenerate instance ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3ALT 35536*	Alternate proof of axsepg3 35535, derived directly from ax-sep 5258 with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg4 35537*	A generalization of ax-sep 5258 that combines axsepg 5259 and axsepg2 35534 into a single theorem scheme. Unlike ax-sep 5258, this scheme lacks a distinct variable condition for 𝜑 and 𝑧 as well as for 𝑥 and 𝑧. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg5 35538*	A generalization of ax-sep 5258 that combines axsepg 5259, axsepg2 35534, and axsepg3 35535 into a single theorem scheme. Unlike ax-sep 5258, this scheme lacks a distinct variable condition for 𝜑 and 𝑧, for 𝑥 and 𝑧, and for 𝑦 and 𝑧. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axnulg 35539	A generalization of ax-nul 5270 in which 𝑥 and 𝑦 need not be distinct. This theorem scheme bundles ax-nul 5270 with the degenerate instance ∃𝑥∀𝑥¬ 𝑥 ∈ 𝑥 which is satisfied by elirrv 9560. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axpowg 35540*	A generalization of ax-pow 5338 that combines it and zfpow 5339 into a single theorem scheme. Unlike ax-pow 5338, this scheme lacks a distinct variable condition for 𝑦 and 𝑤. (Contributed by BTernaryTau, 26-May-2026.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg2 35541*	A generalization of ax-pow 5338 in which 𝑥 and 𝑤 need not be distinct. This theorem scheme bundles ax-pow 5338 with the degenerate instance ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 5396). Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg3 35542*	A generalization of ax-pow 5338 that combines axpowg 35540 and axpowg2 35541 into a single theorem scheme. Unlike ax-pow 5338, this scheme lacks a distinct variable condition for 𝑦 and 𝑤 as well as for 𝑥 and 𝑤. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
21.5.2.5  Cardinality without the Axiom of Choice
Syntax	ckard 35543	Extend class definition to include the alternative cardinal size function.
class kard
Definition	df-kard 35544*	Define the alternative cardinal number function. Under this definition, the cardinal number of a set is the set of all sets equinumerous to it and having the least possible rank. Definition of [Enderton] p. 222. See kardval 35546 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng 35551. Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card 9926. (Contributed by BTernaryTau, 2-Jul-2026.)
⊢ kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})
Theorem	kardfn 35545	The kard class is a function on the universe. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ kard Fn V
Theorem	kardval 35546*	The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval2 35547. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = Scott {𝑥 ∣ 𝑥 ≈ 𝐴}
Theorem	kardval2 35547*	The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval 35546. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	kard0 35548	The kard cardinality of the empty set is the singleton of the empty set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘∅) = {∅}
Theorem	elkarden 35549	Any member of the kard cardinal number of a set is equinumerous to the set. Contrast with cardne 9952 for card cardinals. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ (kard‘𝐵) → 𝐴 ≈ 𝐵)
Theorem	kardeq0 35550	Applying kard to a class yields the empty set iff the class is a proper class. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = ∅ ↔ ¬ 𝐴 ∈ V)
Theorem	kardeng 35551	Two sets are equinumerous iff their kard cardinal numbers are equal. Unlike carden 10536, this theorem does not depend on the Axiom of Choice, but it does depend on the Axiom of Regularity and the Axiom of Infinity. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ 𝑉 → ((kard‘𝐴) = (kard‘𝐵) ↔ 𝐴 ≈ 𝐵))
Theorem	kardenir 35552	If two sets are equinumerous, then their kard cardinal numbers are equal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 → (kard‘𝐴) = (kard‘𝐵))
Theorem	kard0b 35553	The empty set is the only set with cardinality zero. This is the kard version of cardeq0 10537. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = (kard‘∅) ↔ 𝐴 = ∅)
Theorem	kardsn 35554	A singleton has cardinality one. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝑉 → (kard‘{𝐴}) = (kard‘1o))
Theorem	karddom 35555*	One set dominates another iff an element in its kard cardinality dominates an element in the second set's kard cardinality. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≼ 𝑦)
Theorem	kardsdom 35556*	One set strictly dominates another iff an element in its kard cardinality strictly dominates an element in the second set's kard cardinality. (Contributed by BTernaryTau, 6-Jul-2026.)
⊢ (𝐴 ≺ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≺ 𝑦)
Theorem	kardexen 35557*	One set is equinumerous to another iff an element in its kard cardinality is equinumerous to an element in the second set's kard cardinality. See kardeng 35551 for a version with equality of cardinals. (Contributed by BTernaryTau, 7-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≈ 𝑦)
Theorem	kardcard2a 35558	If two sets have equal nonzero card cardinalities, then they have equal kard cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → (kard‘𝐴) = (kard‘𝐵))
Theorem	kardcard2b 35559	If two sets have equal kard cardinalities, then they have equal card cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = (kard‘𝐵) → (card‘𝐴) = (card‘𝐵))
Theorem	kardcard2 35560	Two numerable sets have equal kard cardinalities iff they have equal card cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((kard‘𝐴) = (kard‘𝐵) ↔ (card‘𝐴) = (card‘𝐵)))
Theorem	ackardcard 35561	The Axiom of Choice implies that two sets have equal kard cardinalities iff they have equal card cardinalities. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (CHOICE → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((kard‘𝐴) = (kard‘𝐵) ↔ (card‘𝐴) = (card‘𝐵))))
Theorem	kardcard 35562	Two sets have equal kard cardinalities iff they have equal card cardinalities. This theorem depends on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((kard‘𝐴) = (kard‘𝐵) ↔ (card‘𝐴) = (card‘𝐵)))
Theorem	kardnnfi 35563	The kard cardinal number of a finite ordinal is finite. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ ω → (kard‘𝐴) ∈ Fin)
Theorem	kardfi 35564	The kard cardinal number of a finite set is finite. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ Fin → (kard‘𝐴) ∈ Fin)
Theorem	rankkardu 35565	An upper bound on the rank of a kard cardinal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (rank‘(kard‘𝐴)) ⊆ suc (rank‘𝐴)
Theorem	1enumkard 35566*	The Fundamental Theorem of Enumeration (see https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf), extended to all sets. The expression ∪ 𝑥 ∈ 𝐴({𝑥} × 𝐵) can be thought of as expressing an indexed disjoint union ⊔ 𝑥 ∈ 𝐴𝐵 where each 𝐵 has its elements tagged with the set 𝑥 that generated it. See the comment directly before undjudom 10152 for context on disjoint union as a representation of cardinal addition. This theorem is not limited to numerable sets, but it also does not depend on AC. See 1enumen 35466 for a version that uses equinumerosity , 1enumcard 35467 for a version that uses the card function, and 1enum 35590 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ V → (kard‘𝐴) = (kard‘∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o)))
21.5.2.6  Global choice
Theorem	gblacfnacd 35567*	If 𝐺 is a global choice function, then the Axiom of Choice (in the form of the right-hand side of dfac4 10107) holds. Note that 𝐺 must be a proper class by fndmexb 7904. This means we cannot show that the existence of a class that behaves as a global choice function is sufficient because we only have existential quantifiers for sets, not (proper) classes. However, if a class variant of exlimiv 1960 were available, then it could be used alongside the closed form of this theorem to prove that result. (Contributed by BTernaryTau, 12-Dec-2024.)
⊢ (𝜑 → 𝐺 Fn V)    &   ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    ⇒   ⊢ (𝜑 → ∀𝑥∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
Theorem	onvf1odlem1 35568*	Lemma for onvf1od 35572. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴)
Theorem	onvf1odlem2 35569*	Lemma for onvf1od 35572. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑉 → 𝑁 ∈ ((𝑅1‘𝑀) ∖ 𝐴)))
Theorem	onvf1odlem3 35570*	Lemma for onvf1od 35572. The value of 𝐹 at an ordinal 𝐴. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    &   ⊢ 𝐵 = ∩ {𝑢 ∈ On ∣ ∃𝑣 ∈ (𝑅1‘𝑢) ¬ 𝑣 ∈ (𝐹 “ 𝐴)}    &   ⊢ 𝐶 = (𝐺‘((𝑅1‘𝐵) ∖ (𝐹 “ 𝐴)))    ⇒   ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = 𝐶)
Theorem	onvf1odlem4 35571*	Lemma for onvf1od 35572. If the range of 𝐹 does not exist, then it must equal the universe. (Contributed by BTernaryTau, 4-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    &   ⊢ 𝐵 = ∩ {𝑢 ∈ On ∣ ∃𝑣 ∈ (𝑅1‘𝑢) ¬ 𝑣 ∈ (𝐹 “ 𝑡)}    &   ⊢ 𝐶 = (𝐺‘((𝑅1‘𝐵) ∖ (𝐹 “ 𝑡)))    ⇒   ⊢ (𝜑 → (¬ ran 𝐹 ∈ V → ran 𝐹 = V))
Theorem	onvf1od 35572*	If 𝐺 is a global choice function, then 𝐹 is a bijection from the ordinals to the universe. This is the ZFC version of (1 → 2) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 5-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    ⇒   ⊢ (𝜑 → 𝐹:On–1-1-onto→V)
Theorem	vonf1wev 35573*	If 𝐹 maps the universe one-to-one into the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (6 → 3) which is used in place of (7 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋∃𝐹𝐹:𝑋–1-1→On, but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 11-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V–1-1→On → 𝑅 We V)
Theorem	vonf1owev 35574*	If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (2 → 3) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 6-Dec-2025.) (Proof shortened by BTernaryTau, 11-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V)
Theorem	vonf1owevOLD 35575*	Obsolete version of vonf1owev 35574 as of 11-Jun-2026. (Contributed by BTernaryTau, 6-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V)
Theorem	wevgblacfn 35576*	If 𝑅 is a well-ordering of the universe, then 𝐺 is a global choice function. Here 𝐺 maps each set 𝑧 to its minimal element with respect to 𝑅 (except when 𝑧 is the empty set, in which case it is mapped to the empty set, though this is only done for convenience). This is the ZFC version of (3 → 1) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 29-Jun-2025.)
⊢ 𝐺 = (𝑧 ∈ V ↦ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 We V → (𝐺 Fn V ∧ ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
Theorem	vonf1osev 35577*	If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 is a set-like well-ordering of the universe. This is the ZFC version of (2 → 4) which is used in place of (3 → 4) in https://tinyurl.com/hamkins-gblac. This proof takes advantage of the fact that the well-order constructed in (2 → 3) is also set-like. (Contributed by BTernaryTau, 8-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V–1-1-onto→On → (𝑅 We V ∧ 𝑅 Se V))
Theorem	wevonprcf1o 35578	If 𝑅 is a set-like well-ordering of the universe and 𝐴 is a proper class, then 𝐹 is a bijection from the ordinals to 𝐴. This is the ZFC version of (4 → 5) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 9-Jun-2026.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We V ∧ 𝑅 Se V ∧ ¬ 𝐴 ∈ V) → 𝐹:On–1-1-onto→𝐴)
Theorem	vonf1oonf1 35579	If 𝐹 is a bijection from the universe to the ordinals, then 𝐻 maps 𝐴 one-to-one into the ordinals. This is the ZFC version of (5 → 6) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:𝑋–1-1-onto→On), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. This theorem can also be viewed as (2 → 6). (Contributed by BTernaryTau, 10-Jun-2026.)
⊢ 𝐻 = (𝐹 ↾ 𝐴)    ⇒   ⊢ (𝐹:V–1-1-onto→On → 𝐻:𝐴–1-1→On)
Theorem	vonf1oonfo 35580*	If 𝐹 is a bijection from the ordinals to the universe and 𝐴 is non-empty, then 𝐻 maps the ordinals onto 𝐴. This is the ZFC version of (5 → 8) in https://tinyurl.com/hamkins-gblac, though it neglects to specify that 𝐴 must be non-empty. Note that in NBG set theory the antecedent would be something like ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:𝑋–1-1-onto→On), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. This theorem can also be viewed as (2 → 8). (Contributed by BTernaryTau, 11-Jun-2026.)
⊢ 𝐻 = (𝑥 ∈ On ↦ if((𝐹‘𝑥) ∈ 𝐴, (𝐹‘𝑥), 𝐷))    &   ⊢ 𝐷 = (𝐹‘∩ {𝑦 ∈ On ∣ (𝐹‘𝑦) ∈ 𝐴})    ⇒   ⊢ ((𝐹:On–1-1-onto→V ∧ 𝐴 ≠ ∅) → 𝐻:On–onto→𝐴)
Theorem	onvfowev 35581*	If 𝐹 maps the ordinals onto the universe, then 𝑅 well-orders the universe. This is the ZFC version of (8 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋(𝑋 ≠ ∅ → ∃𝐹𝐹:On–onto→𝑋), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 12-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐻‘𝑥) ∈ (𝐻‘𝑦)}    &   ⊢ 𝐻 = (𝑧 ∈ V ↦ ∩ (◡𝐹 “ {𝑧}))    ⇒   ⊢ (𝐹:On–onto→V → 𝑅 We V)
21.5.3  Real and complex numbers
Theorem	zltp1ne 35582	Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nnltp1ne 35583	Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nn0ltp1ne 35584	Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	0nn0m1nnn0 35585	A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ (𝑁 = 0 ↔ (𝑁 ∈ ℕ0 ∧ ¬ (𝑁 − 1) ∈ ℕ0))
Theorem	f1resfz0f1d 35586	If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:(0...𝐾)⟶𝑉)    &   ⊢ (𝜑 → (𝐹 ↾ (1...𝐾)):(1...𝐾)–1-1→𝑉)    &   ⊢ (𝜑 → ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ∅)    ⇒   ⊢ (𝜑 → 𝐹:(0...𝐾)–1-1→𝑉)
Theorem	fisshasheq 35587	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	revpfxsfxrev 35588	The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr ⟨((♯‘𝑊) − 𝐿), (♯‘𝑊)⟩))
Theorem	swrdrevpfx 35589	A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝐹, 𝐿⟩) = (reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))))
Theorem	1enum 35590*	The Fundamental Theorem of Enumeration. According to Doron Zeilberger (in https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf), this theorem was independently discovered by several anonymous cave-dwellers. Zeilberger also states that "While this formula is still useful after all these years, enumerating specific finite sets is no longer considered mathematics. A genuine mathematical fact has to incorporate infinitely many facts". Fortunately, theorems in Metamath are actually theorem schemes that correspond to an infinite number of object-language theorems, so this concern does not apply to us. See 1enumen 35466 for a version that uses equinumerosity , 1enumcard 35467 for a version that uses the card function, and 1enumkard 35566 for a version that uses the kard function. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ Fin → (♯‘𝐴) = Σ𝑎 ∈ 𝐴 1)
21.5.4  Graph theory
Theorem	lfuhgr 35591*	A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)2 ≤ (♯‘𝑥)))
Theorem	lfuhgr2 35592*	A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)(♯‘𝑥) ≠ 1))
Theorem	lfuhgr3 35593*	A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺)))
Theorem	cplgredgex 35594*	Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))
Theorem	cusgredgex 35595	Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	cusgredgex2 35596	Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	pfxwlk 35597	A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1)))
Theorem	revwlk 35598	The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃))
Theorem	revwlkb 35599	Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023.)
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈) → (𝐹(Walks‘𝐺)𝑃 ↔ (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)))
Theorem	swrdwlk 35600	Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐵 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 substr ⟨𝐵, 𝐿⟩)(Walks‘𝐺)(𝑃 substr ⟨𝐵, (𝐿 + 1)⟩))