P. 127 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12601-12700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	4sqlem17 12601*	Lemma for 4sq 12604. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ ¬ 𝜑
Theorem	4sqlem18 12602*	Lemma for 4sq 12604. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑆)
Theorem	4sqlem19 12603*	Lemma for 4sq 12604. The proof is by strong induction - we show that if all the integers less than 𝑘 are in 𝑆, then 𝑘 is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 12602. If 𝑘 is 0, 1, 2, we show 𝑘 ∈ 𝑆 directly; otherwise if 𝑘 is composite, 𝑘 is the product of two numbers less than it (and hence in 𝑆 by assumption), so by mul4sq 12588 𝑘 ∈ 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ℕ0 = 𝑆
Theorem	4sq 12604*	Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℕ0 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
5.2.13  Decimal arithmetic (cont.)
Theorem	dec2dvds 12605	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    &   ⊢ 𝐷 = (𝐶 + 1)    ⇒   ⊢ ¬ 2 ∥ ;𝐴𝐷
Theorem	dec5dvds 12606	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐵
Theorem	dec5dvds2 12607	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    &   ⊢ (5 + 𝐵) = 𝐶    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐶
Theorem	dec5nprm 12608	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ¬ ;𝐴5 ∈ ℙ
Theorem	dec2nprm 12609	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    ⇒   ⊢ ¬ ;𝐴𝐶 ∈ ℙ
Theorem	modxai 12610	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ ((𝐴↑𝐶) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (𝐵 + 𝐶) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐿)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	mod2xi 12611	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modxp1i 12612	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝐵 + 1) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐴)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modsubi 12613	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝑀 + 𝐵) = 𝐾    ⇒   ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	gcdi 12614	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    &   ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀    ⇒   ⊢ (𝑀 gcd 𝑁) = 𝐺
Theorem	gcdmodi 12615	Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ (𝐾 mod 𝑁) = (𝑅 mod 𝑁)    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    ⇒   ⊢ (𝐾 gcd 𝑁) = 𝐺
Theorem	numexp0 12616	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑0) = 1
Theorem	numexp1 12617	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑1) = 𝐴
Theorem	numexpp1 12618	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	numexp2x 12619	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (2 · 𝑀) = 𝑁    &   ⊢ (𝐴↑𝑀) = 𝐷    &   ⊢ (𝐷 · 𝐷) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	decsplit0b 12620	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 𝐵) = (𝐴 + 𝐵)
Theorem	decsplit0 12621	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 0) = 𝐴
Theorem	decsplit1 12622	Split a decimal number into two parts. Base case: 𝑁 = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑1)) + 𝐵) = ;𝐴𝐵
Theorem	decsplit 12623	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝐶    ⇒   ⊢ ((𝐴 · (;10↑𝑁)) + ;𝐵𝐷) = ;𝐶𝐷
Theorem	karatsuba 12624	The Karatsuba multiplication algorithm. If 𝑋 and 𝑌 are decomposed into two groups of digits of length 𝑀 (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then 𝑋𝑌 can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log2 3) instead of n^2 for the "naive" algorithm decmul1c 9538. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑆 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝑅    &   ⊢ (𝐵 · 𝐷) = 𝑇    &   ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = ((𝑅 + 𝑆) + 𝑇)    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝑋    &   ⊢ ((𝐶 · (;10↑𝑀)) + 𝐷) = 𝑌    &   ⊢ ((𝑅 · (;10↑𝑀)) + 𝑆) = 𝑊    &   ⊢ ((𝑊 · (;10↑𝑀)) + 𝑇) = 𝑍    ⇒   ⊢ (𝑋 · 𝑌) = 𝑍
Theorem	2exp4 12625	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑4) = ;16
Theorem	2exp5 12626	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑5) = ;32
Theorem	2exp6 12627	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (2↑6) = ;64
Theorem	2exp7 12628	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑7) = ;;128
Theorem	2exp8 12629	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑8) = ;;256
Theorem	2exp11 12630	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑;11) = ;;;2048
Theorem	2exp16 12631	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑;16) = ;;;;65536
Theorem	3exp3 12632	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (3↑3) = ;27
Theorem	2expltfac 12633	The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (2↑𝑁) < (!‘𝑁))
5.3  Cardinality of real and complex number subsets
5.3.1  Countability of integers and rationals
Theorem	oddennn 12634	There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ
Theorem	evenennn 12635	There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈ ℕ
Theorem	xpnnen 12636	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 12637	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 12638	The cartesian product of two sets dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
Theorem	unennn 12639	The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ)
Theorem	znnen 12640	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 12641*	Lemma for ennnfone 12667. A direct consequence of fidcenumlemrk 7029. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → 𝑃 ∈ ω)    ⇒   ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃))
Theorem	ennnfonelemk 12642*	Lemma for ennnfone 12667. (Contributed by Jim Kingdon, 15-Jul-2023.)
⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗))    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝐾)
Theorem	ennnfonelemj0 12643*	Lemma for ennnfone 12667. 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 12644*	Lemma for ennnfone 12667. 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 12645*	Lemma for ennnfone 12667. 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 12646*	Lemma for ennnfone 12667. (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 12647*	Lemma for ennnfone 12667. 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 12648*	Lemma for ennnfone 12667. 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 12649*	Lemma for ennnfone 12667. 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 12650*	Lemma for ennnfone 12667. 𝐻 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 12651*	Lemma for ennnfone 12667. 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 12652*	Lemma for ennnfone 12667. 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 12653*	Lemma for ennnfone 12667. 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 12654*	Lemma for ennnfone 12667. 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 12655*	Lemma for ennnfone 12667. 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 12656*	Lemma for ennnfone 12667. 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 12657*	Lemma for ennnfone 12667. 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 12658*	Lemma for ennnfone 12667. A consequence of ennnfonelemss 12652. (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 12659*	Lemma for ennnfone 12667. 𝐿 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 12660*	Lemma for ennnfone 12667. 𝐿 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 12661*	Lemma for ennnfone 12667. 𝐿 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 12662*	Lemma for ennnfone 12667. 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 12663*	Lemma for ennnfone 12667. 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 12664*	Lemma for ennnfone 12667. A version of ennnfonelemen 12663 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 12665*	Lemma for ennnfone 12667. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗))    ⇒   ⊢ (𝜑 → 𝐴 ≈ ℕ)
Theorem	ennnfonelemim 12666*	Lemma for ennnfone 12667. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
⊢ (𝐴 ≈ ℕ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗))))
Theorem	ennnfone 12667*	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 7184), 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 12668*	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 12669*	Lemma for ctinfom 12670. Converting between ω and ℕ0. (Contributed by Jim Kingdon, 10-Aug-2023.)
⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐺 = (𝐹 ∘ ◡𝑁)    &   ⊢ (𝜑 → 𝐹:ω–onto→𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹‘𝑘) ∈ (𝐹 “ 𝑛))    ⇒   ⊢ (𝜑 → (𝐺:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0 ∀𝑖 ∈ (0...𝑚)(𝐺‘𝑗) ≠ (𝐺‘𝑖)))
Theorem	ctinfom 12670*	A condition for a set being countably infinite. Restates ennnfone 12667 in terms of ω and function image. Like ennnfone 12667 the condition can be summarized as 𝐴 being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
⊢ (𝐴 ≈ ℕ ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛))))
Theorem	inffinp1 12671*	An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → ω ≼ 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	ctinf 12672*	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 12673	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 12674*	Lemma for enct 12675. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
Theorem	enct 12675*	Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
Theorem	ctiunctlemu1st 12676*	Lemma for ctiunct 12682. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (1st ‘(𝐽‘𝑁)) ∈ 𝑆)
Theorem	ctiunctlemu2nd 12677*	Lemma for ctiunct 12682. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ (𝜑 → 𝑁 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (2nd ‘(𝐽‘𝑁)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑁))) / 𝑥⦌𝑇)
Theorem	ctiunctlemuom 12678	Lemma for ctiunct 12682. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    ⇒   ⊢ (𝜑 → 𝑈 ⊆ ω)
Theorem	ctiunctlemudc 12679*	Lemma for ctiunct 12682. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑈)
Theorem	ctiunctlemf 12680*	Lemma for ctiunct 12682. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))))    ⇒   ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ctiunctlemfo 12681*	Lemma for ctiunct 12682. (Contributed by Jim Kingdon, 28-Oct-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)    &   ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω))    &   ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛))))    &   ⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑈    ⇒   ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ctiunct 12682*	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 12686 (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 12684, 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 12637) 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 7186 and ctssdc 7188. (Contributed by Jim Kingdon, 31-Oct-2023.)
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o))    ⇒   ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
Theorem	ctiunctal 12683*	Variation of ctiunct 12682 which allows 𝑥 to be present in 𝜑. (Contributed by Jim Kingdon, 5-May-2024.)
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐺:ω–onto→(𝐵 ⊔ 1o))    ⇒   ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))
Theorem	unct 12684*	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 12685*	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 12686*	The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12682 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 12687*	A decidable subset of ω is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	ssnnctlemct 12688*	Lemma for ssnnct 12689. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1)    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	ssnnct 12689*	A decidable subset of ℕ is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	nninfdclemcl 12690*	Lemma for nninfdc 12695. (Contributed by Jim Kingdon, 25-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴)
Theorem	nninfdclemf 12691*	Lemma for nninfdc 12695. A function from the natural numbers into 𝐴. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)
Theorem	nninfdclemp1 12692*	Lemma for nninfdc 12695. 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 12693*	Lemma for nninfdc 12695. The function from nninfdclemf 12691 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   ⊢ (𝜑 → 𝑈 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑈 < 𝑉)    ⇒   ⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑉))
Theorem	nninfdclemf1 12694*	Lemma for nninfdc 12695. The function from nninfdclemf 12691 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   ⊢ (𝜑 → 𝐹:ℕ–1-1→𝐴)
Theorem	nninfdc 12695*	An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → ω ≼ 𝐴)
Theorem	unbendc 12696*	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 12697	There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ ℙ ≈ ℕ
Theorem	infpn2 12698*	There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 12555, so by unbendc 12696 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 12727 and strslfv 12748. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 12758 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 12711. 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 12699	Extend class notation with the class of structures with components numbered below 𝐴.
class Struct
Syntax	cnx 12700	Extend class notation with the structure component index extractor.
class ndx