Home Intuitionistic Logic ExplorerTheorem List (p. 120 of 134) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremphi1 11901 Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
(ϕ‘1) = 1

Theoremdfphi2 11902* Alternate definition of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.)
(𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1}))

Theoremhashdvds 11903* The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐴 ∈ ℤ)    &   (𝜑𝐵 ∈ (ℤ‘(𝐴 − 1)))    &   (𝜑𝐶 ∈ ℤ)       (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))

Theoremphiprmpw 11904 Value of the Euler ϕ function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))

Theoremphiprm 11905 Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
(𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))

Theoremcrth 11906* The Chinese Remainder Theorem: the function that maps 𝑥 to its remainder classes mod 𝑀 and mod 𝑁 is 1-1 and onto when 𝑀 and 𝑁 are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.)
𝑆 = (0..^(𝑀 · 𝑁))    &   𝑇 = ((0..^𝑀) × (0..^𝑁))    &   𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))       (𝜑𝐹:𝑆1-1-onto𝑇)

Theoremphimullem 11907* Lemma for phimul 11908. (Contributed by Mario Carneiro, 24-Feb-2014.)
𝑆 = (0..^(𝑀 · 𝑁))    &   𝑇 = ((0..^𝑀) × (0..^𝑁))    &   𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    &   𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}    &   𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}       (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))

Theoremphimul 11908 The Euler ϕ function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1) → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))

Theoremhashgcdlem 11909* A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}    &   𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}    &   𝐹 = (𝑥𝐴 ↦ (𝑥 · 𝑁))       ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁𝑀) → 𝐹:𝐴1-1-onto𝐵)

Theoremhashgcdeq 11910* Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (0..^𝑀) ∣ (𝑥 gcd 𝑀) = 𝑁}) = if(𝑁𝑀, (ϕ‘(𝑀 / 𝑁)), 0))

5.3  Cardinality of real and complex number subsets

5.3.1  Countability of integers and rationals

Theoremoddennn 11911 There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
{𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ

Theoremevenennn 11912 There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
{𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈ ℕ

Theoremxpnnen 11913 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.)
(ℕ × ℕ) ≈ ℕ

Theoremxpomen 11914 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.)
(ω × ω) ≈ ω

Theoremxpct 11915 The cartesian product of two sets dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 24-Sep-2017.)
((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)

Theoremunennn 11916 The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) ≈ ℕ)

Theoremznnen 11917 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.)
ℤ ≈ ℕ

Theoremennnfonelemdc 11918* Lemma for ennnfone 11944. A direct consequence of fidcenumlemrk 6842. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑𝑃 ∈ ω)       (𝜑DECID (𝐹𝑃) ∈ (𝐹𝑃))

Theoremennnfonelemk 11919* Lemma for ennnfone 11944. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑𝐹:ω–onto𝐴)    &   (𝜑𝐾 ∈ ω)    &   (𝜑𝑁 ∈ ω)    &   (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹𝐾) ≠ (𝐹𝑗))       (𝜑𝑁𝐾)

Theoremennnfonelemj0 11920* Lemma for ennnfone 11944. 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 𝑔 ∈ ω})

Theoremennnfonelemjn 11921* Lemma for ennnfone 11944. 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))) → (𝐽𝑓) ∈ ω)

Theoremennnfonelemg 11922* Lemma for ennnfone 11944. 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 𝑔 ∈ ω})

Theoremennnfonelemh 11923* Lemma for ennnfone 11944. (Contributed by Jim Kingdon, 8-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑𝐻:ℕ0⟶(𝐴pm ω))

Theoremennnfonelem0 11924* Lemma for ennnfone 11944. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑 → (𝐻‘0) = ∅)

Theoremennnfonelemp1 11925* Lemma for ennnfone 11944. 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 (𝐻𝑃), (𝐹‘(𝑁𝑃))⟩})))

Theoremennnfonelem1 11926* Lemma for ennnfone 11944. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑 → (𝐻‘1) = {⟨∅, (𝐹‘∅)⟩})

