P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axtco2 37101*	Weak form of the Axiom of Transitive Containment. See ax-tco 37099 for more information. In particular, this theorem shows the derivation of the weak form from the strong form. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
Theorem	axtco1from2 37102*	Strong form axtco1 37100 of the Axiom of Transitive Containment, derived from the weak form axtco2 37101. See ax-tco 37099 for more information. As written, the proof uses ax-pr 5402 via el 5417, but we could alternatively use ax-pow 5334 via elALT2 5338. Use axtco1 37100 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 37103*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 37099 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 37104*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 37099 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 37105	A version of the Axiom of Transitive Containment with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2403. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 37106*	Derivation of ax-un 7740 from ax-tco 37099. Use ax-un 7740 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 37107*	Derivation of ax-nul 5267 from ax-reg 9568 and ax-tco 37099. Use ax-nul 5267 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 37108*	Derivation of el 5417 from ax-tco 37099. Use el 5417 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 37109*	Version of tz9.1c 9713 derived from ax-tco 37099. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 37110*	Version of tz9.1 9712 derived from ax-tco 37099. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.17.3  Transitive closure of a class
Theorem	tr0elw 37111	Every nonempty transitive set contains the empty set ∅ as an element, a consequence of Regularity. If we assume Transitive Containment, then we can omit the 𝐴 ∈ 𝑉 hypothesis, see tr0el 37112. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 37112	Every nonempty transitive class contains the empty set ∅ as an element, a consequence of Regularity and Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Syntax	cttc 37113	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 37114*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9718), this definition works even if 𝐴 or its transitive closure is a proper class. Note that unless we assume Transitive Containment, the transitive closure of a set may be a proper class. If we only assume Regularity, then the class of sets whose transitive closure is a set is precisely the class of well-founded sets, see ttcwf3 37153. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 37115	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 37116	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 37117	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 37118	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 37119	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴
Theorem	ttctr 37120	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Tr TC+ 𝐴
Theorem	ttctr2 37121	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctr3 37122	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
Theorem	ttcmin 37123	The transitive closure of 𝐴 is a subclass of every transitive class containing 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → TC+ 𝐴 ⊆ 𝐵)
Theorem	ttcexrg 37124	If the transitive closure of a class is a set, then the class is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → 𝐴 ∈ V)
Theorem	ttcss 37125	A transitive closure contains the transitive closures of all its subclasses. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcss2 37126	The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel 37127	A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel2 37128	Elements turn into subclasses upon taking transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctrid 37129	The transitive closure of a transitive class is the class itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (Tr 𝐴 → TC+ 𝐴 = 𝐴)
Theorem	ttcidm 37130	The transitive closure operation is idempotent. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ TC+ 𝐴 = TC+ 𝐴
Theorem	ssttctr 37131	Transitivity of 𝐴 ⊆ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ TC+ 𝐵 ∧ 𝐵 ⊆ TC+ 𝐶) → 𝐴 ⊆ TC+ 𝐶)
Theorem	elttctr 37132	Transitivity of 𝐴 ∈ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶) → 𝐴 ∈ TC+ 𝐶)
Theorem	dfttc2g 37133	A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ (rec((𝑥 ∈ V ↦ ∪ 𝑥), 𝐴) “ ω))
Theorem	ttc0 37134	The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∅ = ∅
Theorem	ttc00 37135	A class has an empty transitive closure iff it is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = ∅ ↔ TC+ 𝐴 = ∅)
Theorem	csbttc 37136	Distribute proper substitution through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ⦋𝐴 / 𝑥⦌TC+ 𝐵 = TC+ ⦋𝐴 / 𝑥⦌𝐵
Theorem	ttcuniun 37137	Relationship between TC+ 𝐴 and TC+ ∪ 𝐴: we can decompose TC+ 𝐴 into the elements of TC+ ∪ 𝐴 plus the elements of 𝐴 itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = (TC+ ∪ 𝐴 ∪ 𝐴)
Theorem	ttciunun 37138*	Relationship between TC+ 𝐴 and ∪ 𝑥 ∈ 𝐴TC+ 𝑥: we can decompose TC+ 𝐴 into the elements of ∪ 𝑥 ∈ 𝐴TC+ 𝑥 plus the elements of 𝐴 itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = (∪ 𝑥 ∈ 𝐴 TC+ 𝑥 ∪ 𝐴)
Theorem	ttcun 37139	Distribute union of two classes through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ (𝐴 ∪ 𝐵) = (TC+ 𝐴 ∪ TC+ 𝐵)
Theorem	ttcuni 37140	Distribute union of a class through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴
Theorem	ttciun 37141	Distribute indexed union through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵
Theorem	ttcpwss 37142	The transitive closure of a power class is contained in the power class of the transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝒫 𝐴 ⊆ 𝒫 TC+ 𝐴
Theorem	ttcsnssg 37143	The transitive closure is contained in the singleton transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ TC+ {𝐴})
Theorem	ttcsnidg 37144	The singleton transitive closure contains its argument 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ {𝐴})
Theorem	ttcsnmin 37145	The singleton transitive closure is the minimal transitive class containing 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝐵 ∧ Tr 𝐵) → TC+ {𝐴} ⊆ 𝐵)
Theorem	ttcsng 37146	Relationship between TC+ {𝐴} and TC+ 𝐴: the former contains the additional element 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ {𝐴} = (TC+ 𝐴 ∪ {𝐴}))
Theorem	ttcsnexg 37147	If the transitive closure of a class is a set, then its singleton transitive closure is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ {𝐴} ∈ V)
Theorem	ttcsnexbig 37148	The transitive closure of a set is a set iff its singleton transitive closure is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → (TC+ 𝐴 ∈ V ↔ TC+ {𝐴} ∈ V))
Theorem	ttcsntrsucg 37149	The singleton transitive closure of a transitive set is its successor. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ Tr 𝐴) → TC+ {𝐴} = suc 𝐴)
Theorem	dfttc3gw 37150	If the transitive closure of 𝐴 is a set, then its value is (TC‘𝐴). If we assume Transitive Containment, then we can weaken the hypothesis to 𝐴 ∈ 𝑉, see dfttc3g 37161. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttcwf 37151	A set is well-founded iff its transitive closure is well-founded. As a corollary, the transitive closure of any well-founded set is a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ TC+ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	ttcwf2 37152	If a transitive closure class is a set, then it is well-founded, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ V ↔ TC+ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	ttcwf3 37153	The sets whose transitive closures are sets are precisely the well-founded sets, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ V ↔ 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	ttc0elw 37154	If a transitive closure is a set, then it contains ∅ as an element iff it is nonempty, assuming Regularity. If we also assume Transitive Containment, then we can remove the TC+ 𝐴 ∈ 𝑉 hypothesis, see ttc0el 37162. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴))
Theorem	dfttc4lem1 37155*	Lemma for dfttc4 37157. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∩ 𝐶) ≠ ∅ ∧ ∀𝑧 ∈ 𝐶 ((𝑧 ∩ 𝐶) = ∅ → 𝑧 = 𝐷)) → 𝐷 ∈ 𝐵)
Theorem	dfttc4lem2 37156*	Lemma for dfttc4 37157. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    ⇒   ⊢ (𝐴 ⊆ 𝐵 ∧ Tr 𝐵)
Theorem	dfttc4 37157*	An alternative expression for the transitive closure of a class, assuming Regularity. A set 𝑥 is contained in the transitive closure of 𝐴 iff we can construct an ∈-chain from 𝑥 to an element of 𝐴. This weak definition is primarily useful for proving elttcirr 37158. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}
Theorem	elttcirr 37158	Irreflexivity of 𝐴 ∈ TC+ 𝐵 relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 37157 to construct a set in which 𝐴 is both ∈-minimal and not ∈-minimal. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ¬ 𝐴 ∈ TC+ 𝐴
Theorem	ttcexg 37159	The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V)
Theorem	ttcexbi 37160	A class is a set iff its transitive closure is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ V ↔ TC+ 𝐴 ∈ V)
Theorem	dfttc3g 37161	The transitive closure of a set 𝐴 is (TC‘𝐴), assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttc0el 37162	A transitive closure contains ∅ as an element iff it is nonempty, assuming Regularity and Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴)
21.17.4  Stronger axioms of regularity This section contains some experiments related to the Axiom of Regularity ax-reg 9568. As written, ax-reg 9568 cannot guarantee that all sets are well-founded unless we further assume ax-inf 9621 / ax-inf2 9624; in particular, ax-reg 9568 alone is insufficient to assert that every set has a transitive closure (tz9.1 9712), even though this is true among the hereditarily finite sets. The underlying cause of this issue is that ax-reg 9568 requires a witness set to detect non-well-foundedness, but if all sets are hereditarily finite, then there may be no such witness set for an infinite descending ∈-chain. The question is, how can we strengthen ax-reg 9568 so that we get a true "Axiom of Foundation" even in the absence of ax-inf 9621 / ax-inf2 9624 (e.g., so that we can prove unir1 9799 ∪ (𝑅1 “ On) = V)? There are a few possible solutions. First, we can directly strengthen ax-reg 9568 into ax-regs 35660, which asserts that every class {𝑥 ∣ 𝜑} has an ∈-minimal element. Second, we can keep ax-reg 9568 and add ax-tco 37099, which asserts that every set is a member of a transitive set. Third, we can replace ax-reg 9568 with a set-induction axiom mh-setind 37163. Fourth, we can take unir1 9799 as an axiom and derive everything from that. This list is far from exhaustive. In this section, we prove that these four listed principles are equivalent. We see that ax-regs 35660 implies the other three principles: ax-reg 9568 + ax-tco 37099 via axreg 35661 + tz9.1regs 35668, mh-setind 37163 via setindregs 35664, and unir1 9799 via unir1regs 35669. So we just have to show that ax-regs 35660 is implied by each of the other three. Some questions: When expanded to primitives, what is the shortest single axiom equivalent to these, over ZF minus ax-reg 9568 and ax-inf 9621 / ax-inf2 9624? One candidate is mh-setind 37163, with 19 primitives. What is the shortest single axiom not using any wff variables? The conjunction of ax-reg 9568 + ax-tco 37099, expanded using mh-regprimbi 37172 and slightly simplified, comes out to 42 primitives. Can we do better?
Theorem	mh-setind 37163*	Principle of set induction setind 9730, written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → 𝜑)
Theorem	mh-setindnd 37164	A version of mh-setind 37163 with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026.) (New usage is discouraged.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑦𝜑)) → 𝜑)
Theorem	regsfromregtco 37165*	Derivation of ax-regs 35660 from ax-reg 9568 + ax-tco 37099. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∃𝑦 𝑦 ∈ 𝑤 → ∃𝑦(𝑦 ∈ 𝑤 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤)))    &   ⊢ ∃𝑢(𝑣 ∈ 𝑢 ∧ ∀𝑡(𝑡 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢)))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromsetind 37166*	Derivation of ax-regs 35660 from mh-setind 37163. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) → ¬ 𝜑)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromunir1 37167*	Derivation of ax-regs 35660 from unir1 9799. (Contributed by Matthew House, 4-Mar-2026.)
⊢ ∪ (𝑅1 “ On) = V    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.17.5  Short axioms written in primitive symbols
Theorem	mh-inf3f1 37168	A variant of inf3 9618. If 𝐹 is a one-to-one function from 𝐴 into itself, and there exists an element 𝐵 not in its range, then (rec(𝐹, 𝐵) ↾ ω) is an infinite sequence of distinct elements from 𝐴. If 𝐴 is a set, we can use this theorem to prove ω ∈ V via f1dmex 7958. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)
Theorem	mh-inf3sn 37169*	Version of inf3 9618 for the set of Zermelo ordinals ∅, {∅}, {{∅}}, {{{∅}}}, etc., where the successor of 𝑦 is {𝑦}. Unlike inf3 9618, the proof does not require ax-reg 9568, since the singleton properties snnz 4740 and sneqr 4803 are sufficient to guarantee that all elements of the sequence are distinct. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	mh-prprimbi 37170*	Shortest possible version of ax-pr 5402 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ¬ ∀𝑧(𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧))
Theorem	mh-unprimbi 37171*	Shortest possible version of ax-un 7740 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	mh-regprimbi 37172*	Shortest possible version of ax-reg 9568 in primitive symbols. The equivalence is nontrivial, but it still follows solely from the axioms of predicate calculus. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ((∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) ↔ ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim1bi 37173*	Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf 9621 or ax-inf2 9624 from this axiom requires ax-ext 2734, ax-rep 5236, and ax-reg 9568, see inf3 9618 and inf0 9604. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim2bi 37174*	Shortest possible axiom of infinity in primitive symbols not requiring ax-reg 9568. Deriving ax-inf 9621 or ax-inf2 9624 from this axiom requires ax-ext 2734 and ax-rep 5236, see mh-inf3sn 37169 and inf0 9604. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑦 → ¬ (𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧)) → 𝑦 ∈ 𝑥))
Theorem	mh-infprim3bi 37175*	An axiom of infinity in primitive symbols not requiring ax-reg 9568. This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines 9568. It directly implies ax-inf 9621, but deriving ax-inf2 9624 requires ax-ext 2734 and ax-rep 5236, see mh-inf3sn 37169. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 {𝑧} ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ¬ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧 ¬ ¬ (𝑧 ∈ 𝑦 → ¬ ∀𝑦 ¬ ((𝑦 ∈ 𝑧 → 𝑦 = 𝑥) → ¬ (𝑦 = 𝑥 → 𝑦 ∈ 𝑧))))))
21.18  Mathbox for Asger C. Ipsen
21.18.1  Continuous nowhere differentiable functions
Theorem	dnival 37176*	Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))
Theorem	dnicld1 37177	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)
Theorem	dnicld2 37178*	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ)
Theorem	dnif 37179	The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇:ℝ⟶ℝ
Theorem	dnizeq0 37180*	The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) = 0)
Theorem	dnizphlfeqhlf 37181*	The distance to nearest integer is a half for half-integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘(𝐴 + (1 / 2))) = (1 / 2))
Theorem	rddif2 37182	Variant of rddif 15432. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))
Theorem	dnibndlem1 37183*	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆))
Theorem	dnibndlem2 37184*	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem3 37185	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) + (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))))
Theorem	dnibndlem4 37186	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem5 37187	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem6 37188	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))))
Theorem	dnibndlem7 37189	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem8 37190	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem9 37191*	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem10 37192	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴))
Theorem	dnibndlem11 37193	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2))
Theorem	dnibndlem12 37194*	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem13 37195*	Lemma for dnibnd 37196. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibnd 37196*	The "distance to nearest integer" function is 1-Lipschitz continuous, i.e., is a short map. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnicn 37197	The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇 ∈ (ℝ–cn→ℝ)
Theorem	knoppcnlem1 37198*	Lemma for knoppcn 37209. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))
Theorem	knoppcnlem2 37199*	Lemma for knoppcn 37209. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ)
Theorem	knoppcnlem3 37200*	Lemma for knoppcn 37209. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) ∈ ℝ)