![]() |
Metamath
Proof Explorer Theorem List (p. 392 of 445) | < 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-28378) |
![]() (28379-29901) |
![]() (29902-44425) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | jm2.27b 39101 | Lemma for jm2.27 39103. Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐸 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ ℕ0) & ⊢ (𝜑 → 𝐺 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1) & ⊢ (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1) & ⊢ (𝜑 → 𝐺 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1) & ⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2)))) & ⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴)) & ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1)) & ⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶)) & ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) | ||
Theorem | jm2.27c 39102 | Lemma for jm2.27 39103. Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) & ⊢ 𝐷 = (𝐴 Xrm 𝐵) & ⊢ 𝑄 = (𝐵 · (𝐴 Yrm 𝐵)) & ⊢ 𝐸 = (𝐴 Yrm (2 · 𝑄)) & ⊢ 𝐹 = (𝐴 Xrm (2 · 𝑄)) & ⊢ 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) & ⊢ 𝐻 = (𝐺 Yrm 𝐵) & ⊢ 𝐼 = (𝐺 Xrm 𝐵) & ⊢ 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1) ⇒ ⊢ (𝜑 → (((𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℕ0) ∧ (𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0)) ∧ (𝐽 ∈ ℕ0 ∧ (((((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ≥‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶)))))) | ||
Theorem | jm2.27 39103* | Lemma 2.27 of [JonesMatijasevic] p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a 39100 and jm2.27c 39102. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine" (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 = (𝐴 Yrm 𝐵) ↔ ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 ∃𝑖 ∈ ℕ0 ∃𝑗 ∈ ℕ0 (((((𝑑↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝑓↑2) − (((𝐴↑2) − 1) · (𝑒↑2))) = 1 ∧ 𝑔 ∈ (ℤ≥‘2)) ∧ (((𝑖↑2) − (((𝑔↑2) − 1) · (ℎ↑2))) = 1 ∧ 𝑒 = ((𝑗 + 1) · (2 · (𝐶↑2))) ∧ 𝑓 ∥ (𝑔 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝑔 − 1) ∧ 𝑓 ∥ (ℎ − 𝐶)) ∧ ((2 · 𝐶) ∥ (ℎ − 𝐵) ∧ 𝐵 ≤ 𝐶))))) | ||
Theorem | jm2.27dlem1 39104* | Lemma for rmydioph 39109. Substitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ (1...𝐵) ⇒ ⊢ (𝑎 = (𝑏 ↾ (1...𝐵)) → (𝑎‘𝐴) = (𝑏‘𝐴)) | ||
Theorem | jm2.27dlem2 39105 | Lemma for rmydioph 39109. This theorem is used along with the next three to efficiently infer steps like 7 ∈ (1...;10). (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ (1...𝐵) & ⊢ 𝐶 = (𝐵 + 1) & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ 𝐴 ∈ (1...𝐶) | ||
Theorem | jm2.27dlem3 39106 | Lemma for rmydioph 39109. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ (1...𝐴) | ||
Theorem | jm2.27dlem4 39107 | Lemma for rmydioph 39109. Infer ℕ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 = (𝐴 + 1) ⇒ ⊢ 𝐵 ∈ ℕ | ||
Theorem | jm2.27dlem5 39108 | Lemma for rmydioph 39109. Used with sselii 3888 to infer membership of midpoints of range; jm2.27dlem2 39105 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐵 = (𝐴 + 1) & ⊢ (1...𝐵) ⊆ (1...𝐶) ⇒ ⊢ (1...𝐴) ⊆ (1...𝐶) | ||
Theorem | rmydioph 39109 | jm2.27 39103 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | rmxdiophlem 39110* | X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0) → (𝑋 = (𝐴 Xrm 𝑁) ↔ ∃𝑦 ∈ ℕ0 (𝑦 = (𝐴 Yrm 𝑁) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1))) | ||
Theorem | rmxdioph 39111 | 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 39112 | Lemma for jm3.1 39115. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐾↑𝑁) < 𝐴) | ||
Theorem | jm3.1lem2 39113 | Lemma for jm3.1 39115. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1)) | ||
Theorem | jm3.1lem3 39114 | Lemma for jm3.1 39115. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℕ) | ||
Theorem | jm3.1 39115 | 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 39116* | Lemma for expdioph 39118. 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 39117 | Lemma for expdioph 39118. 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 39118 | 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 39119* | 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 9025; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → (∃𝑦(Tr 𝑦 ∧ 𝐵 ∈ 𝑦) → 𝐵 ∈ 𝐴)) | ||
Theorem | setindtrs 39120* | Epsilon induction scheme without Infinity. See comments at setindtr 39119. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒) | ||
Theorem | dford3lem1 39121* | Lemma for dford3 39123. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 (Tr 𝑏 ∧ ∀𝑦 ∈ 𝑏 Tr 𝑦)) | ||
Theorem | dford3lem2 39122* | Lemma for dford3 39123. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ ((Tr 𝑥 ∧ ∀𝑦 ∈ 𝑥 Tr 𝑦) → 𝑥 ∈ On) | ||
Theorem | dford3 39123* | Ordinals are precisely the hereditarily transitive classes. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (Ord 𝑁 ↔ (Tr 𝑁 ∧ ∀𝑥 ∈ 𝑁 Tr 𝑥)) | ||
Theorem | dford4 39124* | dford3 39123 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (Ord 𝑁 ↔ ∀𝑎∀𝑏∀𝑐((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ 𝑁 ∧ (𝑐 ∈ 𝑏 → 𝑐 ∈ 𝑎)))) | ||
Theorem | wopprc 39125 | Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬ 1o ∈ {{{𝐴}, ∅}, {{𝐵}}}) | ||
Theorem | rpnnen3lem 39126* | Lemma for rpnnen3 39127. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝑎 < 𝑏) → {𝑐 ∈ ℚ ∣ 𝑐 < 𝑎} ≠ {𝑐 ∈ ℚ ∣ 𝑐 < 𝑏}) | ||
Theorem | rpnnen3 39127 | Dedekind cut injection of ℝ into 𝒫 ℚ. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ ℝ ≼ 𝒫 ℚ | ||
Theorem | axac10 39128 | Characterization of choice similar to dffin1-5 9659. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
⊢ ( ≈ “ On) = V | ||
Theorem | harinf 39129 | The Hartogs number of an infinite set is at least ω. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin) → ω ⊆ (har‘𝑆)) | ||
Theorem | wdom2d2 39130* | Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑥 = 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ≼* (𝐵 × 𝐶)) | ||
Theorem | ttac 39131 | Tarski's theorem about choice: infxpidm 9833 is equivalent to ax-ac 9730. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.) |
⊢ (CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐)) | ||
Theorem | pw2f1ocnv 39132* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8474, 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.) |
⊢ 𝐹 = (𝑥 ∈ (2o ↑𝑚 𝐴) ↦ (◡𝑥 “ {1o})) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹:(2o ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴 ∧ ◡𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))))) | ||
Theorem | pw2f1o2 39133* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8474, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2o ↑𝑚 𝐴) ↦ (◡𝑥 “ {1o})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:(2o ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴) | ||
Theorem | pw2f1o2val 39134* | Function value of the pw2f1o2 39133 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2o ↑𝑚 𝐴) ↦ (◡𝑥 “ {1o})) ⇒ ⊢ (𝑋 ∈ (2o ↑𝑚 𝐴) → (𝐹‘𝑋) = (◡𝑋 “ {1o})) | ||
Theorem | pw2f1o2val2 39135* | Membership in a mapped set under the pw2f1o2 39133 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (2o ↑𝑚 𝐴) ↦ (◡𝑥 “ {1o})) ⇒ ⊢ ((𝑋 ∈ (2o ↑𝑚 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋‘𝑌) = 1o)) | ||
Theorem | soeq12d 39136 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) | ||
Theorem | freq12d 39137 | Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵)) | ||
Theorem | weeq12d 39138 | Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵)) | ||
Theorem | limsuc2 39139 | 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 39140* | Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))} & ⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝐹 = (𝑎 ∈ (2o ↑𝑚 𝐴) ↦ (◡𝑎 “ {1o})) ⇒ ⊢ (𝐴 ∈ V → 𝐹 Isom 𝑈, 𝑇 ((2o ↑𝑚 𝐴), 𝒫 𝐴)) | ||
Theorem | wepwso 39141* | 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 39142* | Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 9305. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) | ||
Theorem | dnnumch2 39143* | 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 39144* | Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) ⇒ ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) | ||
Theorem | dnnumch3 39145* | 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 39146* | Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) & ⊢ 𝐻 = {〈𝑣, 𝑤〉 ∣ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})} ⇒ ⊢ (𝜑 → 𝐻 We 𝐴) | ||
Theorem | fnwe2val 39147* | Lemma for fnwe2 39151. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} ⇒ ⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) | ||
Theorem | fnwe2lem1 39148* | Lemma for fnwe2 39151. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | ||
Theorem | fnwe2lem2 39149* | Lemma for fnwe2 39151. 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 39150* | Lemma for fnwe2 39151. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) & ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑎 ∈ 𝐴) & ⊢ (𝜑 → 𝑏 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | ||
Theorem | fnwe2 39151* | 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 7682 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 39152* |
Lemma for dfac11 39160. 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 indices 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 39153* | Lemma for dfac11 39160. 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 39154* | Lemma for dfac11 39160. 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 39155* | Lemma for dfac11 39160. Limit case. Patch together well-orderings constructed so far using fnwe2 39151 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 39156* | Lemma for dfac11 39160. 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 39157* | Lemma for dfac11 39160. 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 39158* | Lemma for dfac11 39160. (𝑅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 39159* | Lemma for dfac11 39160. 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 39160* |
The right-hand side of this theorem (compare with ac4 9746),
sometimes
known as the "axiom of multiple choice", is a choice
equivalent.
Curiously, this statement cannot be proved without ax-reg 8905, 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 39161* | 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 39162 | Lemma for kelac2 39163 and dfac21 39164: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪ 𝑆}}) ∈ Comp) | ||
Theorem | kelac2 39163* | 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 39164 | 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 39165 | Extend class notation with the class of finitely generated left modules. |
class LFinGen | ||
Definition | df-lfig 39166 | 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 39167* | Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ (𝑊 ∈ LMod → (𝑊 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝐵(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝐵))) | ||
Theorem | islssfg 39168* | Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝑈(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝑈))) | ||
Theorem | islssfg2 39169* | 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 39170 | Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑋 = (𝑊 ↾s (𝑁‘𝐵)) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin) → 𝑋 ∈ LFinGen) | ||
Theorem | fglmod 39171 | Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ (𝑀 ∈ LFinGen → 𝑀 ∈ LMod) | ||
Theorem | lsmfgcl 39172 | 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 39173 | Extend class notation with the class of Noetherian left modules. |
class LNoeM | ||
Definition | df-lnm 39174* | 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 39175* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ 𝑆 = (LSubSp‘𝑀) ⇒ ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen)) | ||
Theorem | islnm2 39176* | 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 39177 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod) | ||
Theorem | lnmlssfg 39178 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (𝑀 ↾s 𝑈) ⇒ ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen) | ||
Theorem | lnmlsslnm 39179 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
⊢ 𝑆 = (LSubSp‘𝑀) & ⊢ 𝑅 = (𝑀 ↾s 𝑈) ⇒ ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM) | ||
Theorem | lnmfg 39180 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen) | ||
Theorem | kercvrlsm 39181 | 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 39182 | 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 39183 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM) | ||
Theorem | lmhmfgsplit 39184 | 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 39185 | 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 39186 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑚 𝑆 → (𝑅 ∈ LNoeM ↔ 𝑆 ∈ LNoeM)) | ||
Theorem | pwssplit4 39187* | 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 39188 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM) | ||
Theorem | pwslnmlem0 39189 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s ∅) ⇒ ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM) | ||
Theorem | pwslnmlem1 39190* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s {𝑖}) ⇒ ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM) | ||
Theorem | pwslnmlem2 39191 | 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 39192 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑊 ↑s 𝐼) ⇒ ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM) | ||
Theorem | unxpwdom3 39193* | Weaker version of unxpwdom 8902 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 39194* | The pw2f1o 8472 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.) |
⊢ 𝑆 = {𝑦 ∈ (2o ↑𝑚 𝐴) ∣ 𝑦 finSupp ∅} & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1o})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin)) | ||
Theorem | pwfi2en 39195* | Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
⊢ 𝑆 = {𝑦 ∈ (2o ↑𝑚 𝐴) ∣ 𝑦 finSupp ∅} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑆 ≈ (𝒫 𝐴 ∩ Fin)) | ||
Theorem | frlmpwfi 39196 | 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 39197 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel)) | ||
Theorem | imasgim 39198 | 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 | isnumbasgrplem1 39199 | 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 39200 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |