![]() |
Metamath
Proof Explorer Theorem List (p. 367 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-27159) |
![]() (27160-28684) |
![]() (28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rmxdioph 36601 | X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | jm3.1lem1 36602 | Lemma for jm3.1 36605. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐾↑𝑁) < 𝐴) | ||
Theorem | jm3.1lem2 36603 | Lemma for jm3.1 36605. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1)) | ||
Theorem | jm3.1lem3 36604 | Lemma for jm3.1 36605. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℕ) | ||
Theorem | jm3.1 36605 | Diophantine expression for exponentiation. Lemma 3.1 of [JonesMatijasevic] p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾↑𝑁) = (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) mod ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1))) | ||
Theorem | expdiophlem1 36606* | Lemma for expdioph 36608. Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ (𝐶 ∈ ℕ0 → (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ) ∧ 𝐶 = (𝐴↑𝐵)) ↔ ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ) ∧ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑑 = (𝐴 Yrm (𝐵 + 1))) ∧ ((𝑑 ∈ (ℤ≥‘2) ∧ 𝑒 = (𝑑 Yrm 𝐵)) ∧ ((𝑑 ∈ (ℤ≥‘2) ∧ 𝑓 = (𝑑 Xrm 𝐵)) ∧ (𝐶 < ((((2 · 𝑑) · 𝐴) − (𝐴↑2)) − 1) ∧ ((((2 · 𝑑) · 𝐴) − (𝐴↑2)) − 1) ∥ ((𝑓 − ((𝑑 − 𝐴) · 𝑒)) − 𝐶)))))))) | ||
Theorem | expdiophlem2 36607 | Lemma for expdioph 36608. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | expdioph 36608 | The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))} ∈ (Dioph‘3) | ||
Theorem | setindtr 36609* | Epsilon induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind 8493; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → (∃𝑦(Tr 𝑦 ∧ 𝐵 ∈ 𝑦) → 𝐵 ∈ 𝐴)) | ||
Theorem | setindtrs 36610* | Epsilon induction scheme without Infinity. See comments at setindtr 36609. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒) | ||
Theorem | dford3lem1 36611* | Lemma for dford3 36613. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 (Tr 𝑏 ∧ ∀𝑦 ∈ 𝑏 Tr 𝑦)) | ||
Theorem | dford3lem2 36612* | Lemma for dford3 36613. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ ((Tr 𝑥 ∧ ∀𝑦 ∈ 𝑥 Tr 𝑦) → 𝑥 ∈ On) | ||
Theorem | dford3 36613* | Ordinals are precisely the hereditarily transitive classes. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (Ord 𝑁 ↔ (Tr 𝑁 ∧ ∀𝑥 ∈ 𝑁 Tr 𝑥)) | ||
Theorem | dford4 36614* | dford3 36613 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (Ord 𝑁 ↔ ∀𝑎∀𝑏∀𝑐((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ 𝑁 ∧ (𝑐 ∈ 𝑏 → 𝑐 ∈ 𝑎)))) | ||
Theorem | wopprc 36615 | Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬ 1𝑜 ∈ {{{𝐴}, ∅}, {{𝐵}}}) | ||
Theorem | rpnnen3lem 36616* | Lemma for rpnnen3 36617. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝑎 < 𝑏) → {𝑐 ∈ ℚ ∣ 𝑐 < 𝑎} ≠ {𝑐 ∈ ℚ ∣ 𝑐 < 𝑏}) | ||
Theorem | rpnnen3 36617 | Dedekind cut injection of ℝ into 𝒫 ℚ. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ ℝ ≼ 𝒫 ℚ | ||
Theorem | axac10 36618 | Characterization of choice similar to dffin1-5 9093. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
⊢ ( ≈ “ On) = V | ||
Theorem | harinf 36619 | The Hartogs number of an infinite set is at least ω. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin) → ω ⊆ (har‘𝑆)) | ||
Theorem | wdom2d2 36620* | Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑥 = 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ≼* (𝐵 × 𝐶)) | ||
Theorem | ttac 36621 | Tarski's theorem about choice: infxpidm 9263 is equivalent to ax-ac 9164. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.) |
⊢ (CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) | ||
Theorem | pw2f1ocnv 36622* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 7952, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2𝑜 ↑𝑚 𝐴) ↦ (◡𝑥 “ {1𝑜})) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹:(2𝑜 ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴 ∧ ◡𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))))) | ||
Theorem | pw2f1o2 36623* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 7952, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2𝑜 ↑𝑚 𝐴) ↦ (◡𝑥 “ {1𝑜})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:(2𝑜 ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴) | ||
Theorem | pw2f1o2val 36624* | Function value of the pw2f1o2 36623 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2𝑜 ↑𝑚 𝐴) ↦ (◡𝑥 “ {1𝑜})) ⇒ ⊢ (𝑋 ∈ (2𝑜 ↑𝑚 𝐴) → (𝐹‘𝑋) = (◡𝑋 “ {1𝑜})) | ||
Theorem | pw2f1o2val2 36625* | Membership in a mapped set under the pw2f1o2 36623 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2𝑜 ↑𝑚 𝐴) ↦ (◡𝑥 “ {1𝑜})) ⇒ ⊢ ((𝑋 ∈ (2𝑜 ↑𝑚 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋‘𝑌) = 1𝑜)) | ||
Theorem | soeq12d 36626 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) | ||
Theorem | freq12d 36627 | Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵)) | ||
Theorem | weeq12d 36628 | Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵)) | ||
Theorem | limsuc2 36629 | Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ ((Ord 𝐴 ∧ 𝐴 = ∪ 𝐴) → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) | ||
Theorem | wepwsolem 36630* | Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))} & ⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝐹 = (𝑎 ∈ (2𝑜 ↑𝑚 𝐴) ↦ (◡𝑎 “ {1𝑜})) ⇒ ⊢ (𝐴 ∈ V → 𝐹 Isom 𝑈, 𝑇 ((2𝑜 ↑𝑚 𝐴), 𝒫 𝐴)) | ||
Theorem | wepwso 36631* | A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove 𝐴 ∈ 𝑉. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → 𝑇 Or 𝒫 𝐴) | ||
Theorem | dnnumch1 36632* | Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 8736. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) | ||
Theorem | dnnumch2 36633* | Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) | ||
Theorem | dnnumch3lem 36634* | Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) ⇒ ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) | ||
Theorem | dnnumch3 36635* | Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On) | ||
Theorem | dnwech 36636* | Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) & ⊢ 𝐻 = {〈𝑣, 𝑤〉 ∣ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})} ⇒ ⊢ (𝜑 → 𝐻 We 𝐴) | ||
Theorem | fnwe2val 36637* | Lemma for fnwe2 36641. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} ⇒ ⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) | ||
Theorem | fnwe2lem1 36638* | Lemma for fnwe2 36641. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | ||
Theorem | fnwe2lem2 36639* | Lemma for fnwe2 36641. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus 𝑇 is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) & ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑎 ⊆ 𝐴) & ⊢ (𝜑 → 𝑎 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏) | ||
Theorem | fnwe2lem3 36640* | Lemma for fnwe2 36641. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) & ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑎 ∈ 𝐴) & ⊢ (𝜑 → 𝑏 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | ||
Theorem | fnwe2 36641* | A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 7180 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) & ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | aomclem1 36642* |
Lemma for dfac11 36650. This is the beginning of the proof that
multiple
choice is equivalent to choice. Our goal is to construct, by
transfinite recursion, a well-ordering of (𝑅1‘𝐴). In what
follows, 𝐴 is the index of the rank we wish to
well-order, 𝑧 is
the collection of well-orderings constructed so far, dom 𝑧 is
the
set of ordinal indexes of constructed ranks i.e. the next rank to
construct, and 𝑦 is a postulated multiple-choice
function.
Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} & ⊢ (𝜑 → dom 𝑧 ∈ On) & ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) ⇒ ⊢ (𝜑 → 𝐵 Or (𝑅1‘dom 𝑧)) | ||
Theorem | aomclem2 36643* | Lemma for dfac11 36650. Successor case 2, a choice function for subsets of (𝑅1‘dom 𝑧). (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} & ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) & ⊢ (𝜑 → dom 𝑧 ∈ On) & ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}))) ⇒ ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘dom 𝑧)(𝑎 ≠ ∅ → (𝐶‘𝑎) ∈ 𝑎)) | ||
Theorem | aomclem3 36644* | Lemma for dfac11 36650. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} & ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) & ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎)))) & ⊢ 𝐸 = {〈𝑎, 𝑏〉 ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})} & ⊢ (𝜑 → dom 𝑧 ∈ On) & ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}))) ⇒ ⊢ (𝜑 → 𝐸 We (𝑅1‘dom 𝑧)) | ||
Theorem | aomclem4 36645* | Lemma for dfac11 36650. Limit case. Patch together well-orderings constructed so far using fnwe2 36641 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} & ⊢ (𝜑 → dom 𝑧 ∈ On) & ⊢ (𝜑 → dom 𝑧 = ∪ dom 𝑧) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) ⇒ ⊢ (𝜑 → 𝐹 We (𝑅1‘dom 𝑧)) | ||
Theorem | aomclem5 36646* | Lemma for dfac11 36650. Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} & ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) & ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎)))) & ⊢ 𝐸 = {〈𝑎, 𝑏〉 ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})} & ⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} & ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) & ⊢ (𝜑 → dom 𝑧 ∈ On) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎)) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}))) ⇒ ⊢ (𝜑 → 𝐺 We (𝑅1‘dom 𝑧)) | ||
Theorem | aomclem6 36647* | Lemma for dfac11 36650. Transfinite induction, close over 𝑧. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} & ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) & ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎)))) & ⊢ 𝐸 = {〈𝑎, 𝑏〉 ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})} & ⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} & ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) & ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺)) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}))) ⇒ ⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴)) | ||
Theorem | aomclem7 36648* | Lemma for dfac11 36650. (𝑅1‘𝐴) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ 𝐵 = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))} & ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵)) & ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎)))) & ⊢ 𝐸 = {〈𝑎, 𝑏〉 ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})} & ⊢ 𝐹 = {〈𝑎, 𝑏〉 ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))} & ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧))) & ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺)) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}))) ⇒ ⊢ (𝜑 → ∃𝑏 𝑏 We (𝑅1‘𝐴)) | ||
Theorem | aomclem8 36649* | Lemma for dfac11 36650. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}))) ⇒ ⊢ (𝜑 → ∃𝑏 𝑏 We (𝑅1‘𝐴)) | ||
Theorem | dfac11 36650* |
The right-hand side of this theorem (compare with ac4 9180),
sometimes
known as the "axiom of multiple choice", is a choice
equivalent.
Curiously, this statement cannot be proved without ax-reg 8380, despite
not mentioning the cumulative hierarchy in any way as most consequences
of regularity do.
This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.) |
⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ ((𝒫 𝑧 ∩ Fin) ∖ {∅}))) | ||
Theorem | kelac1 36651* | Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ∈ (Clsd‘𝐽)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽) & ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅) | ||
Theorem | kelac2lem 36652 | Lemma for kelac2 36653 and dfac21 36654: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪ 𝑆}}) ∈ Comp) | ||
Theorem | kelac2 36653* | Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) & ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ (topGen‘{𝑆, {𝒫 ∪ 𝑆}}))) ∈ Comp) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅) | ||
Theorem | dfac21 36654 | Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.) |
⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp)) | ||
Syntax | clfig 36655 | Extend class notation with the class of finitely generated left modules. |
class LFinGen | ||
Definition | df-lfig 36656 | Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using ↾s. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ LFinGen = {𝑤 ∈ LMod ∣ (Base‘𝑤) ∈ ((LSpan‘𝑤) “ (𝒫 (Base‘𝑤) ∩ Fin))} | ||
Theorem | islmodfg 36657* | Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑊 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝐵(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝐵))) | ||
Theorem | islssfg 36658* | Property of a finitely generated left (sub-)module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝑈(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝑈))) | ||
Theorem | islssfg2 36659* | Property of a finitely generated left (sub-)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑁‘𝑏) = 𝑈)) | ||
Theorem | islssfgi 36660 | Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s (𝑁‘𝐵)) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin) → 𝑋 ∈ LFinGen) | ||
Theorem | fglmod 36661 | Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝑀 ∈ LFinGen → 𝑀 ∈ LMod) | ||
Theorem | lsmfgcl 36662 | The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑈 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐷 = (𝑊 ↾s 𝐴) & ⊢ 𝐸 = (𝑊 ↾s 𝐵) & ⊢ 𝐹 = (𝑊 ↾s (𝐴 ⊕ 𝐵)) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ LFinGen) & ⊢ (𝜑 → 𝐸 ∈ LFinGen) ⇒ ⊢ (𝜑 → 𝐹 ∈ LFinGen) | ||
Syntax | clnm 36663 | Extend class notation with the class of Noetherian left modules. |
class LNoeM | ||
Definition | df-lnm 36664* | A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen} | ||
Theorem | islnm 36665* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑀) ⇒ ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen)) | ||
Theorem | islnm2 36666* | Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑁 = (LSpan‘𝑀) ⇒ ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 ∃𝑔 ∈ (𝒫 𝐵 ∩ Fin)𝑖 = (𝑁‘𝑔))) | ||
Theorem | lnmlmod 36667 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod) | ||
Theorem | lnmlssfg 36668 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (𝑀 ↾s 𝑈) ⇒ ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen) | ||
Theorem | lnmlsslnm 36669 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (𝑀 ↾s 𝑈) ⇒ ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM) | ||
Theorem | lnmfg 36670 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen) | ||
Theorem | kercvrlsm 36671 | The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ 𝑈 = (LSubSp‘𝑆) & ⊢ ⊕ = (LSSum‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → (𝐹 “ 𝐷) = ran 𝐹) ⇒ ⊢ (𝜑 → (𝐾 ⊕ 𝐷) = 𝐵) | ||
Theorem | lmhmfgima 36672 | A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑇 ↾s (𝐹 “ 𝐴)) & ⊢ 𝑋 = (𝑆 ↾s 𝐴) & ⊢ 𝑈 = (LSubSp‘𝑆) & ⊢ (𝜑 → 𝑋 ∈ LFinGen) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) ⇒ ⊢ (𝜑 → 𝑌 ∈ LFinGen) | ||
Theorem | lnmepi 36673 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM) | ||
Theorem | lmhmfgsplit 36674 | If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ 0 = (0g‘𝑇) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑈 = (𝑆 ↾s 𝐾) & ⊢ 𝑉 = (𝑇 ↾s ran 𝐹) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen) → 𝑆 ∈ LFinGen) | ||
Theorem | lmhmlnmsplit 36675 | If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 12-Jun-2015.) |
⊢ 0 = (0g‘𝑇) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑈 = (𝑆 ↾s 𝐾) & ⊢ 𝑉 = (𝑇 ↾s ran 𝐹) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LNoeM) | ||
Theorem | lnmlmic 36676 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → (𝑅 ∈ LNoeM ↔ 𝑆 ∈ LNoeM)) | ||
Theorem | pwssplit4 36677* | Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐸 = (𝑅 ↑s (𝐴 ∪ 𝐵)) & ⊢ 𝐺 = (Base‘𝐸) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (𝐴 × { 0 })} & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ↾ 𝐵)) & ⊢ 𝐶 = (𝑅 ↑s 𝐴) & ⊢ 𝐷 = (𝑅 ↑s 𝐵) & ⊢ 𝐿 = (𝐸 ↾s 𝐾) ⇒ ⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹 ∈ (𝐿 LMIso 𝐷)) | ||
Theorem | filnm 36678 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM) | ||
Theorem | pwslnmlem0 36679 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s ∅) ⇒ ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM) | ||
Theorem | pwslnmlem1 36680* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s {𝑖}) ⇒ ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM) | ||
Theorem | pwslnmlem2 36681 | A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑋 = (𝑊 ↑s 𝐴) & ⊢ 𝑌 = (𝑊 ↑s 𝐵) & ⊢ 𝑍 = (𝑊 ↑s (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑋 ∈ LNoeM) & ⊢ (𝜑 → 𝑌 ∈ LNoeM) ⇒ ⊢ (𝜑 → 𝑍 ∈ LNoeM) | ||
Theorem | pwslnm 36682 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝐼) ⇒ ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
Theorem | unxpwdom3 36683* | Weaker version of unxpwdom 8377 where a function is required only to be cancellative, not an injection. 𝐷 and 𝐵 are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into 𝐴, each row must hit an element of 𝐵; by column injectivity, each row can be identified in at least one way by the 𝐵 element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵)) & ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)) & ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎)) & ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴) ⇒ ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵)) | ||
Theorem | pwfi2f1o 36684* | The pw2f1o 7950 bijection relates finitely supported indicator functions on a two-element set to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
⊢ 𝑆 = {𝑦 ∈ (2𝑜 ↑𝑚 𝐴) ∣ 𝑦 finSupp ∅} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1𝑜})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin)) | ||
Theorem | pwfi2en 36685* | Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
⊢ 𝑆 = {𝑦 ∈ (2𝑜 ↑𝑚 𝐴) ∣ 𝑦 finSupp ∅} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑆 ≈ (𝒫 𝐴 ∩ Fin)) | ||
Theorem | frlmpwfi 36686 | Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.) |
⊢ 𝑅 = (ℤ/nℤ‘2) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐵 ≈ (𝒫 𝐼 ∩ Fin)) | ||
Theorem | gicabl 36687 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) | ||
Theorem | imasgim 36688 | A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpIso 𝑈)) | ||
Theorem | basfn 36689 | Functionality of the base set extractor. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ Base Fn V | ||
Theorem | isnumbasgrplem1 36690 | A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Abel ∧ 𝐶 ≈ 𝐵) → 𝐶 ∈ (Base “ Abel)) | ||
Theorem | harn0 36691 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅) | ||
Theorem | numinfctb 36692 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆) | ||
Theorem | isnumbasgrplem2 36693 | If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ ((𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp) → 𝑆 ∈ dom card) | ||
Theorem | isnumbasgrplem3 36694 | Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015.) |
⊢ ((𝑆 ∈ dom card ∧ 𝑆 ≠ ∅) → 𝑆 ∈ (Base “ Abel)) | ||
Theorem | isnumbasabl 36695 | A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (𝑆 ∈ dom card ↔ (𝑆 ∪ (har‘𝑆)) ∈ (Base “ Abel)) | ||
Theorem | isnumbasgrp 36696 | A set is numerable iff it and its Hartogs number can be jointly given the structure of a group. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (𝑆 ∈ dom card ↔ (𝑆 ∪ (har‘𝑆)) ∈ (Base “ Grp)) | ||
Theorem | dfacbasgrp 36697 | A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (CHOICE ↔ (Base “ Grp) = (V ∖ {∅})) | ||
Syntax | clnr 36698 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 36699 | A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM} | ||
Theorem | islnr 36700 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ LNoeR ↔ (𝐴 ∈ Ring ∧ (ringLMod‘𝐴) ∈ LNoeM)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |