P. 374 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37301-37400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	onsucconn 37301	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn)
Theorem	ordtopconn 37302	An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn))
Theorem	onintopssconn 37303	An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (On ∩ Top) ⊆ Conn
Theorem	onsuct0 37304	A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2)
Theorem	ordtopt0 37305	An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2))
Theorem	onsucsuccmpi 37306	The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc suc 𝐴 ∈ Comp
Theorem	onsucsuccmp 37307	The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015.)
⊢ (𝐴 ∈ On → suc suc 𝐴 ∈ Comp)
Theorem	limsucncmpi 37308	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ Lim 𝐴    ⇒   ⊢ ¬ suc 𝐴 ∈ Comp
Theorem	limsucncmp 37309	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp)
Theorem	ordcmp 37310	An ordinal topology is compact iff the underlying set is its supremum (union) only when the ordinal is 1o. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 = ∪ ∪ 𝐴 → 𝐴 = 1o)))
Theorem	ssoninhaus 37311	The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ {1o, 2o} ⊆ (On ∩ Haus)
Theorem	onint1 37312	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 37313	The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ (On ∩ Haus) = {1o, 2o}
21.17  Mathbox for Jeff Hoffman
21.17.1  Inferences for finite induction on generic function values
Theorem	fveleq 37314	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃)))
Theorem	findfvcl 37315*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃)    &   ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃)))    ⇒   ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃))
Theorem	findreccl 37316*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃))
Theorem	findabrcl 37317*	Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃) → ((𝑥 ∈ V ↦ (rec(𝐺, 𝐴)‘𝑥))‘𝐶) ∈ 𝑃)
21.17.2  gdc.mm
Theorem	nnssi2 37318	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐵 ∈ ℕ → 𝜑)    &   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓)
Theorem	nnssi3 37319	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐶 ∈ ℕ → 𝜑)    &   ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓)
Theorem	nndivsub 37320	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ))
Theorem	nndivlub 37321	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴))
Syntax	cgcdOLD 37322	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD (𝐴, 𝐵)
Definition	df-gcdOLD 37323*	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 37324	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.18  Mathbox for Matthew House
21.18.1  Relations on well-ordered indexed unions
Theorem	weiunval 37325*	Value of the relation constructed in weiunpo 37328, weiunso 37329, weiunfr 37330, and weiunse 37331. (Contributed by Matthew House, 8-Sep-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
Theorem	weiunlem 37326*	Lemma for weiunpo 37328, weiunso 37329, weiunfr 37330, and weiunse 37331. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
Theorem	weiunfrlem 37327*	Lemma for weiunfr 37330. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ 𝐸 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)    &   ⊢ (𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝑟 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋𝐸 / 𝑥⦌𝐵)(𝐹‘𝑡) = 𝐸))
Theorem	weiunpo 37328*	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 37329*	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 37330*	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 37331*	The relation constructed in weiunpo 37328, weiunso 37329, weiunfr 37330, and weiunwe 37332 is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunwe 37332*	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 37333*	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.18.2  Axiom of Transitive Containment
Theorem	axtco 37334*	Axiom of Transitive Containment, derived as a theorem from ax-ext 2732, ax-rep 5231, and ax-inf2 9643. Use ax-tco 37335 instead. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Axiom	ax-tco 37335*	The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 37334 above and is therefore redundant if we assume ax-ext 2732, ax-rep 5231 and ax-inf2 9643, 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 9737. 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 37336 and axtco1g 37339, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 37337 and axtco2g 37340. The weak form follows directly from the strong form, see axtco2 37337. But the strong form only follows from the weak form if we allow el 5405 or one of its variants, see axtco1from2 37338. 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 37341 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1 37336*	Strong form of the Axiom of Transitive Containment. See ax-tco 37335 for more information. In particular, this theorem generalizes the statement of ax-tco 37335, 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 37337*	Weak form of the Axiom of Transitive Containment. See ax-tco 37335 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 37338*	Strong form axtco1 37336 of the Axiom of Transitive Containment, derived from the weak form axtco2 37337. See ax-tco 37335 for more information. As written, the proof uses ax-pr 5390 via el 5405, but we could alternatively use ax-pow 5326 via elALT2 5330. Use axtco1 37336 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 37339*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 37335 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 37340*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 37335 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 37341	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 2401. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 37342*	Derivation of ax-un 7751 from ax-tco 37335. Use ax-un 7751 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 37343*	Derivation of ax-nul 5259 from ax-reg 9587 and ax-tco 37335. Use ax-nul 5259 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 37344*	Derivation of el 5405 from ax-tco 37335. Use el 5405 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 37345*	Version of tz9.1c 9732 derived from ax-tco 37335. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 37346*	Version of tz9.1 9731 derived from ax-tco 37335. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.18.3  Transitive closure of a class
Theorem	tr0elw 37347	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 37348. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 37348	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 37349	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 37350*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9737), 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 37389. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 37351	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 37352	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 37353	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 37354	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 37355	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴
Theorem	ttctr 37356	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Tr TC+ 𝐴
Theorem	ttctr2 37357	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctr3 37358	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
Theorem	ttcmin 37359	The transitive closure of 𝐴 is a subclass of every transitive class containing 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → TC+ 𝐴 ⊆ 𝐵)
Theorem	ttcexrg 37360	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 37361	A transitive closure contains the transitive closures of all its subclasses. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcss2 37362	The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel 37363	A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel2 37364	Elements turn into subclasses upon taking transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctrid 37365	The transitive closure of a transitive class is the class itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (Tr 𝐴 → TC+ 𝐴 = 𝐴)
Theorem	ttcidm 37366	The transitive closure operation is idempotent. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ TC+ 𝐴 = TC+ 𝐴
Theorem	ssttctr 37367	Transitivity of 𝐴 ⊆ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ TC+ 𝐵 ∧ 𝐵 ⊆ TC+ 𝐶) → 𝐴 ⊆ TC+ 𝐶)
Theorem	elttctr 37368	Transitivity of 𝐴 ∈ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶) → 𝐴 ∈ TC+ 𝐶)
Theorem	dfttc2g 37369	A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ (rec((𝑥 ∈ V ↦ ∪ 𝑥), 𝐴) “ ω))
Theorem	ttc0 37370	The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∅ = ∅
Theorem	ttc00 37371	A class has an empty transitive closure iff it is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = ∅ ↔ TC+ 𝐴 = ∅)
Theorem	csbttc 37372	Distribute proper substitution through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ⦋𝐴 / 𝑥⦌TC+ 𝐵 = TC+ ⦋𝐴 / 𝑥⦌𝐵
Theorem	ttcuniun 37373	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 37374*	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 37375	Distribute union of two classes through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ (𝐴 ∪ 𝐵) = (TC+ 𝐴 ∪ TC+ 𝐵)
Theorem	ttcuni 37376	Distribute union of a class through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴
Theorem	ttciun 37377	Distribute indexed union through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵
Theorem	ttcpwss 37378	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 37379	The transitive closure is contained in the singleton transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ TC+ {𝐴})
Theorem	ttcsnidg 37380	The singleton transitive closure contains its argument 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ {𝐴})
Theorem	ttcsnmin 37381	The singleton transitive closure is the minimal transitive class containing 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝐵 ∧ Tr 𝐵) → TC+ {𝐴} ⊆ 𝐵)
Theorem	ttcsng 37382	Relationship between TC+ {𝐴} and TC+ 𝐴: the former contains the additional element 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ {𝐴} = (TC+ 𝐴 ∪ {𝐴}))
Theorem	ttcsnexg 37383	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 37384	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 37385	The singleton transitive closure of a transitive set is its successor. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ Tr 𝐴) → TC+ {𝐴} = suc 𝐴)
Theorem	dfttc3gw 37386	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 37397. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttcwf 37387	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 37388	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 37389	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 37390	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 37398. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (TC+ 𝐴 ∈ 𝑉 → (𝐴 ≠ ∅ ↔ ∅ ∈ TC+ 𝐴))
Theorem	dfttc4lem1 37391*	Lemma for dfttc4 37393. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∩ 𝐶) ≠ ∅ ∧ ∀𝑧 ∈ 𝐶 ((𝑧 ∩ 𝐶) = ∅ → 𝑧 = 𝐷)) → 𝐷 ∈ 𝐵)
Theorem	dfttc4lem2 37392*	Lemma for dfttc4 37393. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐵 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}    ⇒   ⊢ (𝐴 ⊆ 𝐵 ∧ Tr 𝐵)
Theorem	dfttc4 37393*	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 37394. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = {𝑥 ∣ ∃𝑦((𝐴 ∩ 𝑦) ≠ ∅ ∧ ∀𝑧 ∈ 𝑦 ((𝑧 ∩ 𝑦) = ∅ → 𝑧 = 𝑥))}
Theorem	elttcirr 37394	Irreflexivity of 𝐴 ∈ TC+ 𝐵 relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 37393 to construct a set in which 𝐴 is both ∈-minimal and not ∈-minimal. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ¬ 𝐴 ∈ TC+ 𝐴
Theorem	ttcexg 37395	The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V)
Theorem	ttcexbi 37396	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 37397	The transitive closure of a set 𝐴 is (TC‘𝐴), assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = (TC‘𝐴))
Theorem	ttc0el 37398	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.18.4  Stronger axioms of regularity This section contains some experiments related to the Axiom of Regularity ax-reg 9587. As written, ax-reg 9587 cannot guarantee that all sets are well-founded unless we further assume ax-inf 9640 / ax-inf2 9643; in particular, ax-reg 9587 alone is insufficient to assert that every set has a transitive closure (tz9.1 9731), even though this is true among the hereditarily finite sets. The underlying cause of this issue is that ax-reg 9587 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 9587 so that we get a true "Axiom of Foundation" even in the absence of ax-inf 9640 / ax-inf2 9643 (e.g., so that we can prove unir1 9822 ∪ (𝑅1 “ On) = V)? There are a few possible solutions. First, we can directly strengthen ax-reg 9587 into ax-regs 35843, which asserts that every class {𝑥 ∣ 𝜑} has an ∈-minimal element. Second, we can keep ax-reg 9587 and add ax-tco 37335, which asserts that every set is a member of a transitive set. Third, we can replace ax-reg 9587 with a set-induction axiom mh-setind 37399. Fourth, we can take unir1 9822 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 35843 implies the other three principles: ax-reg 9587 + ax-tco 37335 via axreg 35844 + tz9.1regs 35851, mh-setind 37399 via setindregs 35847, and unir1 9822 via unir1regs 35852. So we just have to show that ax-regs 35843 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 9587 and ax-inf 9640 / ax-inf2 9643? One candidate is mh-setind 37399, with 19 primitives. What is the shortest single axiom not using any wff variables? The conjunction of ax-reg 9587 + ax-tco 37335, expanded using mh-regprimbi 37408 and slightly simplified, comes out to 42 primitives. Can we do better?
Theorem	mh-setind 37399*	Principle of set induction setind 9749, written with primitive symbols. (Contributed by Matthew House, 4-Mar-2026.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → 𝜑)
Theorem	mh-setindnd 37400	A version of mh-setind 37399 with no distinct variable conditions. (Contributed by Matthew House, 5-Mar-2026.) (New usage is discouraged.)
⊢ (∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑦𝜑)) → 𝜑)