Theoremennnfonelemom 11927* Lemma for ennnfone 11944. 𝐻 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 (𝐻𝑃) ∈ ω)

Theoremennnfonelemhdmp1 11928* Lemma for ennnfone 11944. 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 (𝐻𝑃))

Theoremennnfonelemss 11929* Lemma for ennnfone 11944. 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)))

Theoremennnfoneleminc 11930* Lemma for ennnfone 11944. 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)    &   (𝜑𝑃𝑄)       (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑄))

Theoremennnfonelemkh 11931* Lemma for ennnfone 11944. 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 (𝐻𝑃) ⊆ (𝑁𝑃))

Theoremennnfonelemhf1o 11932* Lemma for ennnfone 11944. 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→(𝐹 “ (𝑁𝑃)))

Theoremennnfonelemex 11933* Lemma for ennnfone 11944. 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 (𝐻𝑖))

Theoremennnfonelemhom 11934* Lemma for ennnfone 11944. 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 (𝐻𝑖))

Theoremennnfonelemrnh 11935* Lemma for ennnfone 11944. A consequence of ennnfonelemss 11929. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑋 ∈ ran 𝐻)    &   (𝜑𝑌 ∈ ran 𝐻)       (𝜑 → (𝑋𝑌𝑌𝑋))

Theoremennnfonelemfun 11936* Lemma for ennnfone 11944. 𝐿 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 𝐿)

Theoremennnfonelemf1 11937* Lemma for ennnfone 11944. 𝐿 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𝐴)

Theoremennnfonelemrn 11938* Lemma for ennnfone 11944. 𝐿 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 𝐿 = 𝐴)

Theoremennnfonelemdm 11939* Lemma for ennnfone 11944. 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 𝐿 = ω)

Theoremennnfonelemen 11940* Lemma for ennnfone 11944. The result. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)       (𝜑𝐴 ≈ ℕ)

Theoremennnfonelemnn0 11941* Lemma for ennnfone 11944. A version of ennnfonelemen 11940 expressed in terms of 0 instead of ω. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ℕ0onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝐹𝑘) ≠ (𝐹𝑗))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)       (𝜑𝐴 ≈ ℕ)

Theoremennnfonelemr 11942* Lemma for ennnfone 11944. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ℕ0onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝐹𝑘) ≠ (𝐹𝑗))       (𝜑𝐴 ≈ ℕ)

Theoremennnfonelemim 11943* Lemma for ennnfone 11944. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝐴 ≈ ℕ → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))

Theoremennnfone 11944* 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 𝑓:ℕ0onto𝐴 part, as seen in theorems like ctm 6994), 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 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))

Theoremexmidunben 11945* 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)

Theoremctinfomlemom 11946* Lemma for ctinfom 11947. Converting between ω and 0. (Contributed by Jim Kingdon, 10-Aug-2023.)
𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐺 = (𝐹𝑁)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹𝑛))       (𝜑 → (𝐺:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖)))

Theoremctinfom 11947* A condition for a set being countably infinite. Restates ennnfone 11944 in terms of ω and function image. Like ennnfone 11944 the condition can be summarized as 𝐴 being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
(𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))

Theoreminffinp1 11948* An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑 → ω ≼ 𝐴)    &   (𝜑𝐵𝐴)    &   (𝜑𝐵 ∈ Fin)       (𝜑 → ∃𝑥𝐴 ¬ 𝑥𝐵)

Theoremctinf 11949* 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𝐴 ∧ ω ≼ 𝐴))

Theoremqnnen 11950 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.)
ℚ ≈ ℕ

Theoremenctlem 11951* Lemma for enct 11952. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
(𝐴𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))

Theoremenct 11952* Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
(𝐴𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))

Theoremctiunctlemu1st 11953* Lemma for ctiunct 11959. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   (𝜑𝑁𝑈)       (𝜑 → (1st ‘(𝐽𝑁)) ∈ 𝑆)

