P. 125 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12401-12500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	4sqlem8 12401	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2)))
Theorem	4sqlem9 12402	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2))
Theorem	4sqlem10 12403	Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
Theorem	4sqlem1 12404*	Lemma for 4sq (not yet proved here) . The set 𝑆 is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that 𝑆 = ℕ0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ 𝑆 ⊆ ℕ0
Theorem	4sqlem2 12405*	Lemma for 4sq (not yet proved here) . Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
Theorem	4sqlem3 12406*	Lemma for 4sq (not yet proved here) . Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆)
Theorem	4sqlem4a 12407*	Lemma for 4sqlem4 12408. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆)
Theorem	4sqlem4 12408*	Lemma for 4sq (not yet proved here) . We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))
Theorem	mul4sqlem 12409*	Lemma for mul4sq 12410: algebraic manipulations. The extra assumptions involving 𝑀 would let us know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐵 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐶 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐷 ∈ ℤ[i])    &   ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))    &   ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])    &   ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])    &   ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Theorem	mul4sq 12410*	Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 12409. (For the curious, the explicit formula that is used is ( ∣ 𝑎 ∣ ↑2 + ∣ 𝑏 ∣ ↑2)( ∣ 𝑐 ∣ ↑2 + ∣ 𝑑 ∣ ↑2) = ∣ 𝑎∗ · 𝑐 + 𝑏 · 𝑑∗ ∣ ↑2 + ∣ 𝑎∗ · 𝑑 − 𝑏 · 𝑐∗ ∣ ↑2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆)
5.3  Cardinality of real and complex number subsets
5.3.1  Countability of integers and rationals
Theorem	oddennn 12411	There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ
Theorem	evenennn 12412	There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈ ℕ
Theorem	xpnnen 12413	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.)
⊢ (ℕ × ℕ) ≈ ℕ
Theorem	xpomen 12414	The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.)
⊢ (ω × ω) ≈ ω
Theorem	xpct 12415	The cartesian product of two sets dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
Theorem	unennn 12416	The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ)
Theorem	znnen 12417	The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.)
⊢ ℤ ≈ ℕ
Theorem	ennnfonelemdc 12418*	Lemma for ennnfone 12444. A direct consequence of fidcenumlemrk 6971. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → 𝑃 ∈ ω)    ⇒   ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃))
Theorem	ennnfonelemk 12419*	Lemma for ennnfone 12444. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝐾)
Theorem	ennnfonelemj0 12420*	Lemma for ennnfone 12444. Initial state for 𝐽. (Contributed by Jim Kingdon, 20-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → (𝐽‘0) ∈ {𝑔 ∈ (𝐴 ↑pm ω) ∣ dom 𝑔 ∈ ω})
Theorem	ennnfonelemjn 12421*	Lemma for ennnfone 12444. Non-initial state for 𝐽. (Contributed by Jim Kingdon, 20-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ≥‘(0 + 1))) → (𝐽‘𝑓) ∈ ω)
Theorem	ennnfonelemg 12422*	Lemma for ennnfone 12444. Closure for 𝐺. (Contributed by Jim Kingdon, 20-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴 ↑pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝑓𝐺𝑗) ∈ {𝑔 ∈ (𝐴 ↑pm ω) ∣ dom 𝑔 ∈ ω})
Theorem	ennnfonelemh 12423*	Lemma for ennnfone 12444. (Contributed by Jim Kingdon, 8-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → 𝐻:ℕ0⟶(𝐴 ↑pm ω))
Theorem	ennnfonelem0 12424*	Lemma for ennnfone 12444. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → (𝐻‘0) = ∅)
Theorem	ennnfonelemp1 12425*	Lemma for ennnfone 12444. Value of 𝐻 at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘(𝑃 + 1)) = if((𝐹‘(◡𝑁‘𝑃)) ∈ (𝐹 “ (◡𝑁‘𝑃)), (𝐻‘𝑃), ((𝐻‘𝑃) ∪ {⟨dom (𝐻‘𝑃), (𝐹‘(◡𝑁‘𝑃))⟩})))
Theorem	ennnfonelem1 12426*	Lemma for ennnfone 12444. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    ⇒   ⊢ (𝜑 → (𝐻‘1) = {⟨∅, (𝐹‘∅)⟩})
Theorem	ennnfonelemom 12427*	Lemma for ennnfone 12444. 𝐻 yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → dom (𝐻‘𝑃) ∈ ω)
Theorem	ennnfonelemhdmp1 12428*	Lemma for ennnfone 12444. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    &   ⊢ (𝜑 → ¬ (𝐹‘(◡𝑁‘𝑃)) ∈ (𝐹 “ (◡𝑁‘𝑃)))    ⇒   ⊢ (𝜑 → dom (𝐻‘(𝑃 + 1)) = suc dom (𝐻‘𝑃))
Theorem	ennnfonelemss 12429*	Lemma for ennnfone 12444. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑃) ⊆ (𝐻‘(𝑃 + 1)))
Theorem	ennnfoneleminc 12430*	Lemma for ennnfone 12444. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑄 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑄)    ⇒   ⊢ (𝜑 → (𝐻‘𝑃) ⊆ (𝐻‘𝑄))
Theorem	ennnfonelemkh 12431*	Lemma for ennnfone 12444. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → dom (𝐻‘𝑃) ⊆ (◡𝑁‘𝑃))
Theorem	ennnfonelemhf1o 12432*	Lemma for ennnfone 12444. Each of the functions in 𝐻 is one to one and onto an image of 𝐹. (Contributed by Jim Kingdon, 17-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (◡𝑁‘𝑃)))
Theorem	ennnfonelemex 12433*	Lemma for ennnfone 12444. Extending the sequence (𝐻‘𝑃) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻‘𝑃) ∈ dom (𝐻‘𝑖))
Theorem	ennnfonelemhom 12434*	Lemma for ennnfone 12444. The sequences in 𝐻 increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 𝑀 ∈ dom (𝐻‘𝑖))
Theorem	ennnfonelemrnh 12435*	Lemma for ennnfone 12444. A consequence of ennnfonelemss 12429. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝐻)    &   ⊢ (𝜑 → 𝑌 ∈ ran 𝐻)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∨ 𝑌 ⊆ 𝑋))
Theorem	ennnfonelemfun 12436*	Lemma for ennnfone 12444. 𝐿 is a function. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ 𝐿 = ∪ 𝑖 ∈ ℕ0 (𝐻‘𝑖)    ⇒   ⊢ (𝜑 → Fun 𝐿)
Theorem	ennnfonelemf1 12437*	Lemma for ennnfone 12444. 𝐿 is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ 𝐿 = ∪ 𝑖 ∈ ℕ0 (𝐻‘𝑖)    ⇒   ⊢ (𝜑 → 𝐿:dom 𝐿–1-1→𝐴)
Theorem	ennnfonelemrn 12438*	Lemma for ennnfone 12444. 𝐿 is onto 𝐴. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ 𝐿 = ∪ 𝑖 ∈ ℕ0 (𝐻‘𝑖)    ⇒   ⊢ (𝜑 → ran 𝐿 = 𝐴)
Theorem	ennnfonelemdm 12439*	Lemma for ennnfone 12444. The function 𝐿 is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ 𝐿 = ∪ 𝑖 ∈ ℕ0 (𝐻‘𝑖)    ⇒   ⊢ (𝜑 → dom 𝐿 = ω)
Theorem	ennnfonelemen 12440*	Lemma for ennnfone 12444. The result. (Contributed by Jim Kingdon, 16-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1))))    &   ⊢ 𝐻 = seq0(𝐺, 𝐽)    &   ⊢ 𝐿 = ∪ 𝑖 ∈ ℕ0 (𝐻‘𝑖)    ⇒   ⊢ (𝜑 → 𝐴 ≈ ℕ)
Theorem	ennnfonelemnn0 12441*	Lemma for ennnfone 12444. A version of ennnfonelemen 12440 expressed in terms of ℕ0 instead of ω. (Contributed by Jim Kingdon, 27-Oct-2022.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗))    &   ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝜑 → 𝐴 ≈ ℕ)
Theorem	ennnfonelemr 12442*	Lemma for ennnfone 12444. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗))    ⇒   ⊢ (𝜑 → 𝐴 ≈ ℕ)
Theorem	ennnfonelemim 12443*	Lemma for ennnfone 12444. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
⊢ (𝐴 ≈ ℕ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗))))
Theorem	ennnfone 12444*	A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that 𝐴 is countable (that's the 𝑓:ℕ0–onto→𝐴 part, as seen in theorems like ctm 7126), infinite (that's the part about being able to find an element of 𝐴 distinct from any mapping of a natural number via 𝑓), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.)
⊢ (𝐴 ≈ ℕ ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗))))
Theorem	exmidunben 12445*	If any unbounded set of positive integers is equinumerous to ℕ, then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.)
⊢ ((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) → EXMID)
Theorem	ctinfomlemom 12446*	Lemma for ctinfom 12447. Converting between ω and ℕ0. (Contributed by Jim Kingdon, 10-Aug-2023.)
⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐺 = (𝐹 ∘ ◡𝑁)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹‘𝑘) ∈ (𝐹 “ 𝑛))    ⇒   ⊢ (𝜑 → (𝐺:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0 ∀𝑖 ∈ (0...𝑚)(𝐺‘𝑗) ≠ (𝐺‘𝑖)))
Theorem	ctinfom 12447*	A condition for a set being countably infinite. Restates ennnfone 12444 in terms of ω and function image. Like ennnfone 12444 the condition can be summarized as 𝐴 being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
⊢ (𝐴 ≈ ℕ ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛))))
Theorem	inffinp1 12448*	An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → ω ≼ 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	ctinf 12449*	A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.)
⊢ (𝐴 ≈ ℕ ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto→𝐴 ∧ ω ≼ 𝐴))
Theorem	qnnen 12450	The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.)
⊢ ℚ ≈ ℕ
Theorem	enctlem 12451*	Lemma for enct 12452. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
Theorem	enct 12452*	Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
Theorem	ctiunctlemu1st 12453*	Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (1st ‘(𝐽‘𝑁)) ∈ 𝑆)
Theorem	ctiunctlemu2nd 12454*	Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐽‘𝑁)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑁))) / 𝑥⦌𝑇)
Theorem	ctiunctlemuom 12455	Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    ⇒   ⊢ (𝜑 → 𝑈 ⊆ ω)
Theorem	ctiunctlemudc 12456*	Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑈)
Theorem	ctiunctlemf 12457*	Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))))    ⇒   ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ctiunctlemfo 12458*	Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))))    &   ⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑈    ⇒   ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ctiunct 12459*	A sequence of enumerations gives an enumeration of the union. We refer to "sequence of enumerations" rather than "countably many countable sets" because the hypothesis provides more than countability for each 𝐵(𝑥): it refers to 𝐵(𝑥) together with the 𝐺(𝑥) which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74. For "countably many countable sets" the key hypothesis would be (𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑔𝑔:ω–onto→(𝐵 ⊔ 1o). This is almost omiunct 12463 (which uses countable choice) although that is for a countably infinite collection not any countable collection. Compare with the case of two sets instead of countably many, as seen at unct 12461, which says that the union of two countable sets is countable . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 12414) and using the first number to map to an element 𝑥 of 𝐴 and the second number to map to an element of B(x) . In this way we are able to map to every element of ∪ 𝑥 ∈ 𝐴𝐵. Although it would be possible to work directly with countability expressed as 𝐹:ω–onto→(𝐴 ⊔ 1o), we instead use functions from subsets of the natural numbers via ctssdccl 7128 and ctssdc 7130. (Contributed by Jim Kingdon, 31-Oct-2023.)
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o))    ⇒   ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
Theorem	ctiunctal 12460*	Variation of ctiunct 12459 which allows 𝑥 to be present in 𝜑. (Contributed by Jim Kingdon, 5-May-2024.)
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐺:ω–onto→(𝐵 ⊔ 1o))    ⇒   ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
Theorem	unct 12461*	The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.)
⊢ ((∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) → ∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o))
Theorem	omctfn 12462*	Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn ω ∧ ∀𝑥 ∈ ω (𝑓‘𝑥):ω–onto→(𝐵 ⊔ 1o)))
Theorem	omiunct 12463*	The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12459 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))    ⇒   ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ ω 𝐵 ⊔ 1o))
Theorem	ssomct 12464*	A decidable subset of ω is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	ssnnctlemct 12465*	Lemma for ssnnct 12466. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1)    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	ssnnct 12466*	A decidable subset of ℕ is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	nninfdclemcl 12467*	Lemma for nninfdc 12472. (Contributed by Jim Kingdon, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴)
Theorem	nninfdclemf 12468*	Lemma for nninfdc 12472. A function from the natural numbers into 𝐴. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)
Theorem	nninfdclemp1 12469*	Lemma for nninfdc 12472. Each element of the sequence 𝐹 is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   ⊢ (𝜑 → 𝑈 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘(𝑈 + 1)))
Theorem	nninfdclemlt 12470*	Lemma for nninfdc 12472. The function from nninfdclemf 12468 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   ⊢ (𝜑 → 𝑈 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑈 < 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑉))
Theorem	nninfdclemf1 12471*	Lemma for nninfdc 12472. The function from nninfdclemf 12468 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   ⊢ (𝜑 → 𝐹:ℕ–1-1→𝐴)
Theorem	nninfdc 12472*	An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → ω ≼ 𝐴)
Theorem	unbendc 12473*	An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ)
Theorem	prminf 12474	There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ ℙ ≈ ℕ
Theorem	infpn2 12475*	There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 12377, so by unbendc 12473 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
⊢ 𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))}    ⇒   ⊢ 𝑆 ≈ ℕ
PART 6  BASIC STRUCTURES
6.1  Extensible structures
6.1.1  Basic definitions An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of ℕ. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 12504 and strslfv 12525. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 12535 for more details on numeric indices versus the structure component extractors. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an 𝑋 is a 𝑌 via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-iress 12488. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.
Syntax	cstr 12476	Extend class notation with the class of structures with components numbered below 𝐴.
class Struct
Syntax	cnx 12477	Extend class notation with the structure component index extractor.
class ndx
Syntax	csts 12478	Set components of a structure.
class sSet
Syntax	cslot 12479	Extend class notation with the slot function.
class Slot 𝐴
Syntax	cbs 12480	Extend class notation with the class of all base set extractors.
class Base
Syntax	cress 12481	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-struct 12482*	Define a structure with components in 𝑀...𝑁. This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems. As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set ∅ to be extensible structures. Because of 0nelfun 5249, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12493: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}). Allowing an extensible structure to contain the empty set ensures that expressions like {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} are structures without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are sets (if 𝐴 or 𝐵 is a proper class, then ⟨𝐴, 𝐵⟩ = ∅, see opprc 3814). (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
Definition	df-ndx 12483	Define the structure component index extractor. See Theorem ndxarg 12503 to understand its purpose. The restriction to ℕ ensures that ndx is a set. The restriction to some set is necessary since I is a proper class. In principle, we could have chosen ℂ or (if we revise all structure component definitions such as df-base 12486) another set such as the set of finite ordinals ω (df-iom 4605). (Contributed by NM, 4-Sep-2011.)
⊢ ndx = ( I ↾ ℕ)
Definition	df-slot 12484*	Define the slot extractor for extensible structures. The class Slot 𝐴 is a function whose argument can be any set, although it is meaningful only if that set is a member of an extensible structure (such as a partially ordered set or a group). Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴‘𝑆) is defined to be (𝑆‘𝐴), where 𝐴 will typically be a small nonzero natural number. Each extensible structure 𝑆 is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" ndx, defined as the identity function restricted to ℕ, can be used to extract the number 𝐴 from a slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 12503). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression (Base‘ndx) in theorems and proofs instead of its value 1). The class Slot cannot be defined as (𝑥 ∈ V ↦ (𝑓 ∈ V ↦ (𝑓‘𝑥))) because each Slot 𝐴 is a function on the proper class V so is itself a proper class, and the values of functions are sets (fvex 5550). It is necessary to allow proper classes as values of Slot 𝐴 since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))
Theorem	sloteq 12485	Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
Definition	df-base 12486	Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ Base = Slot 1
Definition	df-sets 12487*	Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-iress 12488 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
Definition	df-iress 12488*	Define a multifunction restriction operator for extensible structures, which can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone; individual kinds of structures will need to handle this behavior, by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. (Credit for this operator, as well as the 2023 modification for iset.mm, goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 7-Oct-2023.)
⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
Theorem	brstruct 12489	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Rel Struct
Theorem	isstruct2im 12490	The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (𝐹 Struct 𝑋 → (𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))
Theorem	isstruct2r 12491	The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 Struct 𝑋)
Theorem	structex 12492	A structure is a set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V)
Theorem	structn0fun 12493	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))
Theorem	isstructim 12494	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (𝐹 Struct ⟨𝑀, 𝑁⟩ → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁)))
Theorem	isstructr 12495	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ (Fun (𝐹 ∖ {∅}) ∧ 𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (𝑀...𝑁))) → 𝐹 Struct ⟨𝑀, 𝑁⟩)
Theorem	structcnvcnv 12496	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 → ◡◡𝐹 = (𝐹 ∖ {∅}))
Theorem	structfung 12497	The converse of the converse of a structure is a function. Closed form of structfun 12498. (Contributed by AV, 12-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹)
Theorem	structfun 12498	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
⊢ 𝐹 Struct 𝑋    ⇒   ⊢ Fun ◡◡𝐹
Theorem	structfn 12499	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝑀, 𝑁⟩    ⇒   ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))
Theorem	strnfvnd 12500	Deduction version of strnfvn 12501. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁))