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
21.19.9  Monoid of endomorphisms
Syntax	cend 37301	Token for the monoid of endomorphisms.
class End
Definition	df-bj-end 37302*	The monoid of endomorphisms on an object of a category. (Contributed by BJ, 4-Apr-2024.)
⊢ End = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}))
Theorem	bj-endval 37303	Value of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) = {⟨(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)⟩, ⟨(+g‘ndx), (⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)⟩})
Theorem	bj-endbase 37304	Base set of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (Base‘((End ‘𝐶)‘𝑋)) = (𝑋(Hom ‘𝐶)𝑋))
Theorem	bj-endcomp 37305	Composition law of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → (+g‘((End ‘𝐶)‘𝑋)) = (⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋))
Theorem	bj-endmnd 37306	The monoid of endomorphisms on an object of a category is a monoid. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))    ⇒   ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) ∈ Mnd)
21.20  Mathbox for Jim Kingdon
21.20.1  Circle constant
Theorem	taupilem3 37307	Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1))
Theorem	taupilemrplb 37308*	A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦
Theorem	taupilem1 37309	Lemma for taupi 37311. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴)
Theorem	taupilem2 37310	Lemma for taupi 37311. The smallest positive real whose cosine is one is at most 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
⊢ τ ≤ (2 · π)
Theorem	taupi 37311	Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
⊢ τ = (2 · π)
21.20.2  Number theory
Theorem	dfgcd3 37312*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
21.20.3  Real numbers
Theorem	irrdifflemf 37313	Lemma for irrdiff 37314. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ≠ (abs‘(𝐴 − 𝑅)))
Theorem	irrdiff 37314*	The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024.)
⊢ (𝐴 ∈ ℝ → (¬ 𝐴 ∈ ℚ ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))))
Theorem	iccioo01 37315	The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024.)
⊢ (0[,]1) ≈ (0(,)1)
21.21  Mathbox for ML
21.21.1  Miscellaneous
Theorem	csbrecsg 37316	Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹))
Theorem	csbrdgg 37317	Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼))
Theorem	csboprabg 37318*	Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpo123 37319*	Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷))
Theorem	con1bii2 37320	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜓)
Theorem	con2bii2 37321	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ 𝜓)
Theorem	vtoclefex 37322*	Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)
Theorem	rnmptsn 37323*	The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.)
⊢ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}
Theorem	f1omptsnlem 37324*	This is the core of the proof of f1omptsn 37325, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ 𝐹:𝐴–1-1-onto→𝑅
Theorem	f1omptsn 37325*	A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ 𝐹:𝐴–1-1-onto→𝑅
Theorem	mptsnunlem 37326*	This is the core of the proof of mptsnun 37327, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))
Theorem	mptsnun 37327*	A class 𝐵 is equal to the union of the class of all singletons of elements of 𝐵. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))
Theorem	dissneqlem 37328*	This is the core of the proof of dissneq 37329, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)
Theorem	dissneq 37329*	Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.)
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)
Theorem	exlimim 37330*	Closed form of exlimimd 37331. (Contributed by ML, 17-Jul-2020.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → 𝜓)
Theorem	exlimimd 37331*	Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	exellim 37332*	Closed form of exellimddv 37333. See also exlimim 37330 for a more general theorem. (Contributed by ML, 17-Jul-2020.)
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) → 𝜑)
Theorem	exellimddv 37333*	Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 37332 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	topdifinfindis 37334*	Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is the trivial topology when 𝐴 is finite. (Contributed by ML, 14-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝐴 ∈ Fin → 𝑇 = {∅, 𝐴})
Theorem	topdifinffinlem 37335*	This is the core of the proof of topdifinffin 37336, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Theorem	topdifinffin 37336*	Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology only if 𝐴 is finite. (Contributed by ML, 17-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)
Theorem	topdifinf 37337*	Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology if and only if 𝐴 is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020.)
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ ((𝑇 ∈ (TopOn‘𝐴) ↔ 𝐴 ∈ Fin) ∧ (𝑇 ∈ (TopOn‘𝐴) → 𝑇 = {∅, 𝐴}))
Theorem	topdifinfeq 37338*	Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.)
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))} = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}
Theorem	icorempo 37339*	Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.)
⊢ 𝐹 = ([,) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
Theorem	icoreresf 37340	Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.)
⊢ ([,) ↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫 ℝ
Theorem	icoreval 37341*	Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,)𝐵) = {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)})
Theorem	icoreelrnab 37342*	Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 𝑋 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)})
Theorem	isbasisrelowllem1 37343*	Lemma for isbasisrelowl 37346. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑)) → (𝑥 ∩ 𝑦) ∈ 𝐼)
Theorem	isbasisrelowllem2 37344*	Lemma for isbasisrelowl 37346. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏)) → (𝑥 ∩ 𝑦) ∈ 𝐼)
Theorem	icoreclin 37345*	The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∩ 𝑦) ∈ 𝐼)
Theorem	isbasisrelowl 37346	The set of all closed-below, open-above intervals of reals form a basis. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ 𝐼 ∈ TopBases
Theorem	icoreunrn 37347	The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ℝ = ∪ 𝐼
Theorem	istoprelowl 37348	The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘𝐼) ∈ (TopOn‘ℝ)
Theorem	icoreelrn 37349*	A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)} ∈ 𝐼)
Theorem	iooelexlt 37350*	An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.)
⊢ (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)
Theorem	relowlssretop 37351	The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)
Theorem	relowlpssretop 37352	The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.)
⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)
Theorem	sucneqond 37353	Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.)
⊢ (𝜑 → 𝑋 = suc 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ On)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)
Theorem	sucneqoni 37354	Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.)
⊢ 𝑋 = suc 𝑌    &   ⊢ 𝑌 ∈ On    ⇒   ⊢ 𝑋 ≠ 𝑌
Theorem	onsucuni3 37355	If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020.)
⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → 𝐵 = suc ∪ 𝐵)
Theorem	1oequni2o 37356	The ordinal number 1o is the predecessor of the ordinal number 2o. (Contributed by ML, 19-Oct-2020.)
⊢ 1o = ∪ 2o
Theorem	rdgsucuni 37357	If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020.)
⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → (rec(𝐹, 𝐼)‘𝐵) = (𝐹‘(rec(𝐹, 𝐼)‘∪ 𝐵)))
Theorem	rdgeqoa 37358	If a recursive function with an initial value 𝐴 at step 𝑁 is equal to itself with an initial value 𝐵 at step 𝑀, then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020.)
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))))
Theorem	elxp8 37359	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 8003. (Contributed by ML, 19-Oct-2020.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ((1st ‘𝐴) ∈ 𝐵 ∧ 𝐴 ∈ (V × 𝐶)))
Theorem	cbveud 37360*	Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvreud 37361*	Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))
Theorem	difunieq 37362	The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021.)
⊢ (∪ 𝐴 ∖ ∪ 𝐵) ⊆ ∪ (𝐴 ∖ 𝐵)
Theorem	inunissunidif 37363	Theorem about subsets of the difference of unions. (Contributed by ML, 29-Mar-2021.)
⊢ ((𝐴 ∩ ∪ 𝐶) = ∅ → (𝐴 ⊆ ∪ 𝐵 ↔ 𝐴 ⊆ ∪ (𝐵 ∖ 𝐶)))
Theorem	rdgellim 37364	Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022.)
⊢ (((𝐵 ∈ On ∧ Lim 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑋 ∈ (rec(𝐹, 𝐴)‘𝐶) → 𝑋 ∈ (rec(𝐹, 𝐴)‘𝐵)))
Theorem	rdglimss 37365	A recursive definition at a limit ordinal is a superset of itself at any smaller ordinal. (Contributed by ML, 30-Mar-2022.)
⊢ (((𝐵 ∈ On ∧ Lim 𝐵) ∧ 𝐶 ∈ 𝐵) → (rec(𝐹, 𝐴)‘𝐶) ⊆ (rec(𝐹, 𝐴)‘𝐵))
Theorem	rdgssun 37366*	In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022.)
⊢ 𝐹 = (𝑤 ∈ V ↦ (𝑤 ∪ 𝐵))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ 𝑋) → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))
Theorem	exrecfnlem 37367*	Lemma for exrecfn 37368. (Contributed by ML, 30-Mar-2022.)
⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))
Theorem	exrecfn 37368*	Theorem about the existence of infinite recursive sets. 𝑦 should usually be free in 𝐵. (Contributed by ML, 30-Mar-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))
Theorem	exrecfnpw 37369*	For any base set, a set which contains the powerset of all of its own elements exists. (Contributed by ML, 30-Mar-2022.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ∈ 𝑥))
Theorem	finorwe 37370	If the Axiom of Infinity is denied, every total order is a well-order. The notion of a well-order cannot be usefully expressed without the Axiom of Infinity due to the inability to quantify over proper classes. (Contributed by ML, 5-Oct-2023.)
⊢ (¬ ω ∈ V → ( < Or 𝐴 → < We 𝐴))
21.21.2  Cartesian exponentiation
Syntax	cfinxp 37371	Extend the definition of a class to include Cartesian exponentiation.
class (𝑈↑↑𝑁)
Definition	df-finxp 37372*	Define Cartesian exponentiation on a class. Note that this definition is limited to finite exponents, since it is defined using nested ordered pairs. If tuples of infinite length are needed, or if they might be needed in the future, use df-ixp 8871 or df-map 8801 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2o), then df-br 5108 can be used on it, and df-fv 6519 can also be used, and so on. It's also worth keeping in mind that ((𝑈↑↑𝑀) × (𝑈↑↑𝑁)) is generally not equal to (𝑈↑↑(𝑀 +o 𝑁)). This definition is technical. Use finxp1o 37380 and finxpsuc 37386 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)
⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
Theorem	dffinxpf 37373*	This theorem is the same as Definition df-finxp 37372, except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020.)
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))}
Theorem	finxpeq1 37374	Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.)
⊢ (𝑈 = 𝑉 → (𝑈↑↑𝑁) = (𝑉↑↑𝑁))
Theorem	finxpeq2 37375	Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.)
⊢ (𝑀 = 𝑁 → (𝑈↑↑𝑀) = (𝑈↑↑𝑁))
Theorem	csbfinxpg 37376*	Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑈↑↑𝑁) = (⦋𝐴 / 𝑥⦌𝑈↑↑⦋𝐴 / 𝑥⦌𝑁))
Theorem	finxpreclem1 37377*	Lemma for ↑↑ recursion theorems. (Contributed by ML, 17-Oct-2020.)
⊢ (𝑋 ∈ 𝑈 → ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1o, 𝑋⟩))
Theorem	finxpreclem2 37378*	Lemma for ↑↑ recursion theorems. (Contributed by ML, 17-Oct-2020.)
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ¬ ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1o, 𝑋⟩))
Theorem	finxp0 37379	The value of Cartesian exponentiation at zero. (Contributed by ML, 24-Oct-2020.)
⊢ (𝑈↑↑∅) = ∅
Theorem	finxp1o 37380	The value of Cartesian exponentiation at one. (Contributed by ML, 17-Oct-2020.)
⊢ (𝑈↑↑1o) = 𝑈
Theorem	finxpreclem3 37381*	Lemma for ↑↑ recursion theorems. (Contributed by ML, 20-Oct-2020.)
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1st ‘𝑋)⟩ = (𝐹‘⟨𝑁, 𝑋⟩))
Theorem	finxpreclem4 37382*	Lemma for ↑↑ recursion theorems. (Contributed by ML, 23-Oct-2020.)
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ (((𝑁 ∈ ω ∧ 2o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1st ‘𝑦)⟩)‘∪ 𝑁))
Theorem	finxpreclem5 37383*	Lemma for ↑↑ recursion theorems. (Contributed by ML, 24-Oct-2020.)
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ ((𝑛 ∈ ω ∧ 1o ∈ 𝑛) → (¬ 𝑥 ∈ (V × 𝑈) → (𝐹‘⟨𝑛, 𝑥⟩) = ⟨𝑛, 𝑥⟩))
Theorem	finxpreclem6 37384*	Lemma for ↑↑ recursion theorems. (Contributed by ML, 24-Oct-2020.)
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 1o ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))
Theorem	finxpsuclem 37385*	Lemma for finxpsuc 37386. (Contributed by ML, 24-Oct-2020.)
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 1o ⊆ 𝑁) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))
Theorem	finxpsuc 37386	The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020.)
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))
Theorem	finxp2o 37387	The value of Cartesian exponentiation at two. (Contributed by ML, 19-Oct-2020.)
⊢ (𝑈↑↑2o) = (𝑈 × 𝑈)
Theorem	finxp3o 37388	The value of Cartesian exponentiation at three. (Contributed by ML, 24-Oct-2020.)
⊢ (𝑈↑↑3o) = ((𝑈 × 𝑈) × 𝑈)
Theorem	finxpnom 37389	Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020.)
⊢ (¬ 𝑁 ∈ ω → (𝑈↑↑𝑁) = ∅)
Theorem	finxp00 37390	Cartesian exponentiation of the empty set to any power is the empty set. (Contributed by ML, 24-Oct-2020.)
⊢ (∅↑↑𝑁) = ∅
21.21.3  Topology
Theorem	iunctb2 37391	Using the axiom of countable choice ax-cc 10388, the countable union of countable sets is countable. See iunctb 10527 for a somewhat more general theorem. (Contributed by ML, 10-Dec-2020.)
⊢ (∀𝑥 ∈ ω 𝐵 ≼ ω → ∪ 𝑥 ∈ ω 𝐵 ≼ ω)
Theorem	domalom 37392*	A class which dominates every natural number is not finite. (Contributed by ML, 14-Dec-2020.)
⊢ (∀𝑛 ∈ ω 𝑛 ≼ 𝐴 → ¬ 𝐴 ∈ Fin)
Theorem	isinf2 37393*	The converse of isinf 9207. Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by ML, 14-Dec-2020.)
⊢ (∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) → ¬ 𝐴 ∈ Fin)
Theorem	ctbssinf 37394*	Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020.)
⊢ (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω))
Theorem	ralssiun 37395*	The index set of an indexed union is a subset of the union when each 𝐵 contains its index. (Contributed by ML, 16-Dec-2020.)
⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	nlpineqsn 37396*	For every point 𝑝 of a subset 𝐴 of 𝑋 with no limit points, there exists an open set 𝑛 that intersects 𝐴 only at 𝑝. (Contributed by ML, 23-Mar-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝐴) = ∅) → ∀𝑝 ∈ 𝐴 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝐴) = {𝑝}))
Theorem	nlpfvineqsn 37397*	Given a subset 𝐴 of 𝑋 with no limit points, there exists a function from each point 𝑝 of 𝐴 to an open set intersecting 𝐴 only at 𝑝. This proof uses the axiom of choice. (Contributed by ML, 23-Mar-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ 𝑉 → ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝐴) = ∅) → ∃𝑓(𝑓:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ((𝑓‘𝑝) ∩ 𝐴) = {𝑝})))
Theorem	fvineqsnf1 37398*	A theorem about functions where the image of every point intersects the domain only at that point. If 𝐽 is a topology and 𝐴 is a set with no limit points, then there exists an 𝐹 such that this antecedent is true. See nlpfvineqsn 37397 for a proof of this fact. (Contributed by ML, 23-Mar-2021.)
⊢ ((𝐹:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) → 𝐹:𝐴–1-1→𝐽)
Theorem	fvineqsneu 37399*	A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 27-Mar-2021.)
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) → ∀𝑞 ∈ 𝐴 ∃!𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥)
Theorem	fvineqsneq 37400*	A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 28-Mar-2021.)
⊢ (((𝐹 Fn 𝐴 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) ∧ (𝑍 ⊆ ran 𝐹 ∧ 𝐴 ⊆ ∪ 𝑍)) → 𝑍 = ran 𝐹)