Theoremctiunctlemu2nd 11954* Lemma for ctiunct 11959. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   (𝜑𝑁𝑈)       (𝜑 → (2nd ‘(𝐽𝑁)) ∈ (𝐹‘(1st ‘(𝐽𝑁))) / 𝑥𝑇)

Theoremctiunctlemuom 11955 Lemma for ctiunct 11959. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}       (𝜑𝑈 ⊆ ω)

Theoremctiunctlemudc 11956* Lemma for ctiunct 11959. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}       (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑈)

Theoremctiunctlemf 11957* Lemma for ctiunct 11959. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   𝐻 = (𝑛𝑈 ↦ ((𝐹‘(1st ‘(𝐽𝑛))) / 𝑥𝐺‘(2nd ‘(𝐽𝑛))))       (𝜑𝐻:𝑈 𝑥𝐴 𝐵)

Theoremctiunctlemfo 11958* Lemma for ctiunct 11959. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   𝐻 = (𝑛𝑈 ↦ ((𝐹‘(1st ‘(𝐽𝑛))) / 𝑥𝐺‘(2nd ‘(𝐽𝑛))))    &   𝑥𝐻    &   𝑥𝑈       (𝜑𝐻:𝑈onto 𝑥𝐴 𝐵)

Theoremctiunct 11959* 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.

The "countably many countable sets" version could be expressed as (𝜑𝑥𝐴) → ∃𝑔𝑔:ω–onto→(𝐵 ⊔ 1o) and countable choice (or something similar) would be needed to derive the current hypothesis from that.

Compare with the case of two sets instead of countably many, as seen at unct 11961, in which case we express countability using .

The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11914) 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 6996 and ctssdc 6998.

(Contributed by Jim Kingdon, 31-Oct-2023.)

(𝜑𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ((𝜑𝑥𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃ :ω–onto→( 𝑥𝐴 𝐵 ⊔ 1o))

Theoremctiunctal 11960* Variation of ctiunct 11959 which allows 𝑥 to be present in 𝜑. (Contributed by Jim Kingdon, 5-May-2024.)
(𝜑𝐹:ω–onto→(𝐴 ⊔ 1o))    &   (𝜑 → ∀𝑥𝐴 𝐺:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃ :ω–onto→( 𝑥𝐴 𝐵 ⊔ 1o))

Theoremunct 11961* 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))

Theoremomctfn 11962* 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)))

Theoremomiunct 11963* The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 11959 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.)
(𝜑CCHOICE)    &   ((𝜑𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃ :ω–onto→( 𝑥 ∈ ω 𝐵 ⊔ 1o))

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 11992 and strslfv 12012. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer.

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-ress 11976. 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.

Syntaxcstr 11964 Extend class notation with the class of structures with components numbered below 𝐴.
class Struct

Syntaxcnx 11965 Extend class notation with the structure component index extractor.
class ndx

Syntaxcsts 11966 Set components of a structure.
class sSet

Syntaxcslot 11967 Extend class notation with the slot function.
class Slot 𝐴

Syntaxcbs 11968 Extend class notation with the class of all base set extractors.
class Base

Syntaxcress 11969 Extend class notation with the extensible structure builder restriction operator.
class s

Definitiondf-struct 11970* 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 5141, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11981: 𝐹 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 3726). (Contributed by Mario Carneiro, 29-Aug-2015.)

Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}

Definitiondf-ndx 11971 Define the structure component index extractor. See theorem ndxarg 11991 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 11974) another set such as the set of finite ordinals ω (df-iom 4505). (Contributed by NM, 4-Sep-2011.)
ndx = ( I ↾ ℕ)

Definitiondf-slot 11972* 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 11991). 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 5441). 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 ↦ (𝑥𝐴))

Theoremsloteq 11973 Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
(𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)

Definitiondf-base 11974 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

Definitiondf-sets 11975* 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-ress 11976 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 {𝑒})) ∪ {𝑒}))

Definitiondf-ress 11976* 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 goes to Mario Carneiro.)

(Contributed by Stefan O'Rear, 29-Nov-2014.)

s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))

Theorembrstruct 11977 The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
Rel Struct

Theoremisstruct2im 11978 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 𝐹 ⊆ (...‘𝑋)))

Theoremisstruct2r 11979 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 𝑋)

Theoremstructex 11980 A structure is a set. (Contributed by AV, 10-Nov-2021.)
(𝐺 Struct 𝑋𝐺 ∈ V)

Theoremstructn0fun 11981 A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
(𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))

Theoremisstructim 11982 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 𝐹 ⊆ (𝑀...𝑁)))

Theoremisstructr 11983 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 ⟨𝑀, 𝑁⟩)

Theoremstructcnvcnv 11984 Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
(𝐹 Struct 𝑋𝐹 = (𝐹 ∖ {∅}))

Theoremstructfung 11985 The converse of the converse of a structure is a function. Closed form of structfun 11986. (Contributed by AV, 12-Nov-2021.)
(𝐹 Struct 𝑋 → Fun 𝐹)

Theoremstructfun 11986 Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
𝐹 Struct 𝑋       Fun 𝐹

Theoremstructfn 11987 Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
𝐹 Struct ⟨𝑀, 𝑁       (Fun 𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))

Theoremstrnfvnd 11988 Deduction version of strnfvn 11989. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
𝐸 = Slot 𝑁    &   (𝜑𝑆𝑉)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (𝐸𝑆) = (𝑆𝑁))

Theoremstrnfvn 11989 Value of a structure component extractor 𝐸. Normally, 𝐸 is a defined constant symbol such as Base (df-base 11974) and 𝑁 is a fixed integer such as 1. 𝑆 is a structure, i.e. a specific member of a class of structures.

Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 12012. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.)

𝑆 ∈ V    &   𝐸 = Slot 𝑁    &   𝑁 ∈ ℕ       (𝐸𝑆) = (𝑆𝑁)

Theoremstrfvssn 11990 A structure component extractor produces a value which is contained in a set dependent on 𝑆, but not 𝐸. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.)
𝐸 = Slot 𝑁    &   (𝜑𝑆𝑉)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (𝐸𝑆) ⊆ ran 𝑆)

Theoremndxarg 11991 Get the numeric argument from a defined structure component extractor such as df-base 11974. (Contributed by Mario Carneiro, 6-Oct-2013.)
𝐸 = Slot 𝑁    &   𝑁 ∈ ℕ       (𝐸‘ndx) = 𝑁

Theoremndxid 11992 A structure component extractor is defined by its own index. This theorem, together with strslfv 12012 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 11974, making it easier to change should the need arise.

(Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.)

𝐸 = Slot 𝑁    &   𝑁 ∈ ℕ       𝐸 = Slot (𝐸‘ndx)

Theoremndxslid 11993 A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 12012. (Contributed by Jim Kingdon, 29-Jan-2023.)
𝐸 = Slot 𝑁    &   𝑁 ∈ ℕ       (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)

Theoremslotslfn 11994 A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
(𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)       𝐸 Fn V

Theoremslotex 11995 Existence of slot value. A corollary of slotslfn 11994. (Contributed by Jim Kingdon, 12-Feb-2023.)
(𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)       (𝐴𝑉 → (𝐸𝐴) ∈ V)

Theoremstrndxid 11996 The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.)
(𝜑𝑆𝑉)    &   𝐸 = Slot 𝑁    &   𝑁 ∈ ℕ       (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸𝑆))

Theoremreldmsets 11997 The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
Rel dom sSet

Theoremsetsvalg 11998 Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
((𝑆𝑉𝐴𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴}))

Theoremsetsvala 11999 Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.)
((𝑆𝑉𝐴𝑋𝐵𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))

Theoremsetsex 12000 Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.)
((𝑆𝑉𝐴𝑋𝐵𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) ∈ V)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13306
 Copyright terms: Public domain < Previous  Next >