P. 368 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-tco 36701*	The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 36700 above and is therefore redundant if we assume ax-ext 2712, ax-rep 5206 and ax-inf2 9560, but we state it as a separate axiom here so that its uses can be identified more easily. It states that a transitive set 𝑦 exists that contains a given set 𝑥. In particular, the transitive closure of 𝑥 is a set, since it is a subset of 𝑦, see df-tc 9654. Traditionally, this statement is not counted as an axiom at all, but as a theorem from Replacement and Infinity. In fact, from the transitive closure of 𝑥 we can construct the set of iterated unions of 𝑥 (and vice versa), and Skolem took the existence of the latter set as a motivation for introducing the Axiom of Replacement. But Transitive Containment is strictly weaker than either of those axioms, so many authors identify it as its own axiom when investigating subsystems of ZF, such as Zermelo set theory or finitist set theory. We follow this separation in order to avoid nonessential usage of the stronger axioms. There are two main versions of this axiom that appear in the literature: the strong form ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ Tr 𝑦), see axtco1 36702 and axtco1g 36705, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 36703 and axtco2g 36706. The weak form follows directly from the strong form, see axtco2 36703. But the strong form only follows from the weak form if we allow el 5384 or one of its variants, see axtco1from2 36704. We take the strong form here as the axiom, since it is slightly shorter when expanded to primitive symbols. Yet the weak form turns out to be more suitable for axtcond 36707 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1 36702*	Strong form of the Axiom of Transitive Containment. See ax-tco 36701 for more information. In particular, this theorem generalizes the statement of ax-tco 36701, allowing it to be written with only three variables, since 𝑥 need not be distinct from both 𝑧 and 𝑤. (Contributed by Matthew House, 7-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco2 36703*	Weak form of the Axiom of Transitive Containment. See ax-tco 36701 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 36704*	Strong form axtco1 36702 of the Axiom of Transitive Containment, derived from the weak form axtco2 36703. See ax-tco 36701 for more information. As written, the proof uses ax-pr 5369 via el 5384, but we could alternatively use ax-pow 5301 via elALT2 5305. Use axtco1 36702 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 36705*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36701 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 36706*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36701 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 36707	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 2380. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 36708*	Derivation of ax-un 7685 from ax-tco 36701. Use ax-un 7685 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 36709*	Derivation of ax-nul 5235 from ax-reg 9504 and ax-tco 36701. Use ax-nul 5235 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 36710*	Derivation of el 5384 from ax-tco 36701. Use el 5384 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 36711*	Version of tz9.1c 9649 derived from ax-tco 36701. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 36712*	Version of tz9.1 9648 derived from ax-tco 36701. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.17.3  Transitive closure of a class
Theorem	tr0elw 36713	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 36714. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 36714	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 36715	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 36716*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9654), 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 36755. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 36717	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 36718	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 36719	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 36720	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 36721	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴
Theorem	ttctr 36722	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Tr TC+ 𝐴
Theorem	ttctr2 36723	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctr3 36724	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
Theorem	ttcmin 36725	The transitive closure of 𝐴 is a subclass of every transitive class containing 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → TC+ 𝐴 ⊆ 𝐵)
Theorem	ttcexrg 36726	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 36727	A transitive closure contains the transitive closures of all its subclasses. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcss2 36728	The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel 36729	A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel2 36730	Elements turn into subclasses upon taking transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctrid 36731	The transitive closure of a transitive class is the class itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (Tr 𝐴 → TC+ 𝐴 = 𝐴)
Theorem	ttcidm 36732	The transitive closure operation is idempotent. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ TC+ 𝐴 = TC+ 𝐴
Theorem	ssttctr 36733	Transitivity of 𝐴 ⊆ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ TC+ 𝐵 ∧ 𝐵 ⊆ TC+ 𝐶) → 𝐴 ⊆ TC+ 𝐶)
Theorem	elttctr 36734	Transitivity of 𝐴 ∈ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶) → 𝐴 ∈ TC+ 𝐶)
Theorem	dfttc2g 36735	A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ (rec((𝑥 ∈ V ↦ ∪ 𝑥), 𝐴) “ ω))
Theorem	ttc0 36736	The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∅ = ∅
Theorem	ttc00 36737	A class has an empty transitive closure iff it is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = ∅ ↔ TC+ 𝐴 = ∅)
Theorem	csbttc 36738	Distribute proper substitution through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ⦋𝐴 / 𝑥⦌TC+ 𝐵 = TC+ ⦋𝐴 / 𝑥⦌𝐵
Theorem	ttcuniun 36739	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 36740*	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 36741	Distribute union of two classes through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ (𝐴 ∪ 𝐵) = (TC+ 𝐴 ∪ TC+ 𝐵)
Theorem	ttcuni 36742	Distribute union of a class through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴
Theorem	ttciun 36743	Distribute indexed union through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵
Theorem	ttcpwss 36744	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 36745	The transitive closure is contained in the singleton transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ TC+ {𝐴})
Theorem	ttcsnidg 36746	The singleton transitive closure contains its argument 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ {𝐴})
Theorem	ttcsnmin 36747	The singleton transitive closure is the minimal transitive class containing 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝐵 ∧ Tr 𝐵) → TC+ {𝐴} ⊆ 𝐵)
Theorem	ttcsng 36748	Relationship between TC+ {𝐴} and TC+ 𝐴: the former contains the additional element 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ {𝐴} = (TC+ 𝐴 ∪ {𝐴}))
Theorem	ttcsnexg 36749	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 36750	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 36751	The singleton transitive closure of a transitive set is its successor. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ Tr 𝐴) → TC+ {𝐴} = suc 𝐴)
Theorem	dfttc3gw 36752	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 36763. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttcwf 36753	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 36754	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 36755	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 36756	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 36764. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴))
Theorem	dfttc4lem1 36757*	Lemma for dfttc4 36759. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∩ 𝐶) ≠ ∅ ∧ ∀𝑧 ∈ 𝐶 ((𝑧 ∩ 𝐶) = ∅ → 𝑧 = 𝐷)) → 𝐷 ∈ 𝐵)
Theorem	dfttc4lem2 36758*	Lemma for dfttc4 36759. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    ⇒   ⊢ (𝐴 ⊆ 𝐵 ∧ Tr 𝐵)
Theorem	dfttc4 36759*	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 36760. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}
Theorem	elttcirr 36760	Irreflexivity of 𝐴 ∈ TC+ 𝐵 relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 36759 to construct a set in which 𝐴 is both ∈-minimal and not ∈-minimal. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ¬ 𝐴 ∈ TC+ 𝐴
Theorem	ttcexg 36761	The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V)
Theorem	ttcexbi 36762	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 36763	The transitive closure of a set 𝐴 is (TC‘𝐴), assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttc0el 36764	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 9504. As written, ax-reg 9504 cannot guarantee that all sets are well-founded unless we further assume ax-inf 9557 / ax-inf2 9560; in particular, ax-reg 9504 alone is insufficient to assert that every set has a transitive closure (tz9.1 9648), even though this is true among the hereditarily finite sets. The underlying cause of this issue is that ax-reg 9504 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 9504 so that we get a true "Axiom of Foundation" even in the absence of ax-inf 9557 / ax-inf2 9560 (e.g., so that we can prove unir1 9735 ∪ (𝑅1 “ On) = V)? There are a few possible solutions. First, we can directly strengthen ax-reg 9504 into ax-regs 35317, which asserts that every class {𝑥 ∣ 𝜑} has an ∈-minimal element. Second, we can keep ax-reg 9504 and add ax-tco 36701, which asserts that every set is a member of a transitive set. Third, we can replace ax-reg 9504 with a set-induction axiom mh-setind 36765. Fourth, we can take unir1 9735 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 35317 implies the other three principles: ax-reg 9504 + ax-tco 36701 via axreg 35318 + tz9.1regs 35325, mh-setind 36765 via setindregs 35321, and unir1 9735 via unir1regs 35326. So we just have to show that ax-regs 35317 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 9504 and ax-inf 9557 / ax-inf2 9560? One candidate is mh-setind 36765, with 19 primitives. What is the shortest single axiom not using any wff variables? The conjunction of ax-reg 9504 + ax-tco 36701, expanded using mh-regprimbi 36774 and slightly simplified, comes out to 42 primitives. Can we do better?
Theorem	mh-setind 36765*	Principle of set induction setind 9666, written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → 𝜑)
Theorem	mh-setindnd 36766	A version of mh-setind 36765 with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026.) (New usage is discouraged.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑦𝜑)) → 𝜑)
Theorem	regsfromregtco 36767*	Derivation of ax-regs 35317 from ax-reg 9504 + ax-tco 36701. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∃𝑦 𝑦 ∈ 𝑤 → ∃𝑦(𝑦 ∈ 𝑤 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤)))    &   ⊢ ∃𝑢(𝑣 ∈ 𝑢 ∧ ∀𝑡(𝑡 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢)))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromsetind 36768*	Derivation of ax-regs 35317 from mh-setind 36765. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) → ¬ 𝜑)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromunir1 36769*	Derivation of ax-regs 35317 from unir1 9735. (Contributed by Matthew House, 4-Mar-2026.)
⊢ ∪ (𝑅1 “ On) = V    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.17.5  Short axioms written in primitive symbols
Theorem	mh-inf3f1 36770	A variant of inf3 9554. 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 7906. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)
Theorem	mh-inf3sn 36771*	Version of inf3 9554 for the set of Zermelo ordinals ∅, {∅}, {{∅}}, {{{∅}}}, etc., where the successor of 𝑦 is {𝑦}. Unlike inf3 9554, the proof does not require ax-reg 9504, since the singleton properties snnz 4715 and sneqr 4778 are sufficient to guarantee that all elements of the sequence are distinct. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	mh-prprimbi 36772*	Shortest possible version of ax-pr 5369 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ¬ ∀𝑧(𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧))
Theorem	mh-unprimbi 36773*	Shortest possible version of ax-un 7685 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	mh-regprimbi 36774*	Shortest possible version of ax-reg 9504 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 36775*	Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf 9557 or ax-inf2 9560 from this axiom requires ax-ext 2712, ax-rep 5206, and ax-reg 9504, see inf3 9554 and inf0 9540. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim2bi 36776*	Shortest possible axiom of infinity in primitive symbols not requiring ax-reg 9504. Deriving ax-inf 9557 or ax-inf2 9560 from this axiom requires ax-ext 2712 and ax-rep 5206, see mh-inf3sn 36771 and inf0 9540. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑦 → ¬ (𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧)) → 𝑦 ∈ 𝑥))
Theorem	mh-infprim3bi 36777*	An axiom of infinity in primitive symbols not requiring ax-reg 9504. This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines 9504. It directly implies ax-inf 9557, but deriving ax-inf2 9560 requires ax-ext 2712 and ax-rep 5206, see mh-inf3sn 36771. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 {𝑧} ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ¬ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧 ¬ ¬ (𝑧 ∈ 𝑦 → ¬ ∀𝑦 ¬ ((𝑦 ∈ 𝑧 → 𝑦 = 𝑥) → ¬ (𝑦 = 𝑥 → 𝑦 ∈ 𝑧))))))
21.18  Mathbox for Asger C. Ipsen
21.18.1  Continuous nowhere differentiable functions
Theorem	dnival 36778*	Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))
Theorem	dnicld1 36779	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)
Theorem	dnicld2 36780*	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ)
Theorem	dnif 36781	The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇:ℝ⟶ℝ
Theorem	dnizeq0 36782*	The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) = 0)
Theorem	dnizphlfeqhlf 36783*	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 36784	Variant of rddif 15301. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))
Theorem	dnibndlem1 36785*	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆))
Theorem	dnibndlem2 36786*	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem3 36787	Lemma for dnibnd 36798. (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 36788	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem5 36789	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem6 36790	Lemma for dnibnd 36798. (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 36791	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem8 36792	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem9 36793*	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem10 36794	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴))
Theorem	dnibndlem11 36795	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2))
Theorem	dnibndlem12 36796*	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem13 36797*	Lemma for dnibnd 36798. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐴 + (1 / 2))) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibnd 36798*	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 36799	The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇 ∈ (ℝ–cn→ℝ)
Theorem	knoppcnlem1 36800*	Lemma for knoppcn 36811. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))