P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abweex 35801*	The class of well-orders of a set 𝐴 and its subsets is a set. (Contributed by BTernaryTau, 2-Aug-2026.)
⊢ (𝐴 ∈ 𝑉 → {𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ∈ V)
Theorem	ordtypeon 35802	A proper class with a set-like well-ordering is isomorphic to the proper class of all ordinal numbers. (Contributed by BTernaryTau, 9-Jun-2026.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V) → 𝐹 Isom E , 𝑅 (On, 𝐴))
Theorem	onf1we 35803*	If 𝐹 maps 𝐴 one-to-one into the ordinals, then 𝑅 well-orders 𝐴. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:𝐴⟶1-1On → 𝑅 We 𝐴)
Theorem	fnrelpredd 35804*	A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐹‘𝑥)𝑆(𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Pred(𝑆, (𝐹 “ 𝐶), (𝐹‘𝐷)) = (𝐹 “ Pred(𝑅, 𝐶, 𝐷)))
Theorem	cardpred 35805	The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card) → Pred( E , (card “ 𝐴), (card‘𝐵)) = (card “ Pred( ≺ , 𝐴, 𝐵)))
Theorem	nummin 35806*	Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅)
Theorem	1enumen 35807*	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 10273 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 35808 for a version that uses the card function, 1enumkard 35940 for a version that uses the kard function , and 1enum 36061 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ V → 𝐴 ≈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o))
Theorem	1enumcard 35808*	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 10273 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 35807 and 1enumkard 35940 for versions that are meaningful for non-numerable sets, and see 1enum 36061 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ V → (card‘𝐴) = (card‘∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o)))
Theorem	r11 35809	Value of the cumulative hierarchy of sets function at 1o. (Contributed by BTernaryTau, 24-Jan-2026.)
⊢ (𝑅1‘1o) = 1o
Theorem	r12 35810	Value of the cumulative hierarchy of sets function at 2o. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (𝑅1‘2o) = 2o
Theorem	onrankid 35811	The rank of an ordinal number is itself. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ On ↔ (rank‘𝐴) = 𝐴)
Theorem	rankfilimb 35812*	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 35813*	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	r1ssel 35814	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 35815*	Alternate proof of axnul 5262, proved from propositional calculus, ax-gen 1828, ax-4 1842, ax-5 1945, and ax-inf2 9669. (Contributed by BTernaryTau, 22-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axprALT2 35816*	Alternate proof of axpr 5393, proved from predicate calculus, ax-rep 5235, and ax-inf2 9669. (Contributed by BTernaryTau, 26-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	rankfo 35817	The rank function maps the universe onto the ordinals. (Contributed by BTernaryTau, 23-Jun-2026.)
⊢ rank:V⟶ontoOn
Theorem	rankfn 35818	The rank function is a function on the universe. (Contributed by BTernaryTau, 23-Jun-2026.)
⊢ rank Fn V
Theorem	trssfihf 35819	If every element in a transitive class is finite, then every element is also hereditarily finite. (Contributed by BTernaryTau, 24-Jan-2026.) Use HF. (Revised by BTernaryTau, 24-Oct-2026.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ HF )
Theorem	eqhf 35820*	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.) Use HF. (Revised by BTernaryTau, 24-Oct-2026.)
⊢ (𝐻 = HF ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻)))
Theorem	werankwe 35821*	Construct a well-order given a relation 𝑅(𝑥) that well-orders elements of the same rank. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((rank‘𝑥) ∈ (rank‘𝑦) ∨ ((rank‘𝑥) = (rank‘𝑦) ∧ 𝑥𝑅𝑦))}    &   ⊢ (𝑤 = (rank‘𝑥) → 𝑇 = 𝑅)    &   ⊢ (𝑣 = 𝑥 → 𝑈 = 𝑅)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝑅 We {𝑧 ∈ 𝐴 ∣ (rank‘𝑧) = (rank‘𝑥)} → 𝑆 We 𝐴)
Theorem	werankwe2 35822*	Construct a well-order given a relation that well-orders elements of the same rank. See werankwe 35821 for a version where 𝑅 can depend on 𝑤. (Contributed by BTernaryTau, 18-Sep-2026.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((rank‘𝑥) ∈ (rank‘𝑦) ∨ ((rank‘𝑥) = (rank‘𝑦) ∧ 𝑥𝑅𝑦))}    ⇒   ⊢ (∀𝑤 ∈ 𝐴 𝑅 We {𝑧 ∈ 𝐴 ∣ (rank‘𝑧) = (rank‘𝑤)} → 𝑆 We 𝐴)
Theorem	rankse 35823*	Construct a relation that is set-like on any class. (Contributed by BTernaryTau, 18-Sep-2026.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((rank‘𝑥) ∈ (rank‘𝑦) ∨ ((rank‘𝑥) = (rank‘𝑦) ∧ 𝜑))}    ⇒   ⊢ 𝑆 Se 𝐴
Theorem	scotteqi 35824	Equality theorem for the Scott operation. Inference form of scotteq 9958. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ Scott 𝐴 = Scott 𝐵
Theorem	elscott 35825*	Membership in a Scott's trick set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ Scott 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 (rank‘𝐴) ⊆ (rank‘𝑥)))
Theorem	dfscott2 35826*	Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) = ∩ (rank “ 𝐴)}
Theorem	dfscott3 35827	Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ Scott 𝐴 = (𝐴 ∩ (𝑅1‘suc ∩ (rank “ 𝐴)))
Theorem	elscott2 35828	Membership in a Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ (𝐴 ∈ Scott 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ (rank‘𝐴) = ∩ (rank “ 𝐵)))
Theorem	elscottrank 35829	The rank of an element in a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ (𝐴 ∈ Scott 𝐵 → (rank‘𝐴) = ∩ (rank “ 𝐵))
Theorem	elscottrankeq 35830	Elements in a Scott's trick set have the same rank. (Contributed by BTernaryTau, 9-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶) → (rank‘𝐴) = (rank‘𝐵))
Theorem	elscottrankss 35831	Relationship between the ranks of an element in a Scott's trick set and an element in the input class. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵) → (rank‘𝐴) ⊆ (rank‘𝐶))
Theorem	scottrankeqel 35832	If a member of the input class 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 35833	If a member of the input class 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 35834	Applying Scott's trick to a singleton leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ Scott {𝐴} = {𝐴}
Theorem	scott0bOLD 35835	Obsolete version of scott0b 9964 as of 18-Jul-2026. (Contributed by BTernaryTau, 3-Jul-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ ↔ Scott 𝐴 = ∅)
Theorem	elscottn0 35836	If the input class has elements, then the Scott's trick set is not empty. (Contributed by BTernaryTau, 23-Aug-2026.)
⊢ (𝐴 ∈ 𝐵 → Scott 𝐵 ≠ ∅)
Theorem	0elscott 35837	If the empty set is an element of the input class, then the Scott's trick set is the singleton of the empty set. (Contributed by BTernaryTau, 23-Aug-2026.)
⊢ (∅ ∈ 𝐴 → Scott 𝐴 = {∅})
Theorem	rankscott 35838	The rank of a nonempty Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ (𝐴 ≠ ∅ → (rank‘Scott 𝐴) = suc ∩ (rank “ 𝐴))
Theorem	rankscottu 35839	An upper bound on the rank of a Scott's trick set. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → (rank‘Scott 𝐵) ⊆ suc (rank‘𝐴))
Theorem	scottssr1 35840	Relationship between a Scott's trick set and the cumulative hierarchy. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → Scott 𝐵 ⊆ (𝑅1‘suc (rank‘𝐴)))
Theorem	scottidm 35841	The Scott operation is idempotent. (Contributed by BTernaryTau, 23-Aug-2026.)
⊢ Scott Scott 𝐴 = Scott 𝐴
Theorem	trscott 35842	The Scott's trick set of a transitive class is also transitive. (Contributed by BTernaryTau, 20-Oct-2026.)
⊢ (Tr 𝐴 → Tr Scott 𝐴)
Theorem	erscottd 35843*	Applying the Scott operation to equivalence classes preserves their equality property. (Contributed by BTernaryTau, 20-Oct-2026.)
⊢ (𝜑 → 𝑅 Er 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ Scott {𝑥 ∣ 𝑥𝑅𝐴} = Scott {𝑥 ∣ 𝑥𝑅𝐵}))
Theorem	ecscottd 35844	Applying the Scott operation to equivalence classes preserves their equality property. (Contributed by BTernaryTau, 20-Oct-2026.)
⊢ (𝜑 → 𝑅 Er 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ Scott [𝐴]𝑅 = Scott [𝐵]𝑅))
Theorem	dfac15 35845*	Axiom of Choice equivalent: every set can be mapped one-to-one into the ordinals. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓 𝑓:𝑥⟶1-1On)
Theorem	dfac16 35846*	Axiom of Choice equivalent: for every pair of sets, one is dominated by the other (see also entri3 10670). (Contributed by BTernaryTau, 17-Sep-2026.)
⊢ (CHOICE ↔ ∀𝑥∀𝑦(𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥))
Theorem	acnum 35847	The Axiom of Choice implies that any set is numerable. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (CHOICE → (𝐴 ∈ 𝑉 → 𝐴 ∈ dom card))
Theorem	weexenwe 35848*	If a well-ordering of an infinite set exists, then a well-ordering equinumerous to the set exists. (Contributed by BTernaryTau, 31-Jul-2026.)
⊢ ((∃𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴) → ∃𝑠(𝑠 ⊆ (𝐴 × 𝐴) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴))
Theorem	infinfnum 35849	Equivalence between two infiniteness criteria for numerable sets. (Contributed by BTernaryTau, 15-Jul-2026.)
⊢ (𝐴 ∈ dom card → (¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴))
Theorem	rncardr1prc 35850	The Axiom of Choice implies that the cardinalities of the layers of the cumulative hierarchy form a proper class. (Contributed by BTernaryTau, 2-Jul-2026.)
⊢ (CHOICE → ¬ ran (card ∘ 𝑅1) ∈ V)
Theorem	acwer1prclem 35851*	Lemma for acwer1prc 35852. (Contributed by BTernaryTau, 31-Jul-2026.)
⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    ⇒   ⊢ ((CHOICE ∧ ω ≼ 𝐴 ∧ (card‘(𝑅1‘𝐵)) = 𝐴) → ∃𝑠((card‘𝑠) ∈ (card “ 𝑊) ∧ (card‘𝑠) = 𝐴))
Theorem	acwer1prc 35852*	The class of all well-orderings of the stages of the cumulative hierarchy is a proper class. (Contributed by BTernaryTau, 31-Jul-2026.)
⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    ⇒   ⊢ (CHOICE → ¬ 𝑊 ∈ V)
21.6.2.1  Ordinals 5 through 9
Syntax	c5o 35853	Extend the definition of a class to include the ordinal number 5.
class 5o
Syntax	c6o 35854	Extend the definition of a class to include the ordinal number 6.
class 6o
Syntax	c7o 35855	Extend the definition of a class to include the ordinal number 7.
class 7o
Syntax	c8o 35856	Extend the definition of a class to include the ordinal number 8.
class 8o
Syntax	c9o 35857	Extend the definition of a class to include the ordinal number 9.
class 9o
Definition	df-5o 35858	Define the ordinal number 5. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 5o = suc 4o
Definition	df-6o 35859	Define the ordinal number 6. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 6o = suc 5o
Definition	df-7o 35860	Define the ordinal number 7. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 7o = suc 6o
Definition	df-8o 35861	Define the ordinal number 8. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 8o = suc 7o
Definition	df-9o 35862	Define the ordinal number 9. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 9o = suc 8o
Theorem	5on 35863	Ordinal 5 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 5o ∈ On
Theorem	6on 35864	Ordinal 6 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 6o ∈ On
Theorem	7on 35865	Ordinal 7 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 7o ∈ On
Theorem	8on 35866	Ordinal 8 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 8o ∈ On
Theorem	9on 35867	Ordinal 9 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 9o ∈ On
Theorem	5onn 35868	The ordinal 5 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 5o ∈ ω
Theorem	6onn 35869	The ordinal 6 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 6o ∈ ω
Theorem	7onn 35870	The ordinal 7 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 7o ∈ ω
Theorem	8onn 35871	The ordinal 8 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 8o ∈ ω
Theorem	9onn 35872	The ordinal 9 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 9o ∈ ω
Theorem	8olt9o 35873	Ordinal 8 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 8o ∈ 9o
Theorem	7olt9o 35874	Ordinal 7 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 7o ∈ 9o
Theorem	6olt9o 35875	Ordinal 6 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 6o ∈ 9o
Theorem	5olt9o 35876	Ordinal 5 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 5o ∈ 9o
Theorem	4olt9o 35877	Ordinal 4 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 4o ∈ 9o
Theorem	3olt9o 35878	Ordinal 3 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 3o ∈ 9o
Theorem	2olt9o 35879	Ordinal 2 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 2o ∈ 9o
Theorem	1olt9o 35880	Ordinal 1 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ 1o ∈ 9o
21.6.2.2  Finitism
Theorem	prcinf 35881*	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 35882*	If all sets are finite, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
Theorem	fineqvpow 35883*	If all sets are finite, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	fineqvac 35884	If all sets are finite, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5235 and ax-pow 5331, see fineqvacALT 35885. (Contributed by BTernaryTau, 21-Sep-2024.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvacALT 35885	Shorter proof of fineqvac 35884 using ax-rep 5235 and ax-pow 5331. (Contributed by BTernaryTau, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvomon 35886	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 35887	All sets are finite iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (Fin = V ↔ ω = On)
Theorem	omprcomonb 35888	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 35889*	Lemma for fineqvnttrclse 35892. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ (𝐵 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝐴 +o 𝑑) = 𝐵} ∈ ω)
Theorem	fineqvnttrclselem2 35890*	Lemma for fineqvnttrclse 35892. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵 ∧ 𝐴 ∈ suc suc 𝑁) → (𝐴 +o (𝐹‘𝐴)) = 𝐵)
Theorem	fineqvnttrclselem3 35891*	Lemma for fineqvnttrclse 35892. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    &   ⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵) → ∀𝑎 ∈ suc 𝑁(𝐹‘𝑎)𝑅(𝐹‘suc 𝑎))
Theorem	fineqvnttrclse 35892*	A counterexample demonstrating that ttrclse 9755 does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    ⇒   ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))
Theorem	fineqvinfep 35893*	A counterexample demonstrating that tz9.1 9757 does not hold when all sets are finite and an infinite descending ∈-chain exists. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ 𝐴 = {(𝐹‘∅)}    ⇒   ⊢ ((Fin = V ∧ 𝐹:ω⟶1-1V ∧ ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ¬ ∃𝑦(𝐴 ⊆ 𝑦 ∧ Tr 𝑦))
21.6.2.3  Introduce ax-regs
Axiom	ax-regs 35894*	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 35907, but this derivation relies on ax-inf2 9669 and is thus not possible in a finitist context. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	axreg 35895*	Derivation of ax-reg 9613 from ax-regs 35894 and Tarski's FOL axiom schemes. This demonstrates the sense in which ax-regs 35894 is a stronger version of ax-reg 9613. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axregscl 35896*	A version of ax-regs 35894 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 35897*	Derivation of zfregs 9760 using ax-regs 35894. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	setindregs 35898*	Set (epsilon) induction. This version of setind 9775 replaces zfregs 9760 with axregszf 35897. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V)
Theorem	setinds2regs 35899*	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 35900*	There are no infinite descending ∈-chains, proven using ax-regs 35894. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ (𝐹 Fn ω → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))