| Metamath
Proof Explorer Theorem List (p. 443 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | int-eqtransd 44201 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
| Theorem | int-eqmvtd 44202 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷)) | ||
| Theorem | int-eqineqd 44203 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
| Theorem | int-ineqmvtd 44204 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶) | ||
| Theorem | int-ineq1stprincd 44205 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶)) | ||
| Theorem | int-ineq2ndprincd 44206 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶)) | ||
| Theorem | int-ineqtransd 44207 | InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≤ 𝐴) | ||
This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12748 addcomli 11453 00id 11436 addridi 11448 addlidi 11449 eqid 2737 dec0h 12755 decadd 12787 decaddc 12788. | ||
| Theorem | unitadd 44208 | Theorem used in conjunction with decaddc 12788 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝐴 + 𝐵) = 𝐹 & ⊢ (𝐶 + 1) = 𝐵 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐶) + 1) = 𝐹 | ||
| Theorem | gsumws3 44209 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg 〈“𝑆𝑇𝑈”〉) = (𝑆 + (𝑇 + 𝑈))) | ||
| Theorem | gsumws4 44210 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg 〈“𝑆𝑇𝑈𝑉”〉) = (𝑆 + (𝑇 + (𝑈 + 𝑉)))) | ||
| Theorem | amgm2d 44211 | Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 27033. (Contributed by Stanislas Polu, 8-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2)) | ||
| Theorem | amgm3d 44212 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
| Theorem | amgm4d 44213 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
| Theorem | spALT 44214 | sp 2183 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2183 instead. (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | elnelneqd 44215 | Two classes are not equal if there is an element of one which is not an element of the other. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) | ||
| Theorem | elnelneq2d 44216 | Two classes are not equal if one but not the other is an element of a given class. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) | ||
| Theorem | rr-spce 44217* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
| Theorem | rexlimdvaacbv 44218* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3156. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
| Theorem | rexlimddvcbvw 44219* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44218. The equivalent of this theorem without the bound variable change is rexlimddv 3161. Version of rexlimddvcbv 44220 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by GG, 2-Apr-2024.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | rexlimddvcbv 44220* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44218. The equivalent of this theorem without the bound variable change is rexlimddv 3161. Usage of this theorem is discouraged because it depends on ax-13 2377, see rexlimddvcbvw 44219 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | rr-elrnmpt3d 44221* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
| Theorem | rr-phpd 44222 | Equivalent of php 9247 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ω) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | suceqd 44223 | Deduction associated with suceq 6450. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → suc 𝐴 = suc 𝐵) | ||
| Theorem | tfindsd 44224* | Deduction associated with tfinds 7881. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → 𝜂) | ||
| Syntax | cmnring 44225 | Extend class notation with the monoid ring function. |
| class MndRing | ||
| Definition | df-mnring 44226* | Define the monoid ring function. This takes a monoid 𝑀 and a ring 𝑅 and produces a free left module over 𝑅 with a product extending the monoid function on 𝑀. (Contributed by Rohan Ridenour, 13-May-2024.) |
| ⊢ MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet 〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉)) | ||
| Theorem | mnringvald 44227* | Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 = (𝑉 sSet 〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))〉)) | ||
| Theorem | mnringnmulrd 44228 | Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (Revised by AV, 1-Nov-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (.r‘ndx) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐸‘𝑉) = (𝐸‘𝐹)) | ||
| Theorem | mnringnmulrdOLD 44229 | Obsolete version of mnringnmulrd 44228 as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ (.r‘ndx) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐸‘𝑉) = (𝐸‘𝐹)) | ||
| Theorem | mnringbased 44230 | The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐹)) | ||
| Theorem | mnringbasedOLD 44231 | Obsolete version of mnringnmulrd 44228 as of 1-Nov-2024. The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝐹)) | ||
| Theorem | mnringbaserd 44232 | The base set of a monoid ring. Converse of mnringbased 44230. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑉)) | ||
| Theorem | mnringelbased 44233 | Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝐶 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (𝐶 ↑m 𝐴) ∧ 𝑋 finSupp 0 ))) | ||
| Theorem | mnringbasefd 44234 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝐶 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐴⟶𝐶) | ||
| Theorem | mnringbasefsuppd 44235 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 finSupp 0 ) | ||
| Theorem | mnringaddgd 44236 | The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (+g‘𝑉) = (+g‘𝐹)) | ||
| Theorem | mnringaddgdOLD 44237 | Obsolete version of mnringaddgd 44236 as of 1-Nov-2024. The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (+g‘𝑉) = (+g‘𝐹)) | ||
| Theorem | mnring0gd 44238 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹)) | ||
| Theorem | mnring0g2d 44239 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹)) | ||
| Theorem | mnringmulrd 44240* | The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) = (.r‘𝐹)) | ||
| Theorem | mnringscad 44241 | The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) | ||
| Theorem | mnringscadOLD 44242 | Obsolete version of mnringscad 44241 as of 1-Nov-2024. The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) | ||
| Theorem | mnringvscad 44243 | The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ·𝑠 ‘𝑉) = ( ·𝑠 ‘𝐹)) | ||
| Theorem | mnringvscadOLD 44244 | Obsolete version of mnringvscad 44243 as of 1-Nov-2024. The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → ( ·𝑠 ‘𝑉) = ( ·𝑠 ‘𝐹)) | ||
| Theorem | mnringlmodd 44245 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐹 ∈ LMod) | ||
| Theorem | mnringmulrvald 44246* | Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ ∙ = (.r‘𝑅) & ⊢ 𝟎 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ · = (.r‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑋‘𝑎) ∙ (𝑌‘𝑏)), 𝟎 ))))) | ||
| Theorem | mnringmulrcld 44247 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ · = (.r‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
| Theorem | gru0eld 44248 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → ∅ ∈ 𝐺) | ||
| Theorem | grusucd 44249 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝐺) | ||
| Theorem | r1rankcld 44250 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅)) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅)) | ||
| Theorem | grur1cld 44251 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺) | ||
| Theorem | grurankcld 44252 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) | ||
| Theorem | grurankrcld 44253 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐺) | ||
| Syntax | cscott 44254 | Extend class notation with the Scott's trick operation. |
| class Scott 𝐴 | ||
| Definition | df-scott 44255* | Define the Scott operation. This operation constructs a subset of the input class which is nonempty whenever its input is using Scott's trick. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ Scott 𝐴 = {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} | ||
| Theorem | scotteqd 44256 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵) | ||
| Theorem | scotteq 44257 | Closed form of scotteqd 44256. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵) | ||
| Theorem | nfscott 44258 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Scott 𝐴 | ||
| Theorem | scottabf 44259* | Value of the Scott operation at a class abstraction. Variant of scottab 44260 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottab 44260* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottabes 44261* | Value of the Scott operation at a class abstraction. Variant of scottab 44260 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottss 44262 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Scott 𝐴 ⊆ 𝐴 | ||
| Theorem | elscottab 44263* | An element of the output of the Scott operation applied to a class abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑦 ∈ Scott {𝑥 ∣ 𝜑} → 𝜓) | ||
| Theorem | scottex2 44264 | scottex 9925 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ Scott 𝐴 ∈ V | ||
| Theorem | scotteld 44265* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴) | ||
| Theorem | scottelrankd 44266 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) & ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶)) | ||
| Theorem | scottrankd 44267 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵)) | ||
| Theorem | gruscottcld 44268 | If a Grothendieck universe contains an element of a Scott's trick set, it contains the Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐵 ∈ 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → Scott 𝐴 ∈ 𝐺) | ||
| Syntax | ccoll 44269 | Extend class notation with the collection operation. |
| class (𝐹 Coll 𝐴) | ||
| Definition | df-coll 44270* | Define the collection operation. This is similar to the image set operation “, but it uses Scott's trick to ensure the output is always a set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott (𝐹 “ {𝑥}) | ||
| Theorem | dfcoll2 44271* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦} | ||
| Theorem | colleq12d 44272 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵)) | ||
| Theorem | colleq1 44273 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴)) | ||
| Theorem | colleq2 44274 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵)) | ||
| Theorem | nfcoll 44275 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹 Coll 𝐴) | ||
| Theorem | collexd 44276 | The output of the collection operation is a set if the second input is. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) ∈ V) | ||
| Theorem | cpcolld 44277* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
| Theorem | cpcoll2d 44278* | cpcolld 44277 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
| Theorem | grucollcld 44279 | A Grothendieck universe contains the output of a collection operation whenever its left input is a relation on the universe, and its right input is in the universe. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐹 ⊆ (𝐺 × 𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) ∈ 𝐺) | ||
| Theorem | ismnu 44280* |
The hypothesis of this theorem defines a class M of sets that we
temporarily call "minimal universes", and which will turn out
in
grumnueq 44306 to be exactly Grothendicek universes.
Minimal universes are
sets which satisfy the predicate on 𝑦 in rr-groth 44318, except for the
𝑥
∈ 𝑦 clause.
A minimal universe is closed under subsets (mnussd 44282), powersets (mnupwd 44286), and an operation which is similar to a combination of collection and union (mnuop3d 44290), from which closure under pairing (mnuprd 44295), unions (mnuunid 44296), and function ranges (mnurnd 44302) can be deduced, from which equivalence with Grothendieck universes (grumnueq 44306) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) | ||
| Theorem | mnuop123d 44281* | Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
| Theorem | mnussd 44282* | Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
| Theorem | mnuss2d 44283* | mnussd 44282 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑈) | ||
| Theorem | mnu0eld 44284* | A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑈) | ||
| Theorem | mnuop23d 44285* | Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) | ||
| Theorem | mnupwd 44286* | Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) | ||
| Theorem | mnusnd 44287* | Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴} ∈ 𝑈) | ||
| Theorem | mnuprssd 44288* | A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuprss2d 44289* | Special case of mnuprssd 44288. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuop3d 44290* | Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) | ||
| Theorem | mnuprdlem1 44291* | Lemma for mnuprd 44295. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑤) | ||
| Theorem | mnuprdlem2 44292* | Lemma for mnuprd 44295. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑤) | ||
| Theorem | mnuprdlem3 44293* | Lemma for mnuprd 44295. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ Ⅎ𝑖𝜑 ⇒ ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) | ||
| Theorem | mnuprdlem4 44294* | Lemma for mnuprd 44295. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuprd 44295* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
| Theorem | mnuunid 44296* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
| Theorem | mnuund 44297* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
| Theorem | mnutrcld 44298* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
| Theorem | mnutrd 44299* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → Tr 𝑈) | ||
| Theorem | mnurndlem1 44300* | Lemma for mnurnd 44302. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |