P. 358 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35701-35800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nummin 35701*	Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅)
Theorem	1enumen 35702*	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 10227 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 1enumcard 35703 for a version that uses the card function, 1enumkard 35813 for a version that uses the kard function , and 1enum 35873 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ V → 𝐴 ≈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o))
Theorem	1enumcard 35703*	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 10227 for context on disjoint union as a representation of cardinal addition. This theorem does not depend on AC, but it is only meaningful for numerable sets. See 1enumen 35702 and 1enumkard 35813 for versions that are meaningful for non-numerable sets, and see 1enum 35873 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ V → (card‘𝐴) = (card‘∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o)))
Theorem	r11 35704	Value of the cumulative hierarchy of sets function at 1o. (Contributed by BTernaryTau, 24-Jan-2026.)
⊢ (𝑅1‘1o) = 1o
Theorem	r12 35705	Value of the cumulative hierarchy of sets function at 2o. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (𝑅1‘2o) = 2o
Theorem	onrankid 35706	The rank of an ordinal number is itself. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ On ↔ (rank‘𝐴) = 𝐴)
Theorem	rankfilimb 35707*	The rank of a finite well-founded set is less than a limit ordinal iff the ranks of all of its elements are less than that limit ordinal. (Contributed by BTernaryTau, 22-Jan-2026.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ (𝑅1 “ On) ∧ Lim 𝐵) → ((rank‘𝐴) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (rank‘𝑥) ∈ 𝐵))
Theorem	r1filim 35708*	A finite set appears in the cumulative hierarchy prior to a limit ordinal iff all of its elements appear in the cumulative hierarchy prior to that limit ordinal. (Contributed by BTernaryTau, 22-Jan-2026.)
⊢ ((𝐴 ∈ Fin ∧ Lim 𝐵) → (𝐴 ∈ ∪ (𝑅1 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑅1 “ 𝐵)))
Theorem	r1omfi 35709	Obsolete theorem, use hffi 9890 instead. Hereditarily finite sets are finite sets. (Contributed by BTernaryTau, 30-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∪ (𝑅1 “ ω) ⊆ Fin
Theorem	r1omhf 35710*	A set is hereditarily finite iff it is finite and all of its elements are hereditarily finite. (Contributed by BTernaryTau, 19-Jan-2026.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ ω) ↔ (𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝑥 ∈ ∪ (𝑅1 “ ω)))
Theorem	r1ssel 35711	A set is a subset of the value of the cumulative hierarchy of sets function iff it is an element of the value at the successor. (Contributed by BTernaryTau, 15-Jan-2026.)
⊢ (𝐵 ∈ On → (𝐴 ⊆ (𝑅1‘𝐵) ↔ 𝐴 ∈ (𝑅1‘suc 𝐵)))
Theorem	axnulALT3 35712*	Alternate proof of axnul 5259, proved from propositional calculus, ax-gen 1828, ax-4 1842, ax-5 1943, and ax-inf2 9626. (Contributed by BTernaryTau, 22-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axprALT2 35713*	Alternate proof of axpr 5389, proved from predicate calculus, ax-rep 5232, and ax-inf2 9626. (Contributed by BTernaryTau, 26-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	rankfo 35714	The rank function maps the universe onto the ordinals. (Contributed by BTernaryTau, 23-Jun-2026.)
⊢ rank:V–onto→On
Theorem	rankfn 35715	The rank function is a function on the universe. (Contributed by BTernaryTau, 23-Jun-2026.)
⊢ rank Fn V
Theorem	trssfir1om 35716	If every element in a transitive class is finite, then every element is also hereditarily finite. (Contributed by BTernaryTau, 24-Jan-2026.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ ∪ (𝑅1 “ ω))
Theorem	r1omhfb 35717*	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. (Contributed by BTernaryTau, 24-Jan-2026.)
⊢ (𝐻 = ∪ (𝑅1 “ ω) ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻)))
Theorem	scotteqi 35718	Equality theorem for the Scott operation. Inference form of scotteq 9912. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ Scott 𝐴 = Scott 𝐵
Theorem	elscott 35719*	Membership in a Scott's trick set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ Scott 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 (rank‘𝐴) ⊆ (rank‘𝑥)))
Theorem	dfscott2 35720*	Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) = ∩ (rank “ 𝐴)}
Theorem	dfscott3 35721	Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ Scott 𝐴 = (𝐴 ∩ (𝑅1‘suc ∩ (rank “ 𝐴)))
Theorem	elscott2 35722	Membership in a Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ (𝐴 ∈ Scott 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ (rank‘𝐴) = ∩ (rank “ 𝐵)))
Theorem	elscottrank 35723	The rank of an element in a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ (𝐴 ∈ Scott 𝐵 → (rank‘𝐴) = ∩ (rank “ 𝐵))
Theorem	elscottrankeq 35724	Elements in a Scott's trick set have the same rank. (Contributed by BTernaryTau, 9-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶) → (rank‘𝐴) = (rank‘𝐵))
Theorem	elscottrankss 35725	Relationship between the ranks of an element in a Scott's trick set and an element in the input set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵) → (rank‘𝐴) ⊆ (rank‘𝐶))
Theorem	scottrankeqel 35726	If a member of the input set has the same rank as a member of the Scott's trick set, then it is also a member of the Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ (rank‘𝐶) = (rank‘𝐴)) → 𝐶 ∈ Scott 𝐵)
Theorem	nelscottrankgt 35727	If a member of the input set is not a member of the Scott's trick set, then its rank is greater than the rank of a member of the Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵) → (rank‘𝐴) ∈ (rank‘𝐶))
Theorem	scottsn 35728	Applying Scott's trick to a singleton leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ Scott {𝐴} = {𝐴}
Theorem	scott0bOLD 35729	Obsolete version of scott0b 9918 as of 18-Jul-2026. (Contributed by BTernaryTau, 3-Jul-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ ↔ Scott 𝐴 = ∅)
Theorem	rankscott 35730	The rank of a nonempty Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ (𝐴 ≠ ∅ → (rank‘Scott 𝐴) = suc ∩ (rank “ 𝐴))
Theorem	rankscottu 35731	An upper bound on the rank of a Scott's trick set. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → (rank‘Scott 𝐵) ⊆ suc (rank‘𝐴))
Theorem	scottssr1 35732	Relationship between a Scott's trick set and the cumulative hierarchy. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → Scott 𝐵 ⊆ (𝑅1‘suc (rank‘𝐴)))
Theorem	acnum 35733	The Axiom of Choice implies that any set is numerable. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (CHOICE → (𝐴 ∈ 𝑉 → 𝐴 ∈ dom card))
21.5.2.1  Ordinals 5 through 9
Syntax	c5o 35734	Extend the definition of a class to include the ordinal number 5.
class 5o
Syntax	c6o 35735	Extend the definition of a class to include the ordinal number 6.
class 6o
Syntax	c7o 35736	Extend the definition of a class to include the ordinal number 7.
class 7o
Syntax	c8o 35737	Extend the definition of a class to include the ordinal number 8.
class 8o
Syntax	c9o 35738	Extend the definition of a class to include the ordinal number 9.
class 9o
Definition	df-5o 35739	Define the ordinal number 5. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 5o = suc 4o
Definition	df-6o 35740	Define the ordinal number 6. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 6o = suc 5o
Definition	df-7o 35741	Define the ordinal number 7. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 7o = suc 6o
Definition	df-8o 35742	Define the ordinal number 8. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 8o = suc 7o
Definition	df-9o 35743	Define the ordinal number 9. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 9o = suc 8o
Theorem	5on 35744	Ordinal 5 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 5o ∈ On
Theorem	6on 35745	Ordinal 6 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 6o ∈ On
Theorem	7on 35746	Ordinal 7 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 7o ∈ On
Theorem	8on 35747	Ordinal 8 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 8o ∈ On
Theorem	9on 35748	Ordinal 9 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 9o ∈ On
Theorem	5onn 35749	The ordinal 5 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 5o ∈ ω
Theorem	6onn 35750	The ordinal 6 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 6o ∈ ω
Theorem	7onn 35751	The ordinal 7 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 7o ∈ ω
Theorem	8onn 35752	The ordinal 8 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 8o ∈ ω
Theorem	9onn 35753	The ordinal 9 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 9o ∈ ω
21.5.2.2  Finitism
Theorem	prcinf 35754*	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 35755*	If all sets are finite, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
Theorem	fineqvpow 35756*	If all sets are finite, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	fineqvac 35757	If all sets are finite, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5232 and ax-pow 5327, see fineqvacALT 35758. (Contributed by BTernaryTau, 21-Sep-2024.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvacALT 35758	Shorter proof of fineqvac 35757 using ax-rep 5232 and ax-pow 5327. (Contributed by BTernaryTau, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvomon 35759	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 35760	All sets are finite iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (Fin = V ↔ ω = On)
Theorem	omprcomonb 35761	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 35762*	Lemma for fineqvnttrclse 35765. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ (𝐵 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝐴 +o 𝑑) = 𝐵} ∈ ω)
Theorem	fineqvnttrclselem2 35763*	Lemma for fineqvnttrclse 35765. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵 ∧ 𝐴 ∈ suc suc 𝑁) → (𝐴 +o (𝐹‘𝐴)) = 𝐵)
Theorem	fineqvnttrclselem3 35764*	Lemma for fineqvnttrclse 35765. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    &   ⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵) → ∀𝑎 ∈ suc 𝑁(𝐹‘𝑎)𝑅(𝐹‘suc 𝑎))
Theorem	fineqvnttrclse 35765*	A counterexample demonstrating that ttrclse 9712 does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    ⇒   ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))
Theorem	fineqvinfep 35766*	A counterexample demonstrating that tz9.1 9714 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.3  Introduce ax-regs
Axiom	ax-regs 35767*	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 35780, but this derivation relies on ax-inf2 9626 and is thus not possible in a finitist context. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	axreg 35768*	Derivation of ax-reg 9570 from ax-regs 35767 and Tarski's FOL axiom schemes. This demonstrates the sense in which ax-regs 35767 is a stronger version of ax-reg 9570. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axregscl 35769*	A version of ax-regs 35767 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 35770*	Derivation of zfregs 9717 using ax-regs 35767. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	setindregs 35771*	Set (epsilon) induction. This version of setind 9732 replaces zfregs 9717 with axregszf 35770. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V)
Theorem	setinds2regs 35772*	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 35773*	There are no infinite descending ∈-chains, proven using ax-regs 35767. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ (𝐹 Fn ω → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))
Theorem	noinfepregs 35774*	There are no infinite descending ∈-chains, proven using ax-regs 35767. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)
Theorem	tz9.1regs 35775*	Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9714 depends on ax-regs 35767 instead of ax-reg 9570 and ax-inf2 9626. This suggests a possible answer to the third question posed in tz9.1 9714, 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 9570 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35767 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 9645 using ax-reg 9570 and ax-inf2 9626 and as noinfepregs 35774 using ax-regs 35767. 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 35766. (Contributed by BTernaryTau, 31-Dec-2025.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
Theorem	unir1regs 35776	The cumulative hierarchy of sets covers the universe. This version of unir1 9803 replaces setind 9732 with setindregs 35771. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ ∪ (𝑅1 “ On) = V
Theorem	trssfir1omregs 35777	If every element in a transitive class is finite, then every element is also hereditarily finite. This version of trssfir1om 35716 replaces setinds2 9736 with setinds2regs 35772. (Contributed by BTernaryTau, 20-Jan-2026.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ ∪ (𝑅1 “ ω))
Theorem	r1omhfbregs 35778*	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 35717 replaces setinds2 9736 with setinds2regs 35772 and trssfir1om 35716 with trssfir1omregs 35777. (Contributed by BTernaryTau, 21-Jan-2026.)
⊢ (𝐻 = ∪ (𝑅1 “ ω) ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻)))
Theorem	fineqvr1ombregs 35779	All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (Fin = V ↔ ∪ (𝑅1 “ ω) = V)
21.5.2.4  Derive ax-regs
Theorem	axregs 35780*	Derivation of ax-regs 35767 from the axioms of ZF set theory. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.5.2.5  ZFC axioms with reduced distinct variable conditions
Theorem	axsepg2 35781*	A generalization of ax-sep 5249 in which 𝑥 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5249 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 2402. (Contributed by BTernaryTau, 21-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3 35782*	A generalization of ax-sep 5249 in which 𝑦 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5249 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 2402. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3ALT 35783*	Alternate proof of axsepg3 35782, derived directly from ax-sep 5249 with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg4 35784*	A generalization of ax-sep 5249 that combines axsepg 5250 and axsepg2 35781 into a single theorem scheme. Unlike ax-sep 5249, 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 2402. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg5 35785*	A generalization of ax-sep 5249 that combines axsepg 5250, axsepg2 35781, and axsepg3 35782 into a single theorem scheme. Unlike ax-sep 5249, 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 2402. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axnulg 35786	A generalization of ax-nul 5260 in which 𝑥 and 𝑦 need not be distinct. This theorem scheme bundles ax-nul 5260 with the degenerate instance ∃𝑥∀𝑥¬ 𝑥 ∈ 𝑥 which is satisfied by elirrv 9575. Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axpowg 35787*	A generalization of ax-pow 5327 that combines it and zfpow 5328 into a single theorem scheme. Unlike ax-pow 5327, this scheme lacks a distinct variable condition for 𝑦 and 𝑤. (Contributed by BTernaryTau, 26-May-2026.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg2 35788*	A generalization of ax-pow 5327 in which 𝑥 and 𝑤 need not be distinct. This theorem scheme bundles ax-pow 5327 with the degenerate instance ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 5385). Usage of this theorem is discouraged because it depends on ax-13 2402. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg3 35789*	A generalization of ax-pow 5327 that combines axpowg 35787 and axpowg2 35788 into a single theorem scheme. Unlike ax-pow 5327, 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 2402. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
21.5.2.6  Cardinality without the Axiom of Choice
Syntax	ckard 35790	Extend class definition to include the alternative cardinal size function.
class kard
Definition	df-kard 35791*	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 35793 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng 35798. Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card 10001. (Contributed by BTernaryTau, 2-Jul-2026.)
⊢ kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})
Theorem	kardfn 35792	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 35793*	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 35794. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = Scott {𝑥 ∣ 𝑥 ≈ 𝐴}
Theorem	kardval2 35794*	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 35793. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	kard0 35795	The kard cardinality of the empty set is the singleton of the empty set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘∅) = {∅}
Theorem	elkarden 35796	Any member of the kard cardinal number of a set is equinumerous to the set. Contrast with cardne 10027 for card cardinals. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ (kard‘𝐵) → 𝐴 ≈ 𝐵)
Theorem	kardeq0 35797	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 35798	Two sets are equinumerous iff their kard cardinal numbers are equal. Unlike carden 10616, 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 35799	If two sets are equinumerous, then their kard cardinal numbers are equal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 → (kard‘𝐴) = (kard‘𝐵))
Theorem	kard0b 35800	The empty set is the only set with cardinality zero. This is the kard version of cardeq0 10617. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = (kard‘∅) ↔ 𝐴 = ∅)