Home | Metamath
Proof Explorer Theorem List (p. 423 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12566 addcomli 11281 00id 11264 addid1i 11276 addid2i 11277 eqid 2738 dec0h 12573 decadd 12605 decaddc 12606. | ||
Theorem | unitadd 42201 | Theorem used in conjunction with decaddc 12606 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π΄ + π΅) = πΉ & β’ (πΆ + 1) = π΅ & β’ π΄ β β0 & β’ πΆ β β0 β β’ ((π΄ + πΆ) + 1) = πΉ | ||
Theorem | gsumws3 42202 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ (π β π΅ β§ π β π΅))) β (πΊ Ξ£g β¨βπππββ©) = (π + (π + π))) | ||
Theorem | gsumws4 42203 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ (π β π΅ β§ (π β π΅ β§ π β π΅)))) β (πΊ Ξ£g β¨βππππββ©) = (π + (π + (π + π)))) | ||
Theorem | amgm2d 42204 | Arithmetic-geometric mean inequality for π = 2, derived from amgmlem 26261. (Contributed by Stanislas Polu, 8-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) β β’ (π β ((π΄ Β· π΅)βπ(1 / 2)) β€ ((π΄ + π΅) / 2)) | ||
Theorem | amgm3d 42205 | Arithmetic-geometric mean inequality for π = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) β β’ (π β ((π΄ Β· (π΅ Β· πΆ))βπ(1 / 3)) β€ ((π΄ + (π΅ + πΆ)) / 3)) | ||
Theorem | amgm4d 42206 | Arithmetic-geometric mean inequality for π = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) & β’ (π β π· β β+) β β’ (π β ((π΄ Β· (π΅ Β· (πΆ Β· π·)))βπ(1 / 4)) β€ ((π΄ + (π΅ + (πΆ + π·))) / 4)) | ||
Theorem | spALT 42207 | sp 2177 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2177 instead. (New usage is discouraged.) |
β’ (βπ₯π β π) | ||
Theorem | elnelneqd 42208 | 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 42209 | 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 42210* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ ((π β§ π₯ = π΄) β π) & β’ (π β π΄ β π) β β’ (π β βπ₯π) | ||
Theorem | rexlimdvaacbv 42211* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3152. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimddvcbvw 42212* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42211. The equivalent of this theorem without the bound variable change is rexlimddv 3157. Version of rexlimddvcbv 42213 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) & β’ (π₯ = π¦ β (π β π)) β β’ (π β π) | ||
Theorem | rexlimddvcbv 42213* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42211. The equivalent of this theorem without the bound variable change is rexlimddv 3157. Usage of this theorem is discouraged because it depends on ax-13 2372, see rexlimddvcbvw 42212 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) & β’ (π₯ = π¦ β (π β π)) β β’ (π β π) | ||
Theorem | rr-elrnmpt3d 42214* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β πΆ β π΄) & β’ (π β π· β π) & β’ ((π β§ π₯ = πΆ) β π΅ = π·) β β’ (π β π· β ran πΉ) | ||
Theorem | finnzfsuppd 42215* | If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.) |
β’ (π β πΉ β π) & β’ (π β πΉ Fn π·) & β’ (π β π β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π·) β (π₯ β π΄ β¨ (πΉβπ₯) = π)) β β’ (π β πΉ finSupp π) | ||
Theorem | rr-phpd 42216 | Equivalent of php 9088 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π β π΄ β Ο) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | suceqd 42217 | Deduction associated with suceq 6380. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π β π΄ = π΅) β β’ (π β suc π΄ = suc π΅) | ||
Theorem | tfindsd 42218* | Deduction associated with tfinds 7787. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = suc π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ π¦ β On β§ π) β π) & β’ ((π β§ Lim π₯ β§ βπ¦ β π₯ π) β π) & β’ (π β π΄ β On) β β’ (π β π) | ||
Syntax | cmnring 42219 | Extend class notation with the monoid ring function. |
class MndRing | ||
Definition | df-mnring 42220* | 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 42221* | 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 42222 | Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (Revised by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (.rβndx) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΈβπ) = (πΈβπΉ)) | ||
Theorem | mnringnmulrdOLD 42223 | Obsolete version of mnringnmulrd 42222 as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ πΈ = Slot π & β’ π β β & β’ π β (.rβndx) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΈβπ) = (πΈβπΉ)) | ||
Theorem | mnringbased 42224 | The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (BaseβπΉ)) | ||
Theorem | mnringbasedOLD 42225 | Obsolete version of mnringnmulrd 42222 as of 1-Nov-2024. The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (BaseβπΉ)) | ||
Theorem | mnringbaserd 42226 | The base set of a monoid ring. Converse of mnringbased 42224. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | mnringelbased 42227 | 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 42228 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ πΆ = (Baseβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β π:π΄βΆπΆ) | ||
Theorem | mnringbasefsuppd 42229 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ 0 = (0gβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β π finSupp 0 ) | ||
Theorem | mnringaddgd 42230 | The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (+gβπ) = (+gβπΉ)) | ||
Theorem | mnringaddgdOLD 42231 | Obsolete version of mnringaddgd 42230 as of 1-Nov-2024. The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (+gβπ) = (+gβπΉ)) | ||
Theorem | mnring0gd 42232 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (0gβπ) = (0gβπΉ)) | ||
Theorem | mnring0g2d 42233 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ 0 = (0gβπ ) & β’ π΄ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β (π΄ Γ { 0 }) = (0gβπΉ)) | ||
Theorem | mnringmulrd 42234* | 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 42235 | The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = (ScalarβπΉ)) | ||
Theorem | mnringscadOLD 42236 | Obsolete version of mnringscad 42235 as of 1-Nov-2024. The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = (ScalarβπΉ)) | ||
Theorem | mnringvscad 42237 | The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (Baseβπ) & β’ π = (π freeLMod π΅) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( Β·π βπ) = ( Β·π βπΉ)) | ||
Theorem | mnringvscadOLD 42238 | Obsolete version of mnringvscad 42237 as of 1-Nov-2024. The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (Baseβπ) & β’ π = (π freeLMod π΅) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( Β·π βπ) = ( Β·π βπΉ)) | ||
Theorem | mnringlmodd 42239 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β πΉ β LMod) | ||
Theorem | mnringmulrvald 42240* | 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 42241 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ Β· = (.rβπΉ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | gru0eld 42242 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β β β πΊ) | ||
Theorem | grusucd 42243 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β suc π΄ β πΊ) | ||
Theorem | r1rankcld 42244 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΄ β (π 1βπ )) β β’ (π β (rankβπ΄) β (π 1βπ )) | ||
Theorem | grur1cld 42245 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β (π 1βπ΄) β πΊ) | ||
Theorem | grurankcld 42246 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β (rankβπ΄) β πΊ) | ||
Theorem | grurankrcld 42247 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β (rankβπ΄) β πΊ) & β’ (π β π΄ β π) β β’ (π β π΄ β πΊ) | ||
Syntax | cscott 42248 | Extend class notation with the Scott's trick operation. |
class Scott π΄ | ||
Definition | df-scott 42249* | 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 42250 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β π΄ = π΅) β β’ (π β Scott π΄ = Scott π΅) | ||
Theorem | scotteq 42251 | Closed form of scotteqd 42250. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π΄ = π΅ β Scott π΄ = Scott π΅) | ||
Theorem | nfscott 42252 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ β²π₯π΄ β β’ β²π₯Scott π΄ | ||
Theorem | scottabf 42253* | Value of the Scott operation at a class abstraction. Variant of scottab 42254 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ β²π₯π & β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottab 42254* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottabes 42255* | Value of the Scott operation at a class abstraction. Variant of scottab 42254 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottss 42256 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ Scott π΄ β π΄ | ||
Theorem | elscottab 42257* | 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 42258 | scottex 9755 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ Scott π΄ β V | ||
Theorem | scotteld 42259* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β βπ₯ π₯ β π΄) β β’ (π β βπ₯ π₯ β Scott π΄) | ||
Theorem | scottelrankd 42260 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) & β’ (π β πΆ β Scott π΄) β β’ (π β (rankβπ΅) β (rankβπΆ)) | ||
Theorem | scottrankd 42261 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) β β’ (π β (rankβScott π΄) = suc (rankβπ΅)) | ||
Theorem | gruscottcld 42262 | 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 42263 | Extend class notation with the collection operation. |
class (πΉ Coll π΄) | ||
Definition | df-coll 42264* | 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 42265* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ Coll π΄) = βͺ π₯ β π΄ Scott {π¦ β£ π₯πΉπ¦} | ||
Theorem | colleq12d 42266 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΉ = πΊ) & β’ (π β π΄ = π΅) β β’ (π β (πΉ Coll π΄) = (πΊ Coll π΅)) | ||
Theorem | colleq1 42267 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ = πΊ β (πΉ Coll π΄) = (πΊ Coll π΄)) | ||
Theorem | colleq2 42268 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π΄ = π΅ β (πΉ Coll π΄) = (πΉ Coll π΅)) | ||
Theorem | nfcoll 42269 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ β²π₯πΉ & β’ β²π₯π΄ β β’ β²π₯(πΉ Coll π΄) | ||
Theorem | collexd 42270 | 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 42271* | Property of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π₯ β π΄) & β’ (π β π₯πΉπ¦) β β’ (π β βπ¦ β (πΉ Coll π΄)π₯πΉπ¦) | ||
Theorem | cpcoll2d 42272* | cpcolld 42271 with an extra existential quantifier. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ (π β π₯ β π΄) & β’ (π β βπ¦ π₯πΉπ¦) β β’ (π β βπ¦ β (πΉ Coll π΄)π₯πΉπ¦) | ||
Theorem | grucollcld 42273 | 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 42274* |
The hypothesis of this theorem defines a class M of sets that we
temporarily call "minimal universes", and which will turn out
in
grumnueq 42300 to be exactly Grothendicek universes.
Minimal universes are
sets which satisfy the predicate on π¦ in rr-groth 42312, except for the
π₯
β π¦ clause.
A minimal universe is closed under subsets (mnussd 42276), powersets (mnupwd 42280), and an operation which is similar to a combination of collection and union (mnuop3d 42284), from which closure under pairing (mnuprd 42289), unions (mnuunid 42290), and function ranges (mnurnd 42296) can be deduced, from which equivalence with Grothendieck universes (grumnueq 42300) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} β β’ (π β π β (π β π β βπ§ β π (π« π§ β π β§ βπβπ€ β π (π« π§ β π€ β§ βπ β π§ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€)))))) | ||
Theorem | mnuop123d 42275* | Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β (π« π΄ β π β§ βπβπ€ β π (π« π΄ β π€ β§ βπ β π΄ (βπ£ β π (π β π£ β§ π£ β π) β βπ’ β π (π β π’ β§ βͺ π’ β π€))))) | ||
Theorem | mnussd 42276* | Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | mnuss2d 42277* | mnussd 42276 with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β βπ₯ β π π΄ β π₯) β β’ (π β π΄ β π) | ||
Theorem | mnu0eld 42278* | A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β β β π) | ||
Theorem | mnuop23d 42279* | Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β πΉ β π) β β’ (π β βπ€ β π (π« π΄ β π€ β§ βπ β π΄ (βπ£ β π (π β π£ β§ π£ β πΉ) β βπ’ β πΉ (π β π’ β§ βͺ π’ β π€)))) | ||
Theorem | mnupwd 42280* | Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β π« π΄ β π) | ||
Theorem | mnusnd 42281* | Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β {π΄} β π) | ||
Theorem | mnuprssd 42282* | A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β πΆ β π) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuprss2d 42283* | Special case of mnuprssd 42282. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β πΆ β π) & β’ π΄ β πΆ & β’ π΅ β πΆ β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuop3d 42284* | Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β πΉ β π) β β’ (π β βπ€ β π βπ β π΄ (βπ£ β πΉ π β π£ β βπ’ β πΉ (π β π’ β§ βͺ π’ β π€))) | ||
Theorem | mnuprdlem1 42285* | Lemma for mnuprd 42289. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β βπ β {β , {β }}βπ’ β πΉ (π β π’ β§ βͺ π’ β π€)) β β’ (π β π΄ β π€) | ||
Theorem | mnuprdlem2 42286* | Lemma for mnuprd 42289. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ (π β π΅ β π) & β’ (π β Β¬ π΄ = β ) & β’ (π β βπ β {β , {β }}βπ’ β πΉ (π β π’ β§ βͺ π’ β π€)) β β’ (π β π΅ β π€) | ||
Theorem | mnuprdlem3 42287* | Lemma for mnuprd 42289. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ β²ππ β β’ (π β βπ β {β , {β }}βπ£ β πΉ π β π£) | ||
Theorem | mnuprdlem4 42288* | Lemma for mnuprd 42289. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ πΉ = {{β , {π΄}}, {{β }, {π΅}}} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β Β¬ π΄ = β ) β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuprd 42289* | Minimal universes are closed under pairing. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β {π΄, π΅} β π) | ||
Theorem | mnuunid 42290* | Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) β β’ (π β βͺ π΄ β π) | ||
Theorem | mnuund 42291* | Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄ βͺ π΅) β π) | ||
Theorem | mnutrcld 42292* | Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π΄) β β’ (π β π΅ β π) | ||
Theorem | mnutrd 42293* | Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) β β’ (π β Tr π) | ||
Theorem | mnurndlem1 42294* | Lemma for mnurnd 42296. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ (π β πΉ:π΄βΆπ) & β’ π΄ β V & β’ (π β βπ β π΄ (βπ£ β ran (π β π΄ β¦ {π, {(πΉβπ), π΄}})π β π£ β βπ’ β ran (π β π΄ β¦ {π, {(πΉβπ), π΄}})(π β π’ β§ βͺ π’ β π€))) β β’ (π β ran πΉ β π€) | ||
Theorem | mnurndlem2 42295* | Lemma for mnurnd 42296. Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ) & β’ π΄ β V β β’ (π β ran πΉ β π) | ||
Theorem | mnurnd 42296* | 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 42297* | Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β π β π) β β’ (π β π β Univ) | ||
Theorem | grumnudlem 42298* | Lemma for grumnud 42299. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β πΊ β Univ) & β’ πΉ = ({β¨π, πβ© β£ βπ(βͺ π = π β§ π β π β§ π β π)} β© (πΊ Γ πΊ)) & β’ ((π β πΊ β§ β β πΊ) β (ππΉβ β βπ(βͺ π = β β§ π β π β§ π β π))) & β’ ((β β (πΉ Coll π§) β§ (βͺ π = β β§ π β π β§ π β π)) β βπ’ β π (π β π’ β§ βͺ π’ β (πΉ Coll π§))) β β’ (π β πΊ β π) | ||
Theorem | grumnud 42299* | Grothendieck universes are minimal universes. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ π = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} & β’ (π β πΊ β Univ) β β’ (π β πΊ β π) | ||
Theorem | grumnueq 42300* | The class of Grothendieck universes is equal to the class of minimal universes. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
β’ Univ = {π β£ βπ β π (π« π β π β§ βπβπ β π (π« π β π β§ βπ β π (βπ β π (π β π β§ π β π) β βπ β π (π β π β§ βͺ π β π))))} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |