Home | Metamath
Proof Explorer Theorem List (p. 405 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | suprlubrd 40401* | Natural deduction form of specialized suprlub 11594. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝐵 < 𝑧) ⇒ ⊢ (𝜑 → 𝐵 < sup(𝐴, ℝ, < )) | ||
Theorem | imo72b2lem1 40402* | Lemma for imo72b2 40406. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ (𝐹‘𝑥) ≠ 0) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ (abs‘(𝐹‘𝑦)) ≤ 1) ⇒ ⊢ (𝜑 → 0 < sup((abs “ (𝐹 “ ℝ)), ℝ, < )) | ||
Theorem | lemuldiv3d 40403 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) | ||
Theorem | lemuldiv4d 40404 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐵 ≤ (𝐶 / 𝐴)) & ⊢ (𝜑 → 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐵 · 𝐴) ≤ 𝐶) | ||
Theorem | rspcdvinvd 40405* | If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | imo72b2 40406* | IMO 1972 B2. (14th International Mathemahics 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 10633 1red 10631 readdcld 10659 remulcld 10660 eqcomd 2827. | ||
Theorem | int-addcomd 40407 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = (𝐶 + 𝐴)) | ||
Theorem | int-addassocd 40408 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + 𝐷)) | ||
Theorem | int-addsimpd 40409 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 = (𝐴 − 𝐵)) | ||
Theorem | int-mulcomd 40410 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴)) | ||
Theorem | int-mulassocd 40411 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷)) | ||
Theorem | int-mulsimpd 40412 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → 1 = (𝐴 / 𝐵)) | ||
Theorem | int-leftdistd 40413 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴))) | ||
Theorem | int-rightdistd 40414 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷))) | ||
Theorem | int-sqdefd 40415 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2)) | ||
Theorem | int-mul11d 40416 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐵) | ||
Theorem | int-mul12d 40417 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐵) | ||
Theorem | int-add01d 40418 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐵) | ||
Theorem | int-add02d 40419 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐵) | ||
Theorem | int-sqgeq0d 40420 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | int-eqprincd 40421 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷)) | ||
Theorem | int-eqtransd 40422 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | int-eqmvtd 40423 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷)) | ||
Theorem | int-eqineqd 40424 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
Theorem | int-ineqmvtd 40425 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶) | ||
Theorem | int-ineq1stprincd 40426 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶)) | ||
Theorem | int-ineq2ndprincd 40427 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶)) | ||
Theorem | int-ineqtransd 40428 | 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 12102 addcomli 10821 00id 10804 addid1i 10816 addid2i 10817 eqid 2821 dec0h 12109 decadd 12141 decaddc 12142. | ||
Theorem | unitadd 40429 | Theorem used in conjunction with decaddc 12142 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝐴 + 𝐵) = 𝐹 & ⊢ (𝐶 + 1) = 𝐵 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐶) + 1) = 𝐹 | ||
Theorem | gsumws3 40430 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg 〈“𝑆𝑇𝑈”〉) = (𝑆 + (𝑇 + 𝑈))) | ||
Theorem | gsumws4 40431 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg 〈“𝑆𝑇𝑈𝑉”〉) = (𝑆 + (𝑇 + (𝑈 + 𝑉)))) | ||
Theorem | amgm2d 40432 | Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 25495. (Contributed by Stanislas Polu, 8-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2)) | ||
Theorem | amgm3d 40433 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
Theorem | amgm4d 40434 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
Theorem | spALT 40435 | sp 2172 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2172 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | elnelneqd 40436 | 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 40437 | 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 40438* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | rexlimdvaacbv 40439* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3285. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜃)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimddvcbv 40440* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 40439. The equivalent of this theorem without the bound variable change is rexlimddv 3291. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | rr-elrnmpt3d 40441* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
Theorem | rr-phpd 40442 | Equivalent of php 8690 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ω) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | suceqd 40443 | Deduction associated with suceq 6250. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → suc 𝐴 = suc 𝐵) | ||
Theorem | tfindsd 40444* | Deduction associated with tfinds 7562. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | gru0eld 40445 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → ∅ ∈ 𝐺) | ||
Theorem | grusucd 40446 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝐺) | ||
Theorem | r1rankcld 40447 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅)) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅)) | ||
Theorem | grur1cld 40448 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺) | ||
Theorem | grurankcld 40449 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) | ||
Theorem | grurankrcld 40450 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐺) | ||
Syntax | cscott 40451 | Extend class notation with the Scott's trick operation. |
class Scott 𝐴 | ||
Definition | df-scott 40452* | 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 40453 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵) | ||
Theorem | scotteq 40454 | Closed form of scotteqd 40453. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵) | ||
Theorem | nfscott 40455 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Scott 𝐴 | ||
Theorem | scottabf 40456* | Value of the Scott operation at a class abstraction. Variant of scottab 40457 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
Theorem | scottab 40457* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
Theorem | scottabes 40458* | Value of the Scott operation at a class abstraction. Variant of scottab 40457 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
Theorem | scottss 40459 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ Scott 𝐴 ⊆ 𝐴 | ||
Theorem | elscottab 40460* | 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 40461 | scottex 9303 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ Scott 𝐴 ∈ V | ||
Theorem | scotteld 40462* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴) | ||
Theorem | scottelrankd 40463 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) & ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶)) | ||
Theorem | scottrankd 40464 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵)) | ||
Theorem | gruscottcld 40465 | 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 40466 | Extend class notation with the collection operation. |
class (𝐹 Coll 𝐴) | ||
Definition | df-coll 40467* | 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 40468* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦} | ||
Theorem | colleq12d 40469 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵)) | ||
Theorem | colleq1 40470 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴)) | ||
Theorem | colleq2 40471 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵)) | ||
Theorem | nfcoll 40472 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹 Coll 𝐴) | ||
Theorem | collexd 40473 | 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 40474* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
Theorem | cpcoll2d 40475* | cpcolld 40474 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
Theorem | grucollcld 40476 | 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 40477* |
The hypothesis of this theorem defines a class M of sets that we
temporarily call "minimal universes", and which will turn out
in
grumnueq 40503 to be exactly Grothendicek universes.
Minimal universes are
sets which satisfy the predicate on 𝑦 in rr-groth 40515, except for the
𝑥
∈ 𝑦 clause.
A minimal universe is closed under subsets (mnussd 40479), powersets (mnupwd 40483), and an operation which is similar to a combination of collection and union (mnuop3d 40487), from which closure under pairing (mnuprd 40492), unions (mnuunid 40493), and function ranges (mnurnd 40499) can be deduced, from which equivalence with Grothendieck universes (grumnueq 40503) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) | ||
Theorem | mnuop123d 40478* | Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
Theorem | mnussd 40479* | Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | mnuss2d 40480* | mnussd 40479 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑈) | ||
Theorem | mnu0eld 40481* | A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑈) | ||
Theorem | mnuop23d 40482* | Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) | ||
Theorem | mnupwd 40483* | Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) | ||
Theorem | mnusnd 40484* | Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴} ∈ 𝑈) | ||
Theorem | mnuprssd 40485* | A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuprss2d 40486* | Special case of mnuprssd 40485. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuop3d 40487* | Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) | ||
Theorem | mnuprdlem1 40488* | Lemma for mnuprd 40492. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑤) | ||
Theorem | mnuprdlem2 40489* | Lemma for mnuprd 40492. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑤) | ||
Theorem | mnuprdlem3 40490* | Lemma for mnuprd 40492. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ Ⅎ𝑖𝜑 ⇒ ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) | ||
Theorem | mnuprdlem4 40491* | Lemma for mnuprd 40492. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuprd 40492* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuunid 40493* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
Theorem | mnuund 40494* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
Theorem | mnutrcld 40495* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | mnutrd 40496* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → Tr 𝑈) | ||
Theorem | mnurndlem1 40497* | Lemma for mnurnd 40499. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤) | ||
Theorem | mnurndlem2 40498* | Lemma for mnurnd 40499. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝜑 → ran 𝐹 ∈ 𝑈) | ||
Theorem | mnurnd 40499* | Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ 𝑈) | ||
Theorem | mnugrud 40500* | Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → 𝑈 ∈ Univ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |