Home | Metamath
Proof Explorer Theorem List (p. 407 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | amgm3d 40601 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
Theorem | amgm4d 40602 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
Theorem | spALT 40603 | sp 2182 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2182 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | elnelneqd 40604 | 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 40605 | 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 40606* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | rexlimdvaacbv 40607* | 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 | rexlimddvcbvw 40608* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 40607. The equivalent of this theorem without the bound variable change is rexlimddv 3291. Version of rexlimddvcbv 40609 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | rexlimddvcbv 40609* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 40607. The equivalent of this theorem without the bound variable change is rexlimddv 3291. Usage of this theorem is discouraged because it depends on ax-13 2390, see rexlimddvcbvw 40608 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | rr-elrnmpt3d 40610* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ ran 𝐹) | ||
Theorem | rr-phpd 40611 | Equivalent of php 8701 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ ω) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | suceqd 40612 | Deduction associated with suceq 6256. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → suc 𝐴 = suc 𝐵) | ||
Theorem | tfindsd 40613* | Deduction associated with tfinds 7574. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = suc 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑦 ∈ On ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝜃) → 𝜓) & ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | gru0eld 40614 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → ∅ ∈ 𝐺) | ||
Theorem | grusucd 40615 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → suc 𝐴 ∈ 𝐺) | ||
Theorem | r1rankcld 40616 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ (𝑅1‘𝑅)) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ (𝑅1‘𝑅)) | ||
Theorem | grur1cld 40617 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ∈ 𝐺) | ||
Theorem | grurankcld 40618 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → 𝐴 ∈ 𝐺) ⇒ ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) | ||
Theorem | grurankrcld 40619 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ (𝜑 → (rank‘𝐴) ∈ 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐺) | ||
Syntax | cscott 40620 | Extend class notation with the Scott's trick operation. |
class Scott 𝐴 | ||
Definition | df-scott 40621* | 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 40622 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Scott 𝐴 = Scott 𝐵) | ||
Theorem | scotteq 40623 | Closed form of scotteqd 40622. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ (𝐴 = 𝐵 → Scott 𝐴 = Scott 𝐵) | ||
Theorem | nfscott 40624 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Scott 𝐴 | ||
Theorem | scottabf 40625* | Value of the Scott operation at a class abstraction. Variant of scottab 40626 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
Theorem | scottab 40626* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
Theorem | scottabes 40627* | Value of the Scott operation at a class abstraction. Variant of scottab 40626 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → (rank‘𝑥) ⊆ (rank‘𝑦)))} | ||
Theorem | scottss 40628 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ Scott 𝐴 ⊆ 𝐴 | ||
Theorem | elscottab 40629* | 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 40630 | scottex 9314 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
⊢ Scott 𝐴 ∈ V | ||
Theorem | scotteld 40631* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ Scott 𝐴) | ||
Theorem | scottelrankd 40632 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) & ⊢ (𝜑 → 𝐶 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘𝐵) ⊆ (rank‘𝐶)) | ||
Theorem | scottrankd 40633 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ Scott 𝐴) ⇒ ⊢ (𝜑 → (rank‘Scott 𝐴) = suc (rank‘𝐵)) | ||
Theorem | gruscottcld 40634 | 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 40635 | Extend class notation with the collection operation. |
class (𝐹 Coll 𝐴) | ||
Definition | df-coll 40636* | 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 40637* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝐹 Coll 𝐴) = ∪ 𝑥 ∈ 𝐴 Scott {𝑦 ∣ 𝑥𝐹𝑦} | ||
Theorem | colleq12d 40638 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐵)) | ||
Theorem | colleq1 40639 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝐹 = 𝐺 → (𝐹 Coll 𝐴) = (𝐺 Coll 𝐴)) | ||
Theorem | colleq2 40640 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝐴 = 𝐵 → (𝐹 Coll 𝐴) = (𝐹 Coll 𝐵)) | ||
Theorem | nfcoll 40641 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹 Coll 𝐴) | ||
Theorem | collexd 40642 | 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 40643* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
Theorem | cpcoll2d 40644* | cpcolld 40643 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑥𝐹𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (𝐹 Coll 𝐴)𝑥𝐹𝑦) | ||
Theorem | grucollcld 40645 | 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 40646* |
The hypothesis of this theorem defines a class M of sets that we
temporarily call "minimal universes", and which will turn out
in
grumnueq 40672 to be exactly Grothendicek universes.
Minimal universes are
sets which satisfy the predicate on 𝑦 in rr-groth 40684, except for the
𝑥
∈ 𝑦 clause.
A minimal universe is closed under subsets (mnussd 40648), powersets (mnupwd 40652), and an operation which is similar to a combination of collection and union (mnuop3d 40656), from which closure under pairing (mnuprd 40661), unions (mnuunid 40662), and function ranges (mnurnd 40668) can be deduced, from which equivalence with Grothendieck universes (grumnueq 40672) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} ⇒ ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))) | ||
Theorem | mnuop123d 40647* | Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝒫 𝐴 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
Theorem | mnussd 40648* | Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | mnuss2d 40649* | mnussd 40648 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 𝐴 ⊆ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑈) | ||
Theorem | mnu0eld 40650* | A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑈) | ||
Theorem | mnuop23d 40651* | Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 (𝒫 𝐴 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹) → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) | ||
Theorem | mnupwd 40652* | Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) | ||
Theorem | mnusnd 40653* | Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴} ∈ 𝑈) | ||
Theorem | mnuprssd 40654* | A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuprss2d 40655* | Special case of mnuprssd 40654. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ 𝐴 ⊆ 𝐶 & ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuop3d 40656* | Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹 ⊆ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) | ||
Theorem | mnuprdlem1 40657* | Lemma for mnuprd 40661. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑤) | ||
Theorem | mnuprdlem2 40658* | Lemma for mnuprd 40661. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) & ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑤) | ||
Theorem | mnuprdlem3 40659* | Lemma for mnuprd 40661. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ Ⅎ𝑖𝜑 ⇒ ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣) | ||
Theorem | mnuprdlem4 40660* | Lemma for mnuprd 40661. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ¬ 𝐴 = ∅) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuprd 40661* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | mnuunid 40662* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈) | ||
Theorem | mnuund 40663* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
Theorem | mnutrcld 40664* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑈) | ||
Theorem | mnutrd 40665* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → Tr 𝑈) | ||
Theorem | mnurndlem1 40666* | Lemma for mnurnd 40668. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 (∃𝑣 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})𝑖 ∈ 𝑣 → ∃𝑢 ∈ ran (𝑎 ∈ 𝐴 ↦ {𝑎, {(𝐹‘𝑎), 𝐴}})(𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝑤) | ||
Theorem | mnurndlem2 40667* | Lemma for mnurnd 40668. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑈) & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝜑 → ran 𝐹 ∈ 𝑈) | ||
Theorem | mnurnd 40668* | 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 40669* | Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝑈 ∈ 𝑀) ⇒ ⊢ (𝜑 → 𝑈 ∈ Univ) | ||
Theorem | grumnudlem 40670* | Lemma for grumnud 40671. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝐺 ∈ Univ) & ⊢ 𝐹 = ({〈𝑏, 𝑐〉 ∣ ∃𝑑(∪ 𝑑 = 𝑐 ∧ 𝑑 ∈ 𝑓 ∧ 𝑏 ∈ 𝑑)} ∩ (𝐺 × 𝐺)) & ⊢ ((𝑖 ∈ 𝐺 ∧ ℎ ∈ 𝐺) → (𝑖𝐹ℎ ↔ ∃𝑗(∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗))) & ⊢ ((ℎ ∈ (𝐹 Coll 𝑧) ∧ (∪ 𝑗 = ℎ ∧ 𝑗 ∈ 𝑓 ∧ 𝑖 ∈ 𝑗)) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ∈ (𝐹 Coll 𝑧))) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
Theorem | grumnud 40671* | Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} & ⊢ (𝜑 → 𝐺 ∈ Univ) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
Theorem | grumnueq 40672* | The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ Univ = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))} | ||
Theorem | expandan 40673 | Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜃)) | ||
Theorem | expandexn 40674 | Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥𝜓) | ||
Theorem | expandral 40675 | Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | expandrexn 40676 | Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | ||
Theorem | expandrex 40677 | Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜓)) | ||
Theorem | expanduniss 40678* | Expand ∪ 𝐴 ⊆ 𝐵 to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) | ||
Theorem | ismnuprim 40679* | Express the predicate on 𝑈 in ismnu 40646 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ↔ ∀𝑧(𝑧 ∈ 𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑈 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))) | ||
Theorem | rr-grothprimbi 40680* | Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim 40685. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥 ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))) | ||
Theorem | inagrud 40681 | Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝜑 → 𝐼 ∈ Inacc) ⇒ ⊢ (𝜑 → (𝑅1‘𝐼) ∈ Univ) | ||
Theorem | inaex 40682* | Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ (𝐴 ∈ On → ∃𝑥 ∈ Inacc 𝐴 ∈ 𝑥) | ||
Theorem | gruex 40683* | Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 | ||
Theorem | rr-groth 40684* | An equivalent of ax-groth 10245 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑓∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑦 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) | ||
Theorem | rr-grothprim 40685* | An equivalent of ax-groth 10245 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10256 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.) |
⊢ ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))) | ||
Theorem | nanorxor 40686 | 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓))) | ||
Theorem | undisjrab 40687 | Union of two disjoint restricted class abstractions; compare unrab 4274. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)}) | ||
Theorem | iso0 40688 | The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅) | ||
Theorem | ssrecnpr 40689 | ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆) | ||
Theorem | seff 40690 | Let set 𝑆 be the real or complex numbers. Then the exponential function restricted to 𝑆 is a mapping from 𝑆 to 𝑆. (Contributed by Steve Rodriguez, 6-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) ⇒ ⊢ (𝜑 → (exp ↾ 𝑆):𝑆⟶𝑆) | ||
Theorem | sblpnf 40691 | The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 23007. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) | ||
Theorem | prmunb2 40692* | The primes are unbounded. This generalizes prmunb 16250 to real 𝐴 with arch 11895 and lttrd 10801: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝) | ||
Theorem | dvgrat 40693* | Ratio test for divergence of a complex infinite series. See e.g. remark "if (abs‘((𝑎‘(𝑛 + 1)) / (𝑎‘𝑛))) ≥ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∉ dom ⇝ ) | ||
Theorem | cvgdvgrat 40694* |
Ratio test for convergence and divergence of a complex infinite series.
If the ratio 𝑅 of the absolute values of successive
terms in an
infinite sequence 𝐹 converges to less than one, then the
infinite
sum of the terms of 𝐹 converges to a complex number; and
if 𝑅
converges greater then the sum diverges. This combined form of
cvgrat 15239 and dvgrat 40693 directly uses the limit of the ratio.
(It also demonstrates how to use climi2 14868 and absltd 14789 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 14789, and how to use r19.29a 3289 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3284 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3284.) (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑅 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 1) ⇒ ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) | ||
Theorem | radcnvrat 40695* | Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 40694) as 𝑘 increases. Then the radius of convergence of power series Σ𝑛 ∈ ℕ0((𝐴‘𝑛) · (𝑥↑𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence 40694 —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0) & ⊢ (𝜑 → 𝐷 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 0) ⇒ ⊢ (𝜑 → 𝑅 = (1 / 𝐿)) | ||
Theorem | reldvds 40696 | The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ Rel ∥ | ||
Theorem | nznngen 40697 | All positive integers in the set of multiples of n, nℤ, are the absolute value of n or greater. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑁}) ∩ ℕ) ⊆ (ℤ≥‘(abs‘𝑁))) | ||
Theorem | nzss 40698 | The set of multiples of m, mℤ, is a subset of those of n, nℤ, iff n divides m. Lemma 2.1(a) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ⊆ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ 𝑀)) | ||
Theorem | nzin 40699 | The intersection of the set of multiples of m, mℤ, and those of n, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) = ( ∥ “ {(𝑀 lcm 𝑁)})) | ||
Theorem | nzprmdif 40700 | Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℙ) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |