P. 369 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36801-36900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	andnand1 36801	Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ⊼ (𝜑 ⊼ 𝜓 ⊼ 𝜒)))
Theorem	imnand2 36802	An → nand relation. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((¬ 𝜑 → 𝜓) ↔ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))
21.14.2  Predicate Calculus
Theorem	nalfal 36803	Not all sets hold ⊥ as true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∀𝑥⊥
Theorem	nexntru 36804	There does not exist a set such that ⊤ is not true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃𝑥 ¬ ⊤
Theorem	nexfal 36805	There does not exist a set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃𝑥⊥
Theorem	neufal 36806	There does not exist exactly one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃!𝑥⊥
Theorem	neutru 36807	There does not exist exactly one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃!𝑥⊤
Theorem	nmotru 36808	There does not exist at most one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃*𝑥⊤
Theorem	mofal 36809	There exist at most one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∃*𝑥⊥
Theorem	nrmo 36810	"At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜑)    ⇒   ⊢ ∃*𝑥 ∈ 𝐴 𝜑
21.14.3  Miscellaneous single axioms
Theorem	meran1 36811	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
Theorem	meran2 36812	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜏 ∨ 𝜃) ∨ (𝜒 ∨ (𝜑 ∨ 𝜃))))
Theorem	meran3 36813	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜒 ∨ 𝜑) ∨ (𝜏 ∨ (𝜃 ∨ 𝜑))))
Theorem	waj-ax 36814	A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓))))
Theorem	lukshef-ax2 36815	A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
Theorem	arg-ax 36816	A single axiom for propositional calculus discovered by Ken Harris and Branden Fitelson. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom HF1 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
21.14.4  Connective Symmetry
Theorem	negsym1 36817	In the paper "On Variable Functors of Propositional Arguments", Lukasiewicz introduced a system that can handle variable connectives. This was done by introducing a variable, marked with a lowercase delta, which takes a wff as input. In the system, "delta 𝜑 " means that "something is true of 𝜑". The expression "delta 𝜑 " can be substituted with ¬ 𝜑, 𝜓 ∧ 𝜑, ∀𝑥𝜑, etc. Later on, Meredith discovered a single axiom, in the form of ( delta delta ⊥ → delta 𝜑 ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus. A symmetry with ¬. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ (¬ ¬ ⊥ → ¬ 𝜑)
Theorem	imsym1 36818	A symmetry with →. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 → (𝜓 → ⊥)) → (𝜓 → 𝜑))
Theorem	bisym1 36819	A symmetry with ↔. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ↔ (𝜓 ↔ ⊥)) → (𝜓 ↔ 𝜑))
Theorem	consym1 36820	A symmetry with ∧. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∧ (𝜓 ∧ ⊥)) → (𝜓 ∧ 𝜑))
Theorem	dissym1 36821	A symmetry with ∨. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∨ (𝜓 ∨ ⊥)) → (𝜓 ∨ 𝜑))
Theorem	nandsym1 36822	A symmetry with ⊼. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ⊼ (𝜓 ⊼ ⊥)) → (𝜓 ⊼ 𝜑))
Theorem	unisym1 36823	A symmetry with ∀. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑥⊥ → ∀𝑥𝜑)
Theorem	exisym1 36824	A symmetry with ∃. See negsym1 36817 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ (∃𝑥∃𝑥⊥ → ∃𝑥𝜑)
Theorem	unqsym1 36825	A symmetry with ∃!. See negsym1 36817 for more information. (Contributed by Anthony Hart, 6-Sep-2011.)
⊢ (∃!𝑥∃!𝑥⊥ → ∃!𝑥𝜑)
Theorem	amosym1 36826	A symmetry with ∃*. See negsym1 36817 for more information. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ (∃*𝑥∃*𝑥⊥ → ∃*𝑥𝜑)
Theorem	subsym1 36827	A symmetry with [𝑥 / 𝑦]. See negsym1 36817 for more information. (Contributed by Anthony Hart, 11-Sep-2011.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]⊥ → [𝑦 / 𝑥]𝜑)
21.15  Mathbox for Chen-Pang He
21.15.1  Ordinal topology
Theorem	ontopbas 36828	An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.)
⊢ (𝐵 ∈ On → 𝐵 ∈ TopBases)
Theorem	onsstopbas 36829	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 36830	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 36831	The topology generated from an ordinal number 𝐵 is suc ∪ 𝐵. (Contributed by Chen-Pang He, 10-Oct-2015.)
⊢ (𝐵 ∈ On → (topGen‘𝐵) = suc ∪ 𝐵)
Theorem	ontgsucval 36832	The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → (topGen‘suc 𝐴) = suc 𝐴)
Theorem	onsuctop 36833	A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Top)
Theorem	onsuctopon 36834	One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴))
Theorem	ordtoplem 36835	Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆)    ⇒   ⊢ (Ord 𝐴 → (𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆))
Theorem	ordtop 36836	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 36837	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ Conn
Theorem	onsucconn 36838	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn)
Theorem	ordtopconn 36839	An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn))
Theorem	onintopssconn 36840	An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (On ∩ Top) ⊆ Conn
Theorem	onsuct0 36841	A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2)
Theorem	ordtopt0 36842	An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2))
Theorem	onsucsuccmpi 36843	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 36844	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 36845	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ Lim 𝐴    ⇒   ⊢ ¬ suc 𝐴 ∈ Comp
Theorem	limsucncmp 36846	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp)
Theorem	ordcmp 36847	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 36848	The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ {1o, 2o} ⊆ (On ∩ Haus)
Theorem	onint1 36849	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 36850	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 36851	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃)))
Theorem	findfvcl 36852*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃)    &   ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃)))    ⇒   ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃))
Theorem	findreccl 36853*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃))
Theorem	findabrcl 36854*	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 36855	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐵 ∈ ℕ → 𝜑)    &   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓)
Theorem	nnssi3 36856	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐶 ∈ ℕ → 𝜑)    &   ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓)
Theorem	nndivsub 36857	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ))
Theorem	nndivlub 36858	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴))
Syntax	cgcdOLD 36859	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD (𝐴, 𝐵)
Definition	df-gcdOLD 36860*	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 36861	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 36862*	Value of the relation constructed in weiunpo 36865, weiunso 36866, weiunfr 36867, and weiunse 36868. (Contributed by Matthew House, 8-Sep-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
Theorem	weiunlem 36863*	Lemma for weiunpo 36865, weiunso 36866, weiunfr 36867, and weiunse 36868. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
Theorem	weiunfrlem 36864*	Lemma for weiunfr 36867. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ 𝐸 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)    &   ⊢ (𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝑟 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋𝐸 / 𝑥⦌𝐵)(𝐹‘𝑡) = 𝐸))
Theorem	weiunpo 36865*	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 36866*	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 36867*	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 36868*	The relation constructed in weiunpo 36865, weiunso 36866, weiunfr 36867, and weiunwe 36869 is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunwe 36869*	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 36870*	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 36871*	Axiom of Transitive Containment, derived as a theorem from ax-ext 2741, ax-rep 5242, and ax-inf2 9610. Use ax-tco 36872 instead. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Axiom	ax-tco 36872*	The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 36871 above and is therefore redundant if we assume ax-ext 2741, ax-rep 5242 and ax-inf2 9610, 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 9704. 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 36873 and axtco1g 36876, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 36874 and axtco2g 36877. The weak form follows directly from the strong form, see axtco2 36874. But the strong form only follows from the weak form if we allow el 5420 or one of its variants, see axtco1from2 36875. 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 36878 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1 36873*	Strong form of the Axiom of Transitive Containment. See ax-tco 36872 for more information. In particular, this theorem generalizes the statement of ax-tco 36872, 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 36874*	Weak form of the Axiom of Transitive Containment. See ax-tco 36872 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 36875*	Strong form axtco1 36873 of the Axiom of Transitive Containment, derived from the weak form axtco2 36874. See ax-tco 36872 for more information. As written, the proof uses ax-pr 5405 via el 5420, but we could alternatively use ax-pow 5337 via elALT2 5341. Use axtco1 36873 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 36876*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36872 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 36877*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36872 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 36878	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 2410. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 36879*	Derivation of ax-un 7733 from ax-tco 36872. Use ax-un 7733 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 36880*	Derivation of ax-nul 5271 from ax-reg 9554 and ax-tco 36872. Use ax-nul 5271 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 36881*	Derivation of el 5420 from ax-tco 36872. Use el 5420 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 36882*	Version of tz9.1c 9699 derived from ax-tco 36872. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 36883*	Version of tz9.1 9698 derived from ax-tco 36872. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.17.3  Transitive closure of a class
Theorem	tr0elw 36884	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 36885. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 36885	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 36886	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 36887*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9704), 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 36926. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 36888	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 36889	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 36890	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 36891	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 36892	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴
Theorem	ttctr 36893	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Tr TC+ 𝐴
Theorem	ttctr2 36894	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → 𝐴 ⊆ TC+ 𝐵)
Theorem	ttctr3 36895	The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∪ TC+ 𝐴 ⊆ TC+ 𝐴
Theorem	ttcmin 36896	The transitive closure of 𝐴 is a subclass of every transitive class containing 𝐴. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → TC+ 𝐴 ⊆ 𝐵)
Theorem	ttcexrg 36897	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 36898	A transitive closure contains the transitive closures of all its subclasses. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcss2 36899	The subclass relationship is inherited by transitive closures. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ⊆ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)
Theorem	ttcel 36900	A transitive closure contains the transitive closures of all its elements. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵)