![]() |
Intuitionistic Logic Explorer Theorem List (p. 120 of 135) | < 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 | qnumdencl 11901 | Lemma for qnumcl 11902 and qdencl 11903. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) ∈ ℤ ∧ (denom‘𝐴) ∈ ℕ)) | ||
Theorem | qnumcl 11902 | The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) ∈ ℤ) | ||
Theorem | qdencl 11903 | The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) ∈ ℕ) | ||
Theorem | fnum 11904 | Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ numer:ℚ⟶ℤ | ||
Theorem | fden 11905 | Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ denom:ℚ⟶ℕ | ||
Theorem | qnumdenbi 11906 | Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (((𝐵 gcd 𝐶) = 1 ∧ 𝐴 = (𝐵 / 𝐶)) ↔ ((numer‘𝐴) = 𝐵 ∧ (denom‘𝐴) = 𝐶))) | ||
Theorem | qnumdencoprm 11907 | The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) gcd (denom‘𝐴)) = 1) | ||
Theorem | qeqnumdivden 11908 | Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → 𝐴 = ((numer‘𝐴) / (denom‘𝐴))) | ||
Theorem | qmuldeneqnum 11909 | Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (𝐴 · (denom‘𝐴)) = (numer‘𝐴)) | ||
Theorem | divnumden 11910 | Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵)))) | ||
Theorem | divdenle 11911 | Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (denom‘(𝐴 / 𝐵)) ≤ 𝐵) | ||
Theorem | qnumgt0 11912 | A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (0 < 𝐴 ↔ 0 < (numer‘𝐴))) | ||
Theorem | qgt0numnn 11913 | A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → (numer‘𝐴) ∈ ℕ) | ||
Theorem | nn0gcdsq 11914 | Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2))) | ||
Theorem | zgcdsq 11915 | nn0gcdsq 11914 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2))) | ||
Theorem | numdensq 11916 | Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((numer‘(𝐴↑2)) = ((numer‘𝐴)↑2) ∧ (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2))) | ||
Theorem | numsq 11917 | Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (numer‘(𝐴↑2)) = ((numer‘𝐴)↑2)) | ||
Theorem | densq 11918 | Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2)) | ||
Theorem | qden1elz 11919 | A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((denom‘𝐴) = 1 ↔ 𝐴 ∈ ℤ)) | ||
Theorem | nn0sqrtelqelz 11920 | If a nonnegative integer has a rational square root, that root must be an integer. (Contributed by Jim Kingdon, 24-May-2022.) |
⊢ ((𝐴 ∈ ℕ0 ∧ (√‘𝐴) ∈ ℚ) → (√‘𝐴) ∈ ℤ) | ||
Theorem | nonsq 11921 | Any integer strictly between two adjacent squares has a non-rational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐵↑2) < 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))) → ¬ (√‘𝐴) ∈ ℚ) | ||
Syntax | cphi 11922 | Extend class notation with the Euler phi function. |
class ϕ | ||
Definition | df-phi 11923* | Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than 𝑛 and coprime to it, see definition in [ApostolNT] p. 25. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1})) | ||
Theorem | phivalfi 11924* | Finiteness of an expression used to define the Euler ϕ function. (Contributed by Jim Kingon, 28-May-2022.) |
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ∈ Fin) | ||
Theorem | phival 11925* | Value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) | ||
Theorem | phicl2 11926 | Bounds and closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ (1...𝑁)) | ||
Theorem | phicl 11927 | Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ) | ||
Theorem | phibndlem 11928* | Lemma for phibnd 11929. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...(𝑁 − 1))) | ||
Theorem | phibnd 11929 | A slightly tighter bound on the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (ϕ‘𝑁) ≤ (𝑁 − 1)) | ||
Theorem | phicld 11930 | Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ) | ||
Theorem | phi1 11931 | Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (ϕ‘1) = 1 | ||
Theorem | dfphi2 11932* | Alternate definition of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1})) | ||
Theorem | hashdvds 11933* | 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) − 𝐶) / 𝑁)))) | ||
Theorem | phiprmpw 11934 | 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))) | ||
Theorem | phiprm 11935 | Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1)) | ||
Theorem | crth 11936* | 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→𝑇) | ||
Theorem | phimullem 11937* | Lemma for phimul 11938. (Contributed by Mario Carneiro, 24-Feb-2014.) |
⊢ 𝑆 = (0..^(𝑀 · 𝑁)) & ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁)) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) & ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) & ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} & ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} & ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⇒ ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁))) | ||
Theorem | phimul 11938 | 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) → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁))) | ||
Theorem | hashgcdlem 11939* | 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→𝐵) | ||
Theorem | hashgcdeq 11940* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (0..^𝑀) ∣ (𝑥 gcd 𝑀) = 𝑁}) = if(𝑁 ∥ 𝑀, (ϕ‘(𝑀 / 𝑁)), 0)) | ||
Theorem | oddennn 11941 | There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.) |
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ | ||
Theorem | evenennn 11942 | There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.) |
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈ ℕ | ||
Theorem | xpnnen 11943 | 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 11944 | 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 11945 | The cartesian product of two sets dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) | ||
Theorem | unennn 11946 | The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.) |
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ) | ||
Theorem | znnen 11947 | 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 11948* | Lemma for ennnfone 11974. A direct consequence of fidcenumlemrk 6850. (Contributed by Jim Kingdon, 15-Jul-2023.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:ω–onto→𝐴) & ⊢ (𝜑 → 𝑃 ∈ ω) ⇒ ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃)) | ||
Theorem | ennnfonelemk 11949* | Lemma for ennnfone 11974. (Contributed by Jim Kingdon, 15-Jul-2023.) |
⊢ (𝜑 → 𝐹:ω–onto→𝐴) & ⊢ (𝜑 → 𝐾 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝐾) | ||
Theorem | ennnfonelemj0 11950* | Lemma for ennnfone 11974. 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 11951* | Lemma for ennnfone 11974. 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 11952* | Lemma for ennnfone 11974. 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 11953* | Lemma for ennnfone 11974. (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 11954* | Lemma for ennnfone 11974. 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 11955* | Lemma for ennnfone 11974. 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 11956* | Lemma for ennnfone 11974. 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 11957* | Lemma for ennnfone 11974. 𝐻 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 11958* | Lemma for ennnfone 11974. 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 11959* | Lemma for ennnfone 11974. 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 11960* | Lemma for ennnfone 11974. 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 11961* | Lemma for ennnfone 11974. 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 11962* | Lemma for ennnfone 11974. 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 11963* | Lemma for ennnfone 11974. 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 11964* | Lemma for ennnfone 11974. 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 11965* | Lemma for ennnfone 11974. A consequence of ennnfonelemss 11959. (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 11966* | Lemma for ennnfone 11974. 𝐿 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 11967* | Lemma for ennnfone 11974. 𝐿 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 11968* | Lemma for ennnfone 11974. 𝐿 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 11969* | Lemma for ennnfone 11974. 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 11970* | Lemma for ennnfone 11974. 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 11971* | Lemma for ennnfone 11974. A version of ennnfonelemen 11970 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 11972* | Lemma for ennnfone 11974. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝐴 ≈ ℕ) | ||
Theorem | ennnfonelemim 11973* | Lemma for ennnfone 11974. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
⊢ (𝐴 ≈ ℕ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗)))) | ||
Theorem | ennnfone 11974* | 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 7002), 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 11975* | 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 11976* | Lemma for ctinfom 11977. Converting between ω and ℕ0. (Contributed by Jim Kingdon, 10-Aug-2023.) |
⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐺 = (𝐹 ∘ ◡𝑁) & ⊢ (𝜑 → 𝐹:ω–onto→𝐴) & ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹‘𝑘) ∈ (𝐹 “ 𝑛)) ⇒ ⊢ (𝜑 → (𝐺:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0 ∀𝑖 ∈ (0...𝑚)(𝐺‘𝑗) ≠ (𝐺‘𝑖))) | ||
Theorem | ctinfom 11977* | A condition for a set being countably infinite. Restates ennnfone 11974 in terms of ω and function image. Like ennnfone 11974 the condition can be summarized as 𝐴 being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
⊢ (𝐴 ≈ ℕ ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)))) | ||
Theorem | inffinp1 11978* | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → ω ≼ 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | ctinf 11979* | 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 11980 | 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 11981* | Lemma for enct 11982. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) | ||
Theorem | enct 11982* | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) | ||
Theorem | ctiunctlemu1st 11983* | Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵) & ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} & ⊢ (𝜑 → 𝑁 ∈ 𝑈) ⇒ ⊢ (𝜑 → (1st ‘(𝐽‘𝑁)) ∈ 𝑆) | ||
Theorem | ctiunctlemu2nd 11984* | Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵) & ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} & ⊢ (𝜑 → 𝑁 ∈ 𝑈) ⇒ ⊢ (𝜑 → (2nd ‘(𝐽‘𝑁)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑁))) / 𝑥⦌𝑇) | ||
Theorem | ctiunctlemuom 11985 | Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵) & ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} ⇒ ⊢ (𝜑 → 𝑈 ⊆ ω) | ||
Theorem | ctiunctlemudc 11986* | Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵) & ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} ⇒ ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑈) | ||
Theorem | ctiunctlemf 11987* | Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵) & ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} & ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛)))) ⇒ ⊢ (𝜑 → 𝐻:𝑈⟶∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | ctiunctlemfo 11988* | Lemma for ctiunct 11989. (Contributed by Jim Kingdon, 28-Oct-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵) & ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} & ⊢ 𝐻 = (𝑛 ∈ 𝑈 ↦ (⦋(𝐹‘(1st ‘(𝐽‘𝑛))) / 𝑥⦌𝐺‘(2nd ‘(𝐽‘𝑛)))) & ⊢ Ⅎ𝑥𝐻 & ⊢ Ⅎ𝑥𝑈 ⇒ ⊢ (𝜑 → 𝐻:𝑈–onto→∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | ctiunct 11989* |
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 11991, in which case we express countability using ∃. The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11944) 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 7004 and ctssdc 7006. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o)) ⇒ ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) | ||
Theorem | ctiunctal 11990* | Variation of ctiunct 11989 which allows 𝑥 to be present in 𝜑. (Contributed by Jim Kingdon, 5-May-2024.) |
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐺:ω–onto→(𝐵 ⊔ 1o)) ⇒ ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) | ||
Theorem | unct 11991* | 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 11992* | 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 11993* | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 11989 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
⊢ (𝜑 → CCHOICE) & ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) ⇒ ⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ ω 𝐵 ⊔ 1o)) | ||
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 12022 and strslfv 12042. 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 12006. 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 11994 | Extend class notation with the class of structures with components numbered below 𝐴. |
class Struct | ||
Syntax | cnx 11995 | Extend class notation with the structure component index extractor. |
class ndx | ||
Syntax | csts 11996 | Set components of a structure. |
class sSet | ||
Syntax | cslot 11997 | Extend class notation with the slot function. |
class Slot 𝐴 | ||
Syntax | cbs 11998 | Extend class notation with the class of all base set extractors. |
class Base | ||
Syntax | cress 11999 | Extend class notation with the extensible structure builder restriction operator. |
class ↾s | ||
Definition | df-struct 12000* |
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 5149, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12011: 𝐹 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 3734). (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ Struct = {〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |