HomeTheorem List (p. 447 of 503)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 447 of 503) | < 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: | Metamath Proof Explorer
(1-31009) |
Hilbert Space Explorer
(31010-32532) |
Users' Mathboxes
(32533-50277) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | absmulrposd 44601 | Specialization of absmuld with absidd 15374. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = (𝐴 · (abs‘𝐵))) | ||
| Theorem | imadisjld 44602 | Natural dduction form of one side of imadisj 6037. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → (dom 𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐵) = ∅) | ||
| Theorem | wnefimgd 44603 | The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ≠ ∅) | ||
| Theorem | fco2d 44604 | Natural deduction form of fco2 6686. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
| Theorem | wfximgfd 44605 | The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ 𝐴)) | ||
| Theorem | extoimad 44606* | If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 𝐶) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (abs “ (𝐹 “ ℝ))𝑥 ≤ 𝐶) | ||
| Theorem | imo72b2lem0 44607* | Lemma for imo72b2 44614. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘(𝐴 + 𝐵)) + (𝐹‘(𝐴 − 𝐵))) = (2 · ((𝐹‘𝐴) · (𝐺‘𝐵)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → ((abs‘(𝐹‘𝐴)) · (abs‘(𝐺‘𝐵))) ≤ sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
| Theorem | suprleubrd 44608* | Natural deduction form of specialized suprleub 12111. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐵) | ||
| Theorem | imo72b2lem2 44609* | Lemma for imo72b2 44614. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → ∀𝑧 ∈ ℝ (abs‘(𝐹‘𝑧)) ≤ 𝐶) ⇒ ⊢ (𝜑 → sup((abs “ (𝐹 “ ℝ)), ℝ, < ) ≤ 𝐶) | ||
| Theorem | suprlubrd 44610* | Natural deduction form of specialized suprlub 12109. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧) ⇒ ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < )) | ||
| Theorem | imo72b2lem1 44611* | Lemma for imo72b2 44614. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
| Theorem | lemuldiv3d 44612 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) | ||
| Theorem | lemuldiv4d 44613 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) | ||
| Theorem | imo72b2 44614* | IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.) |
| ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐺:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ ℝ ∀𝑣 ∈ ℝ ((𝐹‘(𝑢 + 𝑣)) + (𝐹‘(𝑢 − 𝑣))) = (2 · ((𝐹‘𝑢) · (𝐺‘𝑣)))) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) ⇒ ⊢ (𝜑 → (abs‘(𝐺‘𝐵)) ≤ 1) | ||
This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 11136 1red 11134 readdcld 11163 remulcld 11164 eqcomd 2743. | ||
| Theorem | int-addcomd 44615 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴)) | ||
| Theorem | int-addassocd 44616 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷)) | ||
| Theorem | int-addsimpd 44617 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 = (𝐴 − 𝐵)) | ||
| Theorem | int-mulcomd 44618 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴)) | ||
| Theorem | int-mulassocd 44619 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷)) | ||
| Theorem | int-mulsimpd 44620 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → 1 = (𝐴 / 𝐵)) | ||
| Theorem | int-leftdistd 44621 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴))) | ||
| Theorem | int-rightdistd 44622 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷))) | ||
| Theorem | int-sqdefd 44623 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2)) | ||
| Theorem | int-mul11d 44624 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐵) | ||
| Theorem | int-mul12d 44625 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐵) | ||
| Theorem | int-add01d 44626 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐵) | ||
| Theorem | int-add02d 44627 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐵) | ||
| Theorem | int-sqgeq0d 44628 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) | ||
| Theorem | int-eqprincd 44629 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷)) | ||
| Theorem | int-eqtransd 44630 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
| Theorem | int-eqmvtd 44631 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷)) | ||
| Theorem | int-eqineqd 44632 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
| Theorem | int-ineqmvtd 44633 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶) | ||
| Theorem | int-ineq1stprincd 44634 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶)) | ||
| Theorem | int-ineq2ndprincd 44635 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶)) | ||
| Theorem | int-ineqtransd 44636 | 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 12648 addcomli 11327 00id 11310 addridi 11322 addlidi 11323 eqid 2737 dec0h 12655 decadd 12687 decaddc 12688. | ||
| Theorem | unitadd 44637 | Theorem used in conjunction with decaddc 12688 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
| ⊢ (𝐴 + 𝐵) = 𝐹 & ⊢ (𝐶 + 1) = 𝐵 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐶) + 1) = 𝐹 | ||
| Theorem | gsumws3 44638 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg ⟨“𝑆𝑇𝑈”⟩) = (𝑆 + (𝑇 + 𝑈))) | ||
| Theorem | gsumws4 44639 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg ⟨“𝑆𝑇𝑈𝑉”⟩) = (𝑆 + (𝑇 + (𝑈 + 𝑉)))) | ||
| Theorem | amgm2d 44640 | Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 26971. (Contributed by Stanislas Polu, 8-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2)) | ||
| Theorem | amgm3d 44641 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
| Theorem | amgm4d 44642 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
| Theorem | spALT 44643 | sp 2191 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2191 instead. (New usage is discouraged.) |
| ⊢ (∀𝑥𝜑 → 𝜑) | ||
| Theorem | elnelneqd 44644 | 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 44645 | 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 44646* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
| Theorem | rexlimdvaacbv 44647* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3140. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
| Theorem | rexlimddvcbvw 44648* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44647. The equivalent of this theorem without the bound variable change is rexlimddv 3145. Version of rexlimddvcbv 44649 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 44649* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44647. The equivalent of this theorem without the bound variable change is rexlimddv 3145. Usage of this theorem is discouraged because it depends on ax-13 2377, see rexlimddvcbvw 44648 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
| ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | rr-elrnmpt3d 44650* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
| Theorem | rr-phpd 44651 | Equivalent of php 9132 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ω) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | tfindsd 44652* | Deduction associated with tfinds 7802. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → 𝜂) | ||
| Syntax | cmnring 44653 | Extend class notation with the monoid ring function. |
| class MndRing | ||
| Definition | df-mnring 44654* | 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 44655* | 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 44656 | 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 | mnringbased 44657 | 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 | mnringbaserd 44658 | The base set of a monoid ring. Converse of mnringbased 44657. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐵 = (Base‘𝑉)) | ||
| Theorem | mnringelbased 44659 | 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 44660 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝐶 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋:𝐴⟶𝐶) | ||
| Theorem | mnringbasefsuppd 44661 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 finSupp 0 ) | ||
| Theorem | mnringaddgd 44662 | 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 | mnring0gd 44663 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ 𝑉 = (𝑅 freeLMod 𝐴) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (0g‘𝑉) = (0g‘𝐹)) | ||
| Theorem | mnring0g2d 44664 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × { 0 }) = (0g‘𝐹)) | ||
| Theorem | mnringmulrd 44665* | 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 44666 | The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑅 = (Scalar‘𝐹)) | ||
| Theorem | mnringvscad 44667 | 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 | mnringlmodd 44668 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐹 ∈ LMod) | ||
| Theorem | mnringmulrvald 44669* | 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 44670 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
| ⊢ 𝐹 = (𝑅 MndRing 𝑀) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ 𝐴 = (Base‘𝑀) & ⊢ · = (.r‘𝐹) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐵) | ||
| Theorem | gru0eld 44671 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → ∅ ∈ 𝐺) | ||
| Theorem | grusucd 44672 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝐺) | ||
| Theorem | r1rankcld 44673 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅)) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅)) | ||
| Theorem | grur1cld 44674 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺) | ||
| Theorem | grurankcld 44675 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) | ||
| Theorem | grurankrcld 44676 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐺) | ||
| Syntax | cscott 44677 | Extend class notation with the Scott's trick operation. |
| class Scott 𝐴 | ||
| Definition | df-scott 44678* | 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 44679 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵) | ||
| Theorem | scotteq 44680 | Closed form of scotteqd 44679. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵) | ||
| Theorem | nfscott 44681 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Scott 𝐴 | ||
| Theorem | scottabf 44682* | Value of the Scott operation at a class abstraction. Variant of scottab 44683 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottab 44683* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottabes 44684* | Value of the Scott operation at a class abstraction. Variant of scottab 44683 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
| ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
| Theorem | scottss 44685 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Scott 𝐴 ⊆ 𝐴 | ||
| Theorem | elscottab 44686* | 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 44687 | scottex 9798 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
| ⊢ Scott 𝐴 ∈ V | ||
| Theorem | scotteld 44688* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴) | ||
| Theorem | scottelrankd 44689 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) & ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶)) | ||
| Theorem | scottrankd 44690 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵)) | ||
| Theorem | gruscottcld 44691 | 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 44692 | Extend class notation with the collection operation. |
| class (𝐹 Coll 𝐴) | ||
| Definition | df-coll 44693* | 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 44694* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦} | ||
| Theorem | colleq12d 44695 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵)) | ||
| Theorem | colleq1 44696 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴)) | ||
| Theorem | colleq2 44697 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵)) | ||
| Theorem | nfcoll 44698 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹 Coll 𝐴) | ||
| Theorem | collexd 44699 | 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 44700* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
| ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |