![]() |
Intuitionistic Logic Explorer Theorem List (p. 125 of 153) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
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)))} ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆) | ||
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 ∨ 𝑚 = 𝑛)))} ⇒ ⊢ 𝑆 ≈ ℕ | ||
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 𝑁 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |