![]() |
Metamath
Proof Explorer Theorem List (p. 437 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | scottab 43601* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottabes 43602* | Value of the Scott operation at a class abstraction. Variant of scottab 43601 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottss 43603 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ Scott π΄ β π΄ | ||
Theorem | elscottab 43604* | 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 43605 | scottex 9900 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ Scott π΄ β V | ||
Theorem | scotteld 43606* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β βπ₯ π₯ β π΄) β β’ (π β βπ₯ π₯ β Scott π΄) | ||
Theorem | scottelrankd 43607 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) & β’ (π β πΆ β Scott π΄) β β’ (π β (rankβπ΅) β (rankβπΆ)) | ||
Theorem | scottrankd 43608 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) β β’ (π β (rankβScott π΄) = suc (rankβπ΅)) | ||
Theorem | gruscottcld 43609 | 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 43610 | Extend class notation with the collection operation. |
class (πΉ Coll π΄) | ||
Definition | df-coll 43611* | 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 43612* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ Coll π΄) = βͺ π₯ β π΄ Scott {π¦ β£ π₯πΉπ¦} | ||
Theorem | colleq12d 43613 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΉ = πΊ) & β’ (π β π΄ = π΅) β β’ (π β (πΉ Coll π΄) = (πΊ Coll π΅)) | ||
Theorem | colleq1 43614 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ = πΊ β (πΉ Coll π΄) = (πΊ Coll π΄)) | ||
Theorem | colleq2 43615 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π΄ = π΅ β (πΉ Coll π΄) = (πΉ Coll π΅)) | ||
Theorem | nfcoll 43616 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ β²π₯πΉ & β’ β²π₯π΄ β β’ β²π₯(πΉ Coll π΄) | ||
Theorem | collexd 43617 | 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 43618* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π₯ β π΄) & β’ (π β π₯πΉπ¦) β β’ (π β βπ¦ β (πΉ Coll π΄)π₯πΉπ¦) | ||
Theorem | cpcoll2d 43619* | cpcolld 43618 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ (π β π₯ β π΄) & β’ (π β βπ¦ π₯πΉπ¦) β β’ (π β βπ¦ β (πΉ Coll π΄)π₯πΉπ¦) | ||
Theorem | grucollcld 43620 | 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 43621* |
The hypothesis of this theorem defines a class M of sets that we
temporarily call "minimal universes", and which will turn out
in
grumnueq 43647 to be exactly Grothendicek universes.
Minimal universes are
sets which satisfy the predicate on π¦ in rr-groth 43659, except for the
π₯
β π¦ clause.
A minimal universe is closed under subsets (mnussd 43623), powersets (mnupwd 43627), and an operation which is similar to a combination of collection and union (mnuop3d 43631), from which closure under pairing (mnuprd 43636), unions (mnuunid 43637), and function ranges (mnurnd 43643) can be deduced, from which equivalence with Grothendieck universes (grumnueq 43647) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} β β’ (π β π β (π β π β βπ§ β π (π« π§ β π β§ βπβπ€ β π (π« π§ β π€ β§ βπ β π§ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))))) | ||
Theorem | mnuop123d 43622* | Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β (π« π΄ β π β§ βπβπ€ β π (π« π΄ β π€ β§ βπ β π΄ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) | ||
Theorem | mnussd 43623* | Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | mnuss2d 43624* | mnussd 43623 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β βπ₯ β π π΄ β π₯) β β’ (π β π΄ β π) | ||
Theorem | mnu0eld 43625* | A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β β β π) | ||
Theorem | mnuop23d 43626* | Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β πΉ β π) β β’ (π β βπ€ β π (π« π΄ β π€ β§ βπ β π΄ (βπ£ β π (π β π£ β§ π£ β πΉ) β βπ’ β πΉ (π β π’ β§ βͺ π’ β π€)))) | ||
Theorem | mnupwd 43627* | Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β π« π΄ β π) | ||
Theorem | mnusnd 43628* | Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β {π΄} β π) | ||
Theorem | mnuprssd 43629* | A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β πΆ β π) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuprss2d 43630* | Special case of mnuprssd 43629. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β πΆ β π) & β’ π΄ β πΆ & β’ π΅ β πΆ β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuop3d 43631* | Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β πΉ β π) β β’ (π β βπ€ β π βπ β π΄ (βπ£ β πΉ π β π£ β βπ’ β πΉ (π β π’ β§ βͺ π’ β π€))) | ||
Theorem | mnuprdlem1 43632* | Lemma for mnuprd 43636. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β βπ β {β , {β }}βπ’ β πΉ (π β π’ β§ βͺ π’ β π€)) β β’ (π β π΄ β π€) | ||
Theorem | mnuprdlem2 43633* | Lemma for mnuprd 43636. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ (π β π΅ β π) & β’ (π β Β¬ π΄ = β ) & β’ (π β βπ β {β , {β }}βπ’ β πΉ (π β π’ β§ βͺ π’ β π€)) β β’ (π β π΅ β π€) | ||
Theorem | mnuprdlem3 43634* | Lemma for mnuprd 43636. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ β²ππ β β’ (π β βπ β {β , {β }}βπ£ β πΉ π β π£) | ||
Theorem | mnuprdlem4 43635* | Lemma for mnuprd 43636. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β Β¬ π΄ = β ) β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuprd 43636* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuunid 43637* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β βͺ π΄ β π) | ||
Theorem | mnuund 43638* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | mnutrcld 43639* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | mnutrd 43640* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) β β’ (π β Tr π) | ||
Theorem | mnurndlem1 43641* | Lemma for mnurnd 43643. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ (π β πΉ:π΄βΆπ) & β’ π΄ β V & β’ (π β βπ β π΄ (βπ£ β ran (π β π΄ β¦ {π, {(πΉβπ), π΄}})π β π£ β βπ’ β ran (π β π΄ β¦ {π, {(πΉβπ), π΄}})(π β π’ β§ βͺ π’ β π€))) β β’ (π β ran πΉ β π€) | ||
Theorem | mnurndlem2 43642* | Lemma for mnurnd 43643. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ) & β’ π΄ β V β β’ (π β ran πΉ β π) | ||
Theorem | mnurnd 43643* | 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 43644* | Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) β β’ (π β π β Univ) | ||
Theorem | grumnudlem 43645* | Lemma for grumnud 43646. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β πΊ β Univ) & β’ πΉ = ({β¨π, πβ© β£ βπ(βͺ π = π β§ π β π β§ π β π)} β© (πΊ Γ πΊ)) & β’ ((π β πΊ β§ β β πΊ) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) & β’ ((β β (πΉ Coll π§) β§ (βͺ π = β β§ π β π β§ π β π)) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) β β’ (π β πΊ β π) | ||
Theorem | grumnud 43646* | Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β πΊ β Univ) β β’ (π β πΊ β π) | ||
Theorem | grumnueq 43647* | The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ Univ = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} | ||
Theorem | expandan 43648 | Expand conjunction to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β π) & β’ (π β π) β β’ ((π β§ π) β Β¬ (π β Β¬ π)) | ||
Theorem | expandexn 43649 | Expand an existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β Β¬ π) β β’ (βπ₯π β Β¬ βπ₯π) | ||
Theorem | expandral 43650 | Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β π) β β’ (βπ₯ β π΄ π β βπ₯(π₯ β π΄ β π)) | ||
Theorem | expandrexn 43651 | Expand a restricted existential quantifier to primitives while contracting a double negation. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β Β¬ π) β β’ (βπ₯ β π΄ π β Β¬ βπ₯(π₯ β π΄ β π)) | ||
Theorem | expandrex 43652 | Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β π) β β’ (βπ₯ β π΄ π β Β¬ βπ₯(π₯ β π΄ β Β¬ π)) | ||
Theorem | expanduniss 43653* | Expand βͺ π΄ β π΅ to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (βͺ π΄ β π΅ β βπ₯(π₯ β π΄ β βπ¦(π¦ β π₯ β π¦ β π΅))) | ||
Theorem | ismnuprim 43654* | Express the predicate on π in ismnu 43621 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (βπ§ β π (π« π§ β π β§ βπβπ€ β π (π« π§ β π€ β§ βπ β π§ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))) β βπ§(π§ β π β βπ Β¬ βπ€(π€ β π β Β¬ βπ£ Β¬ ((βπ‘(π‘ β π£ β π‘ β π§) β Β¬ (π£ β π β Β¬ π£ β π€)) β Β¬ βπ(π β π§ β (π£ β π β (π β π£ β (π£ β π β Β¬ βπ’(π’ β π β (π β π’ β Β¬ βπ(π β π’ β βπ (π β π β π β π€)))))))))))) | ||
Theorem | rr-grothprimbi 43655* | 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 43660. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (βπ₯βπ¦ β Univ π₯ β π¦ β βπ₯ Β¬ βπ¦(π₯ β π¦ β Β¬ βπ§(π§ β π¦ β βπ Β¬ βπ€(π€ β π¦ β Β¬ βπ£ Β¬ ((βπ‘(π‘ β π£ β π‘ β π§) β Β¬ (π£ β π¦ β Β¬ π£ β π€)) β Β¬ βπ(π β π§ β (π£ β π¦ β (π β π£ β (π£ β π β Β¬ βπ’(π’ β π β (π β π’ β Β¬ βπ(π β π’ β βπ (π β π β π β π€))))))))))))) | ||
Theorem | inagrud 43656 | Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π β πΌ β Inacc) β β’ (π β (π 1βπΌ) β Univ) | ||
Theorem | inaex 43657* | Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ (π΄ β On β βπ₯ β Inacc π΄ β π₯) | ||
Theorem | gruex 43658* | Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ βπ¦ β Univ π₯ β π¦ | ||
Theorem | rr-groth 43659* | An equivalent of ax-groth 10838 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ βπ¦(π₯ β π¦ β§ βπ§ β π¦ (π« π§ β π¦ β§ βπβπ€ β π¦ (π« π§ β π€ β§ βπ β π§ (βπ£ β π¦ (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) | ||
Theorem | rr-grothprim 43660* | An equivalent of ax-groth 10838 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10849 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ Β¬ βπ¦(π₯ β π¦ β Β¬ βπ§(π§ β π¦ β βπ Β¬ βπ€(π€ β π¦ β Β¬ βπ£ Β¬ ((βπ‘(π‘ β π£ β π‘ β π§) β Β¬ (π£ β π¦ β Β¬ π£ β π€)) β Β¬ βπ(π β π§ β (π£ β π¦ β (π β π£ β (π£ β π β Β¬ βπ’(π’ β π β (π β π’ β Β¬ βπ(π β π’ β βπ (π β π β π β π€)))))))))))) | ||
Theorem | ismnushort 43661* | Express the predicate on π and π§ in ismnu 43621 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.) |
β’ (βπ β π« πβπ€ β π (π« π§ β (π β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€)) β (π« π§ β π β§ βπβπ€ β π (π« π§ β π€ β§ βπ β π§ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) | ||
Theorem | dfuniv2 43662* | Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024.) |
β’ Univ = {π¦ β£ βπ§ β π¦ βπ β π« π¦βπ€ β π¦ (π« π§ β (π¦ β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€))} | ||
Theorem | rr-grothshortbi 43663* | Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024.) |
β’ (βπ₯βπ¦ β Univ π₯ β π¦ β βπ₯βπ¦(π₯ β π¦ β§ βπ§ β π¦ βπ β π« π¦βπ€ β π¦ (π« π§ β (π¦ β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€)))) | ||
Theorem | rr-grothshort 43664* | A shorter equivalent of ax-groth 10838 than rr-groth 43659 using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024.) |
β’ βπ¦(π₯ β π¦ β§ βπ§ β π¦ βπ β π« π¦βπ€ β π¦ (π« π§ β (π¦ β© π€) β§ (π§ β© βͺ π) β βͺ (π β© π« π« π€))) | ||
Theorem | nanorxor 43665 | 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ ((π βΌ π) β ((π β¨ π) β (π β» π))) | ||
Theorem | undisjrab 43666 | Union of two disjoint restricted class abstractions; compare unrab 4301. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ (({π₯ β π΄ β£ π} β© {π₯ β π΄ β£ π}) = β β ({π₯ β π΄ β£ π} βͺ {π₯ β π΄ β£ π}) = {π₯ β π΄ β£ (π β» π)}) | ||
Theorem | iso0 43667 | The empty set is an π , π isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
β’ β Isom π , π (β , β ) | ||
Theorem | ssrecnpr 43668 | β is a subset of both β and β. (Contributed by Steve Rodriguez, 22-Nov-2015.) |
β’ (π β {β, β} β β β π) | ||
Theorem | seff 43669 | 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 43670 | The infinity ball in the absolute value metric is just the whole space. π analogue of blpnf 24290. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
β’ (π β π β {β, β}) & β’ π· = ((abs β β ) βΎ (π Γ π)) β β’ ((π β§ π β π) β (π(ballβπ·)+β) = π) | ||
Theorem | prmunb2 43671* | The primes are unbounded. This generalizes prmunb 16874 to real π΄ with arch 12491 and lttrd 11397: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π΄ β β β βπ β β π΄ < π) | ||
Theorem | dvgrat 43672* | 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 43673* |
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 15853 and dvgrat 43672 directly uses the limit of the ratio.
(It also demonstrates how to use climi2 15479 and absltd 15400 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15400, and how to use r19.29a 3157 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3150 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3150.) (Contributed by Steve Rodriguez, 28-Feb-2020.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β 0) & β’ π = (π β π β¦ (absβ((πΉβ(π + 1)) / (πΉβπ)))) & β’ (π β π β πΏ) & β’ (π β πΏ β 1) β β’ (π β (πΏ < 1 β seqπ( + , πΉ) β dom β )) | ||
Theorem | radcnvrat 43674* | Let πΏ be the limit, if one exists, of the ratio (absβ((π΄β(π + 1)) / (π΄βπ))) (as in the ratio test cvgdvgrat 43673) 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 43673 β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 43675 | The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ Rel β₯ | ||
Theorem | nznngen 43676 | 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 43677 | 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 43678 | 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 43679 | Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β π) β β’ (π β (( β₯ β {π}) β ( β₯ β {π})) = (( β₯ β {π}) β ( β₯ β {(π Β· π)}))) | ||
Theorem | hashnzfz 43680 | Special case of hashdvds 16735: the count of multiples in nβ€ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β β) & β’ (π β π½ β β€) & β’ (π β πΎ β (β€β₯β(π½ β 1))) β β’ (π β (β―β(( β₯ β {π}) β© (π½...πΎ))) = ((ββ(πΎ / π)) β (ββ((π½ β 1) / π)))) | ||
Theorem | hashnzfz2 43681 | Special case of hashnzfz 43680: the count of multiples in nβ€, n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β (β€β₯β2)) & β’ (π β πΎ β β) β β’ (π β (β―β(( β₯ β {π}) β© (2...πΎ))) = (ββ(πΎ / π))) | ||
Theorem | hashnzfzclim 43682* | As the upper bound πΎ of the constraint interval (π½...πΎ) in hashnzfz 43680 increases, the resulting count of multiples tends to (πΎ / π) βthat is, there are approximately (πΎ / π) multiples of π in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β π β β) & β’ (π β π½ β β€) β β’ (π β (π β (β€β₯β(π½ β 1)) β¦ ((β―β(( β₯ β {π}) β© (π½...π))) / π)) β (1 / π)) | ||
Theorem | caofcan 43683* | Transfer a cancellation law like mulcan 11873 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ:π΄βΆπ) & β’ (π β π»:π΄βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯π π¦) = (π₯π π§) β π¦ = π§)) β β’ (π β ((πΉ βf π πΊ) = (πΉ βf π π») β πΊ = π»)) | ||
Theorem | ofsubid 43684 | Function analogue of subid 11501. (Contributed by Steve Rodriguez, 5-Nov-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ) β (πΉ βf β πΉ) = (π΄ Γ {0})) | ||
Theorem | ofmul12 43685 | Function analogue of mul12 11401. (Contributed by Steve Rodriguez, 13-Nov-2015.) |
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆβ β§ π»:π΄βΆβ)) β (πΉ βf Β· (πΊ βf Β· π»)) = (πΊ βf Β· (πΉ βf Β· π»))) | ||
Theorem | ofdivrec 43686 | Function analogue of divrec 11910, a division analogue of ofnegsub 12232. (Contributed by Steve Rodriguez, 3-Nov-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β (πΉ βf Β· ((π΄ Γ {1}) βf / πΊ)) = (πΉ βf / πΊ)) | ||
Theorem | ofdivcan4 43687 | Function analogue of divcan4 11921. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆ(β β {0})) β ((πΉ βf Β· πΊ) βf / πΊ) = πΉ) | ||
Theorem | ofdivdiv2 43688 | Function analogue of divdiv2 11948. (Contributed by Steve Rodriguez, 23-Nov-2015.) |
β’ (((π΄ β π β§ πΉ:π΄βΆβ) β§ (πΊ:π΄βΆ(β β {0}) β§ π»:π΄βΆ(β β {0}))) β (πΉ βf / (πΊ βf / π»)) = ((πΉ βf Β· π») βf / πΊ)) | ||
Theorem | lhe4.4ex1a 43689 | Example of the Fundamental Theorem of Calculus, part two (ftc2 25966): β«(1(,)2)((π₯β2) β 3) dπ₯ = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 25966 as simply the "Fundamental Theorem of Calculus", then ftc1 25964 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.) |
β’ β«(1(,)2)((π₯β2) β 3) dπ₯ = -(2 / 3) | ||
Theorem | dvsconst 43690 | Derivative of a constant function on the real or complex numbers. The function may return a complex π΄ even if π is β. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
β’ ((π β {β, β} β§ π΄ β β) β (π D (π Γ {π΄})) = (π Γ {0})) | ||
Theorem | dvsid 43691 | Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
β’ (π β {β, β} β (π D ( I βΎ π)) = (π Γ {1})) | ||
Theorem | dvsef 43692 | Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.) |
β’ (π β {β, β} β (π D (exp βΎ π)) = (exp βΎ π)) | ||
Theorem | expgrowthi 43693* | Exponential growth and decay model. See expgrowth 43695 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
β’ (π β π β {β, β}) & β’ (π β πΎ β β) & β’ (π β πΆ β β) & β’ π = (π‘ β π β¦ (πΆ Β· (expβ(πΎ Β· π‘)))) β β’ (π β (π D π) = ((π Γ {πΎ}) βf Β· π)) | ||
Theorem | dvconstbi 43694* | The derivative of a function on π is zero iff it is a constant function. Roughly a biconditional π analogue of dvconst 25833 and dveq0 25920. Corresponds to integration formula "β«0 dπ₯ = πΆ " in section 4.1 of [LarsonHostetlerEdwards] p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
β’ (π β π β {β, β}) & β’ (π β π:πβΆβ) & β’ (π β dom (π D π) = π) β β’ (π β ((π D π) = (π Γ {0}) β βπ β β π = (π Γ {π}))) | ||
Theorem | expgrowth 43695* |
Exponential growth and decay model. The derivative of a function y of
variable t equals a constant k times y itself, iff
y equals some
constant C times the exponential of kt. This theorem and
expgrowthi 43693 illustrate one of the simplest and most
crucial classes of
differential equations, equations that relate functions to their
derivatives.
Section 6.3 of [Strang] p. 242 calls y' = ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as the Malthusian growth model or exponential law, and C, k, and t correspond to initial population size, growth rate, and time respectively (https://en.wikipedia.org/wiki/Malthusian_growth_model 43693); and in finance, the model appears in a similar role in continuous compounding with C as the initial amount of money. In exponential decay models, k is often expressed as the negative of a positive constant Ξ». Here y' is given as (π D π), C as π, and ky as ((π Γ {πΎ}) βf Β· π). (π Γ {πΎ}) is the constant function that maps any real or complex input to k and βf Β· is multiplication as a function operation. The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf 43693 pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of [LarsonHostetlerEdwards] p. 375 (which notes " C is the initial value of y, and k is the proportionality constant. Exponential growth occurs when k > 0, and exponential decay occurs when k < 0."); its proof here closely follows the proof of y' = y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case 43693. Statements for this and expgrowthi 43693 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.) |
β’ (π β π β {β, β}) & β’ (π β πΎ β β) & β’ (π β π:πβΆβ) & β’ (π β dom (π D π) = π) β β’ (π β ((π D π) = ((π Γ {πΎ}) βf Β· π) β βπ β β π = (π‘ β π β¦ (π Β· (expβ(πΎ Β· π‘)))))) | ||
Syntax | cbcc 43696 | Extend class notation to include the generalized binomial coefficient operation. |
class Cπ | ||
Definition | df-bcc 43697* | Define a generalized binomial coefficient operation, which unlike df-bc 14286 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ Cπ = (π β β, π β β0 β¦ ((π FallFac π) / (!βπ))) | ||
Theorem | bccval 43698 | Value of the generalized binomial coefficient, πΆ choose πΎ. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β (πΆCππΎ) = ((πΆ FallFac πΎ) / (!βπΎ))) | ||
Theorem | bcccl 43699 | Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β (πΆCππΎ) β β) | ||
Theorem | bcc0 43700 | The generalized binomial coefficient πΆ choose πΎ is zero iff πΆ is an integer between zero and (πΎ β 1) inclusive. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β πΎ β β0) β β’ (π β ((πΆCππΎ) = 0 β πΆ β (0...(πΎ β 1)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |