P. 367 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36601-36700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bisym1 36601	A symmetry with ↔. See negsym1 36599 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ↔ (𝜓 ↔ ⊥)) → (𝜓 ↔ 𝜑))
Theorem	consym1 36602	A symmetry with ∧. See negsym1 36599 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∧ (𝜓 ∧ ⊥)) → (𝜓 ∧ 𝜑))
Theorem	dissym1 36603	A symmetry with ∨. See negsym1 36599 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∨ (𝜓 ∨ ⊥)) → (𝜓 ∨ 𝜑))
Theorem	nandsym1 36604	A symmetry with ⊼. See negsym1 36599 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ⊼ (𝜓 ⊼ ⊥)) → (𝜓 ⊼ 𝜑))
Theorem	unisym1 36605	A symmetry with ∀. See negsym1 36599 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑥⊥ → ∀𝑥𝜑)
Theorem	exisym1 36606	A symmetry with ∃. See negsym1 36599 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ (∃𝑥∃𝑥⊥ → ∃𝑥𝜑)
Theorem	unqsym1 36607	A symmetry with ∃!. See negsym1 36599 for more information. (Contributed by Anthony Hart, 6-Sep-2011.)
⊢ (∃!𝑥∃!𝑥⊥ → ∃!𝑥𝜑)
Theorem	amosym1 36608	A symmetry with ∃*. See negsym1 36599 for more information. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ (∃*𝑥∃*𝑥⊥ → ∃*𝑥𝜑)
Theorem	subsym1 36609	A symmetry with [𝑥 / 𝑦]. See negsym1 36599 for more information. (Contributed by Anthony Hart, 11-Sep-2011.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]⊥ → [𝑦 / 𝑥]𝜑)
21.15  Mathbox for Chen-Pang He
21.15.1  Ordinal topology
Theorem	ontopbas 36610	An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.)
⊢ (𝐵 ∈ On → 𝐵 ∈ TopBases)
Theorem	onsstopbas 36611	The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015.)
⊢ On ⊆ TopBases
Theorem	onpsstopbas 36612	The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015.)
⊢ On ⊊ TopBases
Theorem	ontgval 36613	The topology generated from an ordinal number 𝐵 is suc ∪ 𝐵. (Contributed by Chen-Pang He, 10-Oct-2015.)
⊢ (𝐵 ∈ On → (topGen‘𝐵) = suc ∪ 𝐵)
Theorem	ontgsucval 36614	The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → (topGen‘suc 𝐴) = suc 𝐴)
Theorem	onsuctop 36615	A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Top)
Theorem	onsuctopon 36616	One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴))
Theorem	ordtoplem 36617	Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆)    ⇒   ⊢ (Ord 𝐴 → (𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆))
Theorem	ordtop 36618	An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽))
Theorem	onsucconni 36619	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ Conn
Theorem	onsucconn 36620	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn)
Theorem	ordtopconn 36621	An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn))
Theorem	onintopssconn 36622	An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (On ∩ Top) ⊆ Conn
Theorem	onsuct0 36623	A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2)
Theorem	ordtopt0 36624	An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2))
Theorem	onsucsuccmpi 36625	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 36626	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 36627	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ Lim 𝐴    ⇒   ⊢ ¬ suc 𝐴 ∈ Comp
Theorem	limsucncmp 36628	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp)
Theorem	ordcmp 36629	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 36630	The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ {1o, 2o} ⊆ (On ∩ Haus)
Theorem	onint1 36631	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 36632	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 36633	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃)))
Theorem	findfvcl 36634*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃)    &   ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃)))    ⇒   ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃))
Theorem	findreccl 36635*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃))
Theorem	findabrcl 36636*	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 36637	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐵 ∈ ℕ → 𝜑)    &   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓)
Theorem	nnssi3 36638	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐶 ∈ ℕ → 𝜑)    &   ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓)
Theorem	nndivsub 36639	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ))
Theorem	nndivlub 36640	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴))
Syntax	cgcdOLD 36641	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD (𝐴, 𝐵)
Definition	df-gcdOLD 36642*	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 36643	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 36644*	Value of the relation constructed in weiunpo 36647, weiunso 36648, weiunfr 36649, and weiunse 36650. (Contributed by Matthew House, 8-Sep-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
Theorem	weiunlem 36645*	Lemma for weiunpo 36647, weiunso 36648, weiunfr 36649, and weiunse 36650. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
Theorem	weiunfrlem 36646*	Lemma for weiunfr 36649. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ 𝐸 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)    &   ⊢ (𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝑟 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋𝐸 / 𝑥⦌𝐵)(𝐹‘𝑡) = 𝐸))
Theorem	weiunpo 36647*	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 36648*	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 36649*	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 36650*	The relation constructed in weiunpo 36647, weiunso 36648, weiunfr 36649, and weiunwe 36651 is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunwe 36651*	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 36652*	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 36653*	Axiom of Transitive Containment, derived as a theorem from ax-ext 2708, ax-rep 5212, and ax-inf2 9562. Use ax-tco 36654 instead. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Axiom	ax-tco 36654*	The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 36653 above and is therefore redundant if we assume ax-ext 2708, ax-rep 5212 and ax-inf2 9562, 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 9656. 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 36655 and axtco1g 36658, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 36656 and axtco2g 36659. The weak form follows directly from the strong form, see axtco2 36656. But the strong form only follows from the weak form if we allow el 5390 or one of its variants, see axtco1from2 36657. 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 36660 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1 36655*	Strong form of the Axiom of Transitive Containment. See ax-tco 36654 for more information. In particular, this theorem generalizes the statement of ax-tco 36654, 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 36656*	Weak form of the Axiom of Transitive Containment. See ax-tco 36654 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 36657*	Strong form axtco1 36655 of the Axiom of Transitive Containment, derived from the weak form axtco2 36656. See ax-tco 36654 for more information. As written, the proof uses ax-pr 5375 via el 5390, but we could alternatively use ax-pow 5307 via elALT2 5311. Use axtco1 36655 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 36658*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36654 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 36659*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36654 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 36660	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 2376. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 36661*	Derivation of ax-un 7689 from ax-tco 36654. Use ax-un 7689 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 36662*	Derivation of ax-nul 5241 from ax-reg 9507 and ax-tco 36654. Use ax-nul 5241 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 36663*	Derivation of el 5390 from ax-tco 36654. Use el 5390 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 36664*	Version of tz9.1c 9651 derived from ax-tco 36654. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 36665*	Version of tz9.1 9650 derived from ax-tco 36654. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.17.3  Transitive closure of a class
Theorem	tr0elw 36666	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 36667. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 36667	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 36668	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 36669*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9656), 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 36708. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 36670	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 36671	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 36672	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 36673	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 36674	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴
Theorem	ttctr 36675	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Tr TC+ 𝐴
Theorem	ttctr2 36676	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctr3 36677	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
Theorem	ttcmin 36678	The transitive closure of 𝐴 is a subclass of every transitive class containing 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → TC+ 𝐴 ⊆ 𝐵)
Theorem	ttcexrg 36679	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 36680	A transitive closure contains the transitive closures of all its subclasses. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcss2 36681	The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel 36682	A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel2 36683	Elements turn into subclasses upon taking transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctrid 36684	The transitive closure of a transitive class is the class itself. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (Tr 𝐴 → TC+ 𝐴 = 𝐴)
Theorem	ttcidm 36685	The transitive closure operation is idempotent. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ TC+ 𝐴 = TC+ 𝐴
Theorem	ssttctr 36686	Transitivity of 𝐴 ⊆ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ TC+ 𝐵 ∧ 𝐵 ⊆ TC+ 𝐶) → 𝐴 ⊆ TC+ 𝐶)
Theorem	elttctr 36687	Transitivity of 𝐴 ∈ TC+ 𝐵 relationship. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ TC+ 𝐵 ∧ 𝐵 ∈ TC+ 𝐶) → 𝐴 ∈ TC+ 𝐶)
Theorem	dfttc2g 36688	A shorter expression for the transitive closure of a set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 = ∪ (rec((𝑥 ∈ V ↦ ∪ 𝑥), 𝐴) “ ω))
Theorem	ttc0 36689	The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∅ = ∅
Theorem	ttc00 36690	A class has an empty transitive closure iff it is the empty set. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = ∅ ↔ TC+ 𝐴 = ∅)
Theorem	csbttc 36691	Distribute proper substitution through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ⦋𝐴 / 𝑥⦌TC+ 𝐵 = TC+ ⦋𝐴 / 𝑥⦌𝐵
Theorem	ttcuniun 36692	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 36693*	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 36694	Distribute union of two classes through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ (𝐴 ∪ 𝐵) = (TC+ 𝐴 ∪ TC+ 𝐵)
Theorem	ttcuni 36695	Distribute union of a class through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝐴 = ∪ TC+ 𝐴
Theorem	ttciun 36696	Distribute indexed union through a transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 TC+ 𝐵
Theorem	ttcpwss 36697	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 36698	The transitive closure is contained in the singleton transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ TC+ {𝐴})
Theorem	ttcsnidg 36699	The singleton transitive closure contains its argument 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ {𝐴})
Theorem	ttcsnmin 36700	The singleton transitive closure is the minimal transitive class containing 𝐴 as an element. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝐵 ∧ Tr 𝐵) → TC+ {𝐴} ⊆ 𝐵)