P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	onint1 37001	The ordinal T1 spaces are 1o and 2o, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015.)
⊢ (On ∩ Fre) = {1o, 2o}
Theorem	oninhaus 37002	The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ (On ∩ Haus) = {1o, 2o}
21.16  Mathbox for Jeff Hoffman
21.16.1  Inferences for finite induction on generic function values
Theorem	fveleq 37003	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃)))
Theorem	findfvcl 37004*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃)    &   ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃)))    ⇒   ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃))
Theorem	findreccl 37005*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃))
Theorem	findabrcl 37006*	Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃) → ((𝑥 ∈ V ↦ (rec(𝐺, 𝐴)‘𝑥))‘𝐶) ∈ 𝑃)
21.16.2  gdc.mm
Theorem	nnssi2 37007	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐵 ∈ ℕ → 𝜑)    &   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓)
Theorem	nnssi3 37008	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐶 ∈ ℕ → 𝜑)    &   ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓)
Theorem	nndivsub 37009	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ))
Theorem	nndivlub 37010	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴))
Syntax	cgcdOLD 37011	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD (𝐴, 𝐵)
Definition	df-gcdOLD 37012*	gcdOLD (𝐴, 𝐵) is the largest positive integer that evenly divides both 𝐴 and 𝐵. (Contributed by Jeff Hoffman, 17-Jun-2008.) (New usage is discouraged.)
⊢ gcdOLD (𝐴, 𝐵) = sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )
Theorem	ee7.2aOLD 37013	Lemma for Euclid's Elements, Book 7, proposition 2. The original mentions the smaller measure being 'continually subtracted' from the larger. Many authors interpret this phrase as 𝐴 mod 𝐵. Here, just one subtraction step is proved to preserve the gcdOLD. The rec function will be used in other proofs for iterated subtraction. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 → gcdOLD (𝐴, 𝐵) = gcdOLD (𝐴, (𝐵 − 𝐴))))
21.17  Mathbox for Matthew House
21.17.1  Relations on well-ordered indexed unions
Theorem	weiunval 37014*	Value of the relation constructed in weiunpo 37017, weiunso 37018, weiunfr 37019, and weiunse 37020. (Contributed by Matthew House, 8-Sep-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
Theorem	weiunlem 37015*	Lemma for weiunpo 37017, weiunso 37018, weiunfr 37019, and weiunse 37020. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
Theorem	weiunfrlem 37016*	Lemma for weiunfr 37019. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ 𝐸 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)    &   ⊢ (𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝑟 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋𝐸 / 𝑥⦌𝐵)(𝐹‘𝑡) = 𝐸))
Theorem	weiunpo 37017*	A partial ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of partial orderings on its members. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Po 𝐵) → 𝑇 Po ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunso 37018*	A strict ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of strict orderings on its members. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Or 𝐵) → 𝑇 Or ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunfr 37019*	A well-founded relation on an indexed union can be constructed from a well-ordering on its index class and a collection of well-founded relations on its members. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunse 37020*	The relation constructed in weiunpo 37017, weiunso 37018, weiunfr 37019, and weiunwe 37021 is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunwe 37021*	A well-ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 We 𝐵) → 𝑇 We ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	numiunnum 37022*	An indexed union of sets is numerable if its index set is numerable and there exists a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025.)
⊢ ((𝐴 ∈ dom card ∧ ∀𝑥 ∈ 𝐴 (𝐵 ∈ 𝑉 ∧ 𝑆 We 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ dom card)
21.17.2  Axiom of Transitive Containment
Theorem	axtco 37023*	Axiom of Transitive Containment, derived as a theorem from ax-ext 2738, ax-rep 5243, and ax-inf2 9620. Use ax-tco 37024 instead. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Axiom	ax-tco 37024*	The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 37023 above and is therefore redundant if we assume ax-ext 2738, ax-rep 5243 and ax-inf2 9620, 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 9714. 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 37025 and axtco1g 37028, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 37026 and axtco2g 37029. The weak form follows directly from the strong form, see axtco2 37026. But the strong form only follows from the weak form if we allow el 5424 or one of its variants, see axtco1from2 37027. 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 37030 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1 37025*	Strong form of the Axiom of Transitive Containment. See ax-tco 37024 for more information. In particular, this theorem generalizes the statement of ax-tco 37024, 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 37026*	Weak form of the Axiom of Transitive Containment. See ax-tco 37024 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 37027*	Strong form axtco1 37025 of the Axiom of Transitive Containment, derived from the weak form axtco2 37026. See ax-tco 37024 for more information. As written, the proof uses ax-pr 5409 via el 5424, but we could alternatively use ax-pow 5341 via elALT2 5345. Use axtco1 37025 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 37028*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 37024 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 37029*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 37024 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 37030	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 2407. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 37031*	Derivation of ax-un 7745 from ax-tco 37024. Use ax-un 7745 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 37032*	Derivation of ax-nul 5274 from ax-reg 9564 and ax-tco 37024. Use ax-nul 5274 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 37033*	Derivation of el 5424 from ax-tco 37024. Use el 5424 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 37034*	Version of tz9.1c 9709 derived from ax-tco 37024. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 37035*	Version of tz9.1 9708 derived from ax-tco 37024. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.17.3  Transitive closure of a class
Theorem	tr0elw 37036	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 37037. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 37037	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 37038	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 37039*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9714), 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 37078. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 37040	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 37041	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 37042	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 37043	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 37044	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴
Theorem	ttctr 37045	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Tr TC+ 𝐴
Theorem	ttctr2 37046	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctr3 37047	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
Theorem	ttcmin 37048	The transitive closure of 𝐴 is a subclass of every transitive class containing 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → TC+ 𝐴 ⊆ 𝐵)
Theorem	ttcexrg 37049	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 37050	A transitive closure contains the transitive closures of all its subclasses. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcss2 37051	The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel 37052	A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel2 37053	Elements turn into subclasses upon taking transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctrid 37054	The transitive closure of a transitive class is the class itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (Tr 𝐴 → TC+ 𝐴 = 𝐴)
Theorem	ttcidm 37055	The transitive closure operation is idempotent. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ TC+ 𝐴 = TC+ 𝐴
Theorem	ssttctr 37056	Transitivity of 𝐴 ⊆ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ TC+ 𝐵 ∧ 𝐵 ⊆ TC+ 𝐶) → 𝐴 ⊆ TC+ 𝐶)
Theorem	elttctr 37057	Transitivity of 𝐴 ∈ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶) → 𝐴 ∈ TC+ 𝐶)
Theorem	dfttc2g 37058	A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ (rec((𝑥 ∈ V ↦ ∪ 𝑥), 𝐴) “ ω))
Theorem	ttc0 37059	The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∅ = ∅
Theorem	ttc00 37060	A class has an empty transitive closure iff it is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = ∅ ↔ TC+ 𝐴 = ∅)
Theorem	csbttc 37061	Distribute proper substitution through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ⦋𝐴 / 𝑥⦌TC+ 𝐵 = TC+ ⦋𝐴 / 𝑥⦌𝐵
Theorem	ttcuniun 37062	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 37063*	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 37064	Distribute union of two classes through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ (𝐴 ∪ 𝐵) = (TC+ 𝐴 ∪ TC+ 𝐵)
Theorem	ttcuni 37065	Distribute union of a class through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴
Theorem	ttciun 37066	Distribute indexed union through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵
Theorem	ttcpwss 37067	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 37068	The transitive closure is contained in the singleton transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ TC+ {𝐴})
Theorem	ttcsnidg 37069	The singleton transitive closure contains its argument 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ {𝐴})
Theorem	ttcsnmin 37070	The singleton transitive closure is the minimal transitive class containing 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝐵 ∧ Tr 𝐵) → TC+ {𝐴} ⊆ 𝐵)
Theorem	ttcsng 37071	Relationship between TC+ {𝐴} and TC+ 𝐴: the former contains the additional element 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ {𝐴} = (TC+ 𝐴 ∪ {𝐴}))
Theorem	ttcsnexg 37072	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 37073	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 37074	The singleton transitive closure of a transitive set is its successor. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ Tr 𝐴) → TC+ {𝐴} = suc 𝐴)
Theorem	dfttc3gw 37075	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 37086. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttcwf 37076	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 37077	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 37078	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 37079	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 37087. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴))
Theorem	dfttc4lem1 37080*	Lemma for dfttc4 37082. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∩ 𝐶) ≠ ∅ ∧ ∀𝑧 ∈ 𝐶 ((𝑧 ∩ 𝐶) = ∅ → 𝑧 = 𝐷)) → 𝐷 ∈ 𝐵)
Theorem	dfttc4lem2 37081*	Lemma for dfttc4 37082. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    ⇒   ⊢ (𝐴 ⊆ 𝐵 ∧ Tr 𝐵)
Theorem	dfttc4 37082*	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 37083. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}
Theorem	elttcirr 37083	Irreflexivity of 𝐴 ∈ TC+ 𝐵 relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 37082 to construct a set in which 𝐴 is both ∈-minimal and not ∈-minimal. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ¬ 𝐴 ∈ TC+ 𝐴
Theorem	ttcexg 37084	The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V)
Theorem	ttcexbi 37085	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 37086	The transitive closure of a set 𝐴 is (TC‘𝐴), assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttc0el 37087	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 9564. As written, ax-reg 9564 cannot guarantee that all sets are well-founded unless we further assume ax-inf 9617 / ax-inf2 9620; in particular, ax-reg 9564 alone is insufficient to assert that every set has a transitive closure (tz9.1 9708), even though this is true among the hereditarily finite sets. The underlying cause of this issue is that ax-reg 9564 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 9564 so that we get a true "Axiom of Foundation" even in the absence of ax-inf 9617 / ax-inf2 9620 (e.g., so that we can prove unir1 9795 ∪ (𝑅1 “ On) = V)? There are a few possible solutions. First, we can directly strengthen ax-reg 9564 into ax-regs 35563, which asserts that every class {𝑥 ∣ 𝜑} has an ∈-minimal element. Second, we can keep ax-reg 9564 and add ax-tco 37024, which asserts that every set is a member of a transitive set. Third, we can replace ax-reg 9564 with a set-induction axiom mh-setind 37088. Fourth, we can take unir1 9795 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 35563 implies the other three principles: ax-reg 9564 + ax-tco 37024 via axreg 35564 + tz9.1regs 35571, mh-setind 37088 via setindregs 35567, and unir1 9795 via unir1regs 35572. So we just have to show that ax-regs 35563 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 9564 and ax-inf 9617 / ax-inf2 9620? One candidate is mh-setind 37088, with 19 primitives. What is the shortest single axiom not using any wff variables? The conjunction of ax-reg 9564 + ax-tco 37024, expanded using mh-regprimbi 37097 and slightly simplified, comes out to 42 primitives. Can we do better?
Theorem	mh-setind 37088*	Principle of set induction setind 9726, written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → 𝜑)
Theorem	mh-setindnd 37089	A version of mh-setind 37088 with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026.) (New usage is discouraged.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑦𝜑)) → 𝜑)
Theorem	regsfromregtco 37090*	Derivation of ax-regs 35563 from ax-reg 9564 + ax-tco 37024. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∃𝑦 𝑦 ∈ 𝑤 → ∃𝑦(𝑦 ∈ 𝑤 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑤)))    &   ⊢ ∃𝑢(𝑣 ∈ 𝑢 ∧ ∀𝑡(𝑡 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑡 → 𝑠 ∈ 𝑢)))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromsetind 37091*	Derivation of ax-regs 35563 from mh-setind 37088. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) → ¬ 𝜑)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	regsfromunir1 37092*	Derivation of ax-regs 35563 from unir1 9795. (Contributed by Matthew House, 4-Mar-2026.)
⊢ ∪ (𝑅1 “ On) = V    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.17.5  Short axioms written in primitive symbols
Theorem	mh-inf3f1 37093	A variant of inf3 9614. 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 7963. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))    ⇒   ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)
Theorem	mh-inf3sn 37094*	Version of inf3 9614 for the set of Zermelo ordinals ∅, {∅}, {{∅}}, {{{∅}}}, etc., where the successor of 𝑦 is {𝑦}. Unlike inf3 9614, the proof does not require ax-reg 9564, since the singleton properties snnz 4747 and sneqr 4810 are sufficient to guarantee that all elements of the sequence are distinct. (Contributed by Matthew House, 13-Apr-2026.)
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥)    ⇒   ⊢ ω ∈ V
Theorem	mh-prprimbi 37095*	Shortest possible version of ax-pr 5409 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ¬ ∀𝑧(𝑥 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑧))
Theorem	mh-unprimbi 37096*	Shortest possible version of ax-un 7745 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	mh-regprimbi 37097*	Shortest possible version of ax-reg 9564 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 37098*	Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf 9617 or ax-inf2 9620 from this axiom requires ax-ext 2738, ax-rep 5243, and ax-reg 9564, see inf3 9614 and inf0 9600. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦 ¬ ∀𝑧((𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧) → ¬ 𝑧 ∈ 𝑥))
Theorem	mh-infprim2bi 37099*	Shortest possible axiom of infinity in primitive symbols not requiring ax-reg 9564. Deriving ax-inf 9617 or ax-inf2 9620 from this axiom requires ax-ext 2738 and ax-rep 5243, see mh-inf3sn 37094 and inf0 9600. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {𝑦} ∈ 𝑥) ↔ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑦 → ¬ (𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧)) → 𝑦 ∈ 𝑥))
Theorem	mh-infprim3bi 37100*	An axiom of infinity in primitive symbols not requiring ax-reg 9564. This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines 9564. It directly implies ax-inf 9617, but deriving ax-inf2 9620 requires ax-ext 2738 and ax-rep 5243, see mh-inf3sn 37094. (Contributed by Matthew House, 13-Apr-2026.)
⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 {𝑧} ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ¬ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧 ¬ ¬ (𝑧 ∈ 𝑦 → ¬ ∀𝑦 ¬ ((𝑦 ∈ 𝑧 → 𝑦 = 𝑥) → ¬ (𝑦 = 𝑥 → 𝑦 ∈ 𝑧))))))