P. 368 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	naim12i 36701	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜓 ⊼ 𝜃)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	nabi1i 36702	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ⊼ 𝜒)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	nabi2i 36703	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ⊼ 𝜓)    ⇒   ⊢ (𝜒 ⊼ 𝜑)
Theorem	nabi12i 36704	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜓 ⊼ 𝜃)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Syntax	w3nand 36705	The double nand.
wff (𝜑 ⊼ 𝜓 ⊼ 𝜒)
Definition	df-3nand 36706	The double nand. This definition allows to express the input of three variables only being false if all three are true. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒)))
Theorem	df3nandALT1 36707	The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 ⊼ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒))))
Theorem	df3nandALT2 36708	The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	andnand1 36709	Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ⊼ (𝜑 ⊼ 𝜓 ⊼ 𝜒)))
Theorem	imnand2 36710	An → nand relation. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((¬ 𝜑 → 𝜓) ↔ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))
21.14.2  Predicate Calculus
Theorem	nalfal 36711	Not all sets hold ⊥ as true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∀𝑥⊥
Theorem	nexntru 36712	There does not exist a set such that ⊤ is not true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃𝑥 ¬ ⊤
Theorem	nexfal 36713	There does not exist a set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃𝑥⊥
Theorem	neufal 36714	There does not exist exactly one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃!𝑥⊥
Theorem	neutru 36715	There does not exist exactly one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃!𝑥⊤
Theorem	nmotru 36716	There does not exist at most one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃*𝑥⊤
Theorem	mofal 36717	There exist at most one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∃*𝑥⊥
Theorem	nrmo 36718	"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 36719	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
Theorem	meran2 36720	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜏 ∨ 𝜃) ∨ (𝜒 ∨ (𝜑 ∨ 𝜃))))
Theorem	meran3 36721	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜒 ∨ 𝜑) ∨ (𝜏 ∨ (𝜃 ∨ 𝜑))))
Theorem	waj-ax 36722	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 36723	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 36724	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 36725	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 36726	A symmetry with →. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 → (𝜓 → ⊥)) → (𝜓 → 𝜑))
Theorem	bisym1 36727	A symmetry with ↔. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ↔ (𝜓 ↔ ⊥)) → (𝜓 ↔ 𝜑))
Theorem	consym1 36728	A symmetry with ∧. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∧ (𝜓 ∧ ⊥)) → (𝜓 ∧ 𝜑))
Theorem	dissym1 36729	A symmetry with ∨. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∨ (𝜓 ∨ ⊥)) → (𝜓 ∨ 𝜑))
Theorem	nandsym1 36730	A symmetry with ⊼. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ⊼ (𝜓 ⊼ ⊥)) → (𝜓 ⊼ 𝜑))
Theorem	unisym1 36731	A symmetry with ∀. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑥⊥ → ∀𝑥𝜑)
Theorem	exisym1 36732	A symmetry with ∃. See negsym1 36725 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ (∃𝑥∃𝑥⊥ → ∃𝑥𝜑)
Theorem	unqsym1 36733	A symmetry with ∃!. See negsym1 36725 for more information. (Contributed by Anthony Hart, 6-Sep-2011.)
⊢ (∃!𝑥∃!𝑥⊥ → ∃!𝑥𝜑)
Theorem	amosym1 36734	A symmetry with ∃*. See negsym1 36725 for more information. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ (∃*𝑥∃*𝑥⊥ → ∃*𝑥𝜑)
Theorem	subsym1 36735	A symmetry with [𝑥 / 𝑦]. See negsym1 36725 for more information. (Contributed by Anthony Hart, 11-Sep-2011.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]⊥ → [𝑦 / 𝑥]𝜑)
21.15  Mathbox for Chen-Pang He
21.15.1  Ordinal topology
Theorem	ontopbas 36736	An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.)
⊢ (𝐵 ∈ On → 𝐵 ∈ TopBases)
Theorem	onsstopbas 36737	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 36738	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 36739	The topology generated from an ordinal number 𝐵 is suc ∪ 𝐵. (Contributed by Chen-Pang He, 10-Oct-2015.)
⊢ (𝐵 ∈ On → (topGen‘𝐵) = suc ∪ 𝐵)
Theorem	ontgsucval 36740	The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → (topGen‘suc 𝐴) = suc 𝐴)
Theorem	onsuctop 36741	A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Top)
Theorem	onsuctopon 36742	One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴))
Theorem	ordtoplem 36743	Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆)    ⇒   ⊢ (Ord 𝐴 → (𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆))
Theorem	ordtop 36744	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 36745	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ Conn
Theorem	onsucconn 36746	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn)
Theorem	ordtopconn 36747	An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn))
Theorem	onintopssconn 36748	An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (On ∩ Top) ⊆ Conn
Theorem	onsuct0 36749	A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2)
Theorem	ordtopt0 36750	An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2))
Theorem	onsucsuccmpi 36751	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 36752	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 36753	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ Lim 𝐴    ⇒   ⊢ ¬ suc 𝐴 ∈ Comp
Theorem	limsucncmp 36754	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp)
Theorem	ordcmp 36755	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 36756	The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ {1o, 2o} ⊆ (On ∩ Haus)
Theorem	onint1 36757	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 36758	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 36759	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃)))
Theorem	findfvcl 36760*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃)    &   ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃)))    ⇒   ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃))
Theorem	findreccl 36761*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃))
Theorem	findabrcl 36762*	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 36763	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐵 ∈ ℕ → 𝜑)    &   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓)
Theorem	nnssi3 36764	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐶 ∈ ℕ → 𝜑)    &   ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓)
Theorem	nndivsub 36765	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ))
Theorem	nndivlub 36766	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴))
Syntax	cgcdOLD 36767	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD (𝐴, 𝐵)
Definition	df-gcdOLD 36768*	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 36769	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 36770*	Value of the relation constructed in weiunpo 36773, weiunso 36774, weiunfr 36775, and weiunse 36776. (Contributed by Matthew House, 8-Sep-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ (𝐶𝑇𝐷 ↔ ((𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝐶)𝑅(𝐹‘𝐷) ∨ ((𝐹‘𝐶) = (𝐹‘𝐷) ∧ 𝐶⦋(𝐹‘𝐶) / 𝑥⦌𝑆𝐷))))
Theorem	weiunlem 36771*	Lemma for weiunpo 36773, weiunso 36774, weiunfr 36775, and weiunse 36776. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
Theorem	weiunfrlem 36772*	Lemma for weiunfr 36775. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ 𝐸 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)    &   ⊢ (𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝑟 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐸 ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋𝐸 / 𝑥⦌𝐵)(𝐹‘𝑡) = 𝐸))
Theorem	weiunpo 36773*	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 36774*	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 36775*	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 36776*	The relation constructed in weiunpo 36773, weiunso 36774, weiunfr 36775, and weiunwe 36777 is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025.)
⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))    &   ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	weiunwe 36777*	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 36778*	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 36779*	Axiom of Transitive Containment, derived as a theorem from ax-ext 2728, ax-rep 5221, and ax-inf2 9586. Use ax-tco 36780 instead. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Axiom	ax-tco 36780*	The Axiom of Transitive Containment of ZF set theory. It was derived as axtco 36779 above and is therefore redundant if we assume ax-ext 2728, ax-rep 5221 and ax-inf2 9586, 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 9680. 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 36781 and axtco1g 36784, and the weak form ⊢ ∃𝑦(𝑥 ⊆ 𝑦 ∧ Tr 𝑦), see axtco2 36782 and axtco2g 36785. The weak form follows directly from the strong form, see axtco2 36782. But the strong form only follows from the weak form if we allow el 5399 or one of its variants, see axtco1from2 36783. 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 36786 for reasons of syntax. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1 36781*	Strong form of the Axiom of Transitive Containment. See ax-tco 36780 for more information. In particular, this theorem generalizes the statement of ax-tco 36780, 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 36782*	Weak form of the Axiom of Transitive Containment. See ax-tco 36780 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 36783*	Strong form axtco1 36781 of the Axiom of Transitive Containment, derived from the weak form axtco2 36782. See ax-tco 36780 for more information. As written, the proof uses ax-pr 5384 via el 5399, but we could alternatively use ax-pow 5316 via elALT2 5320. Use axtco1 36781 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
Theorem	axtco1g 36784*	Strong form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36780 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ∈ 𝑥 ∧ Tr 𝑥))
Theorem	axtco2g 36785*	Weak form of the Axiom of Transitive Containment using class variables and abbreviations. See ax-tco 36780 for more information. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥))
Theorem	axtcond 36786	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 2397. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
Theorem	axuntco 36787*	Derivation of ax-un 7707 from ax-tco 36780. Use ax-un 7707 instead. (Contributed by Matthew House, 6-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axnulregtco 36788*	Derivation of ax-nul 5250 from ax-reg 9530 and ax-tco 36780. Use ax-nul 5250 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	elALTtco 36789*	Derivation of el 5399 from ax-tco 36780. Use el 5399 instead. (Contributed by Matthew House, 7-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	tz9.1ctco 36790*	Version of tz9.1c 9675 derived from ax-tco 36780. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	tz9.1tco 36791*	Version of tz9.1 9674 derived from ax-tco 36780. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
21.17.3  Transitive closure of a class
Theorem	tr0elw 36792	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 36793. (Contributed by Matthew House, 6-Apr-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ∧ Tr 𝐴) → ∅ ∈ 𝐴)
Theorem	tr0el 36793	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 36794	Extend class notation with the transitive closure of a class. (Contributed by Matthew House, 6-Apr-2026.)
class TC+ 𝐴
Definition	df-ttc 36795*	Transitive closure of a class. Unlike (TC‘𝐴) (see df-tc 9680), 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 36834. (Contributed by Matthew House, 6-Apr-2026.)
⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ (rec((𝑦 ∈ V ↦ ∪ 𝑦), {𝑥}) “ ω)
Theorem	ttceq 36796	Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵)
Theorem	ttceqi 36797	Equality inference for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ TC+ 𝐴 = TC+ 𝐵
Theorem	ttceqd 36798	Equality deduction for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → TC+ 𝐴 = TC+ 𝐵)
Theorem	nfttc 36799	Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥TC+ 𝐴
Theorem	ttcid 36800	The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026.)
⊢ 𝐴 ⊆ TC+ 𝐴