HomeTheorem List (p. 441 of 480)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 441 of 480) | < 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-30435) |
Hilbert Space Explorer
(30436-31958) |
Users' Mathboxes
(31959-47941) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sineq0ALT 44001 | A complex number whose sine is zero is an integer multiple of Ο. The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 44001. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 26266. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/sineq0altro.html 26266 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ (π΄ β β β ((sinβπ΄) = 0 β (π΄ / Ο) β β€)) | ||
| Theorem | evth2f 44002* | A version of evth2 24707 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯πΉ & β’ β²π¦πΉ & β’ β²π₯π & β’ β²π¦π & β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β βπ₯ β π βπ¦ β π (πΉβπ₯) β€ (πΉβπ¦)) | ||
| Theorem | elunif 44003* | A version of eluni 4912 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ β βͺ π΅ β βπ₯(π΄ β π₯ β§ π₯ β π΅)) | ||
| Theorem | rzalf 44004 | A version of rzal 4509 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯ π΄ = β β β’ (π΄ = β β βπ₯ β π΄ π) | ||
| Theorem | fvelrnbf 44005 | A version of fvelrnb 6953 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯πΉ β β’ (πΉ Fn π΄ β (π΅ β ran πΉ β βπ₯ β π΄ (πΉβπ₯) = π΅)) | ||
| Theorem | rfcnpre1 44006 | If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π΅ & β’ β²π₯πΉ & β’ β²π₯π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ π΄ = {π₯ β π β£ π΅ < (πΉβπ₯)} & β’ (π β π΅ β β*) & β’ (π β πΉ β (π½ Cn πΎ)) β β’ (π β π΄ β π½) | ||
| Theorem | ubelsupr 44007* | If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ ((π΄ β β β§ π β π΄ β§ βπ₯ β π΄ π₯ β€ π) β π = sup(π΄, β, < )) | ||
| Theorem | fsumcnf 44008* | A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (π½ Cn πΎ)) | ||
| Theorem | mulltgt0 44009 | The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ (((π΄ β β β§ π΄ < 0) β§ (π΅ β β β§ 0 < π΅)) β (π΄ Β· π΅) < 0) | ||
| Theorem | rspcegf 44010 | A version of rspcev 3613 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π₯ = π΄ β (π β π)) β β’ ((π΄ β π΅ β§ π) β βπ₯ β π΅ π) | ||
| Theorem | rabexgf 44011 | A version of rabexg 5332 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π΄ β β’ (π΄ β π β {π₯ β π΄ β£ π} β V) | ||
| Theorem | fcnre 44012 | A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ πΆ = (π½ Cn πΎ) & β’ (π β πΉ β πΆ) β β’ (π β πΉ:πβΆβ) | ||
| Theorem | sumsnd 44013* | A sum of a singleton is the term. The deduction version of sumsn 15697. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ (π β β²ππ΅) & β’ β²ππ & β’ ((π β§ π = π) β π΄ = π΅) & β’ (π β π β π) & β’ (π β π΅ β β) β β’ (π β Ξ£π β {π}π΄ = π΅) | ||
| Theorem | evthf 44014* | A version of evth 24706 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯πΉ & β’ β²π¦πΉ & β’ β²π₯π & β’ β²π¦π & β’ β²π₯π & β’ β²π¦π & β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β βπ₯ β π βπ¦ β π (πΉβπ¦) β€ (πΉβπ₯)) | ||
| Theorem | cnfex 44015 | The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ ((π½ β Top β§ πΎ β Top) β (π½ Cn πΎ) β V) | ||
| Theorem | fnchoice 44016* | For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ (π΄ β Fin β βπ(π Fn π΄ β§ βπ₯ β π΄ (π₯ β β β (πβπ₯) β π₯))) | ||
| Theorem | refsumcn 44017* | A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn 24609 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (π½ Cn πΎ)) | ||
| Theorem | rfcnpre2 44018 | If πΉ is a continuous function with respect to the standard topology, then the preimage A of the values smaller than a given extended real π΅, is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π΅ & β’ β²π₯πΉ & β’ β²π₯π & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ π΄ = {π₯ β π β£ (πΉβπ₯) < π΅} & β’ (π β π΅ β β*) & β’ (π β πΉ β (π½ Cn πΎ)) β β’ (π β π΄ β π½) | ||
| Theorem | cncmpmax 44019* | When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β (sup(ran πΉ, β, < ) β ran πΉ β§ sup(ran πΉ, β, < ) β β β§ βπ‘ β π (πΉβπ‘) β€ sup(ran πΉ, β, < ))) | ||
| Theorem | rfcnpre3 44020* | If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π‘πΉ & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ π΄ = {π‘ β π β£ π΅ β€ (πΉβπ‘)} & β’ (π β π΅ β β) & β’ (π β πΉ β (π½ Cn πΎ)) β β’ (π β π΄ β (Clsdβπ½)) | ||
| Theorem | rfcnpre4 44021* | If F is a continuous function with respect to the standard topology, then the preimage A of the values less than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π‘πΉ & β’ πΎ = (topGenβran (,)) & β’ π = βͺ π½ & β’ π΄ = {π‘ β π β£ (πΉβπ‘) β€ π΅} & β’ (π β π΅ β β) & β’ (π β πΉ β (π½ Cn πΎ)) β β’ (π β π΄ β (Clsdβπ½)) | ||
| Theorem | sumpair 44022* | Sum of two distinct complex values. The class expression for π΄ and π΅ normally contain free variable π to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ (π β β²ππ·) & β’ (π β β²ππΈ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β β) & β’ (π β πΈ β β) & β’ (π β π΄ β π΅) & β’ ((π β§ π = π΄) β πΆ = π·) & β’ ((π β§ π = π΅) β πΆ = πΈ) β β’ (π β Ξ£π β {π΄, π΅}πΆ = (π· + πΈ)) | ||
| Theorem | rfcnnnub 44023* | Given a real continuous function πΉ defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π‘πΉ & β’ β²π‘π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ π = βͺ π½ & β’ (π β π β β ) & β’ πΆ = (π½ Cn πΎ) & β’ (π β πΉ β πΆ) β β’ (π β βπ β β βπ‘ β π (πΉβπ‘) < π) | ||
| Theorem | refsum2cnlem1 44024* | This is the core Lemma for refsum2cn 44025: the sum of two continuous real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯π΄ & β’ β²π₯πΉ & β’ β²π₯πΊ & β’ β²π₯π & β’ π΄ = (π β {1, 2} β¦ if(π = 1, πΉ, πΊ)) & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ ((πΉβπ₯) + (πΊβπ₯))) β (π½ Cn πΎ)) | ||
| Theorem | refsum2cn 44025* | The sum of two continuus real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
| β’ β²π₯πΉ & β’ β²π₯πΊ & β’ β²π₯π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ ((πΉβπ₯) + (πΊβπ₯))) β (π½ Cn πΎ)) | ||
| Theorem | adantlllr 44026 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ ((((π β§ π) β§ π) β§ π) β π) β β’ (((((π β§ π) β§ π) β§ π) β§ π) β π) | ||
| Theorem | 3adantlr3 44027 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ (((π β§ (π β§ π)) β§ π) β π) β β’ (((π β§ (π β§ π β§ π)) β§ π) β π) | ||
| Theorem | 3adantll2 44028 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ ((((π β§ π) β§ π) β§ π) β π) β β’ ((((π β§ π β§ π) β§ π) β§ π) β π) | ||
| Theorem | 3adantll3 44029 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ ((((π β§ π) β§ π) β§ π) β π) β β’ ((((π β§ π β§ π) β§ π) β§ π) β π) | ||
| Theorem | ssnel 44030 | If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ ((π΄ β π΅ β§ Β¬ πΆ β π΅) β Β¬ πΆ β π΄) | ||
| Theorem | elabrexg 44031* | Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ ((π₯ β π΄ β§ π΅ β π) β π΅ β {π¦ β£ βπ₯ β π΄ π¦ = π΅}) | ||
| Theorem | sncldre 44032 | A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| β’ (π΄ β β β {π΄} β (Clsdβ(topGenβran (,)))) | ||
| Theorem | n0p 44033 | A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| β’ ((π β (Polyββ€) β§ π β β0 β§ ((coeffβπ)βπ) β 0) β π β 0π) | ||
| Theorem | pm2.65ni 44034 | Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| β’ (Β¬ π β π) & β’ (Β¬ π β Β¬ π) β β’ π | ||
| Theorem | pwssfi 44035 | Every element of the power set of π΄ is finite if and only if π΄ is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π΄ β π β (π΄ β Fin β π« π΄ β Fin)) | ||
| Theorem | iuneq2df 44036 | Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β βͺ π₯ β π΄ π΅ = βͺ π₯ β π΄ πΆ) | ||
| Theorem | nnfoctb 44037* | There exists a mapping from β onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ ((π΄ βΌ Ο β§ π΄ β β ) β βπ π:ββontoβπ΄) | ||
| Theorem | ssinss1d 44038 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π β π΄ β πΆ) β β’ (π β (π΄ β© π΅) β πΆ) | ||
| Theorem | elpwinss 44039 | An element of the powerset of π΅ intersected with anything, is a subset of π΅. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π΄ β (π« π΅ β© πΆ) β π΄ β π΅) | ||
| Theorem | unidmex 44040 | If πΉ is a set, then βͺ dom πΉ is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π β πΉ β π) & β’ π = βͺ dom πΉ β β’ (π β π β V) | ||
| Theorem | ndisj2 44041* | A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π₯ = π¦ β π΅ = πΆ) β β’ (Β¬ Disj π₯ β π΄ π΅ β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β§ (π΅ β© πΆ) β β )) | ||
| Theorem | zenom 44042 | The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β€ β Ο | ||
| Theorem | uzwo4 44043* | Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β²ππ & β’ (π = π β (π β π)) β β’ ((π β (β€β₯βπ) β§ βπ β π π) β βπ β π (π β§ βπ β π (π < π β Β¬ π))) | ||
| Theorem | unisn0 44044 | The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ βͺ {β } = β | ||
| Theorem | ssin0 44045 | If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (((π΄ β© π΅) = β β§ πΆ β π΄ β§ π· β π΅) β (πΆ β© π·) = β ) | ||
| Theorem | inabs3 44046 | Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (πΆ β π΅ β ((π΄ β© π΅) β© πΆ) = (π΄ β© πΆ)) | ||
| Theorem | pwpwuni 44047 | Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π΄ β π β (π΄ β π« π« π΅ β βͺ π΄ β π« π΅)) | ||
| Theorem | disjiun2 44048* | In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π β Disj π₯ β π΄ π΅) & β’ (π β πΆ β π΄) & β’ (π β π· β (π΄ β πΆ)) & β’ (π₯ = π· β π΅ = πΈ) β β’ (π β (βͺ π₯ β πΆ π΅ β© πΈ) = β ) | ||
| Theorem | 0pwfi 44049 | The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β β (π« π΄ β© Fin) | ||
| Theorem | ssinss2d 44050 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π β π΅ β πΆ) β β’ (π β (π΄ β© π΅) β πΆ) | ||
| Theorem | zct 44051 | The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β€ βΌ Ο | ||
| Theorem | pwfin0 44052 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ (π« π΄ β© Fin) β β | ||
| Theorem | uzct 44053 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ π = (β€β₯βπ) β β’ π βΌ Ο | ||
| Theorem | iunxsnf 44054* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β²π₯πΆ & β’ π΄ β V & β’ (π₯ = π΄ β π΅ = πΆ) β β’ βͺ π₯ β {π΄}π΅ = πΆ | ||
| Theorem | fiiuncl 44055* | If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β π·) & β’ ((π β§ π¦ β π· β§ π§ β π·) β (π¦ βͺ π§) β π·) & β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) β β’ (π β βͺ π₯ β π΄ π΅ β π·) | ||
| Theorem | iunp1 44056* | The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ β²ππ΅ & β’ (π β π β (β€β₯βπ)) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β βͺ π β (π...(π + 1))π΄ = (βͺ π β (π...π)π΄ βͺ π΅)) | ||
| Theorem | fiunicl 44057* | If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| β’ ((π β§ π₯ β π΄ β§ π¦ β π΄) β (π₯ βͺ π¦) β π΄) & β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) β β’ (π β βͺ π΄ β π΄) | ||
| Theorem | ixpeq2d 44058 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β Xπ₯ β π΄ π΅ = Xπ₯ β π΄ πΆ) | ||
| Theorem | disjxp1 44059* | The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| β’ (π β Disj π₯ β π΄ π΅) β β’ (π β Disj π₯ β π΄ (π΅ Γ πΆ)) | ||
| Theorem | disjsnxp 44060* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| β’ Disj π β π΄ ({π} Γ π΅) | ||
| Theorem | eliind 44061* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| β’ (π β π΄ β β© π₯ β π΅ πΆ) & β’ (π β πΎ β π΅) & β’ (π₯ = πΎ β (π΄ β πΆ β π΄ β π·)) β β’ (π β π΄ β π·) | ||
| Theorem | rspcef 44062 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π₯ = π΄ β (π β π)) β β’ ((π΄ β π΅ β§ π) β βπ₯ β π΅ π) | ||
| Theorem | inn0f 44063 | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| β’ β²π₯π΄ & β’ β²π₯π΅ β β’ ((π΄ β© π΅) β β β βπ₯ β π΄ π₯ β π΅) | ||
| Theorem | ixpssmapc 44064* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| β’ β²π₯π & β’ (π β πΆ β π) & β’ ((π β§ π₯ β π΄) β π΅ β πΆ) β β’ (π β Xπ₯ β π΄ π΅ β (πΆ βm π΄)) | ||
| Theorem | inn0 44065* | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| β’ ((π΄ β© π΅) β β β βπ₯ β π΄ π₯ β π΅) | ||
| Theorem | elintd 44066* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΅) β π΄ β π₯) β β’ (π β π΄ β β© π΅) | ||
| Theorem | ssdf 44067* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π₯ β π΅) β β’ (π β π΄ β π΅) | ||
| Theorem | brneqtrd 44068 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ (π β Β¬ π΄π π΅) & β’ (π β π΅ = πΆ) β β’ (π β Β¬ π΄π πΆ) | ||
| Theorem | ssnct 44069 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ (π β Β¬ π΄ βΌ Ο) & β’ (π β π΄ β π΅) β β’ (π β Β¬ π΅ βΌ Ο) | ||
| Theorem | ssuniint 44070* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΅) β π΄ β π₯) β β’ (π β π΄ β βͺ β© π΅) | ||
| Theorem | elintdv 44071* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΅) β π΄ β π₯) β β’ (π β π΄ β β© π΅) | ||
| Theorem | ssd 44072* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| β’ ((π β§ π₯ β π΄) β π₯ β π΅) β β’ (π β π΄ β π΅) | ||
| Theorem | ralimralim 44073 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| β’ (βπ₯ β π΄ π β βπ₯ β π΄ (π β π)) | ||
| Theorem | snelmap 44074 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β β ) & β’ (π β (π΄ Γ {π₯}) β (π΅ βm π΄)) β β’ (π β π₯ β π΅) | ||
| Theorem | xrnmnfpnf 44075 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| β’ (π β π΄ β β*) & β’ (π β Β¬ π΄ β β) & β’ (π β π΄ β -β) β β’ (π β π΄ = +β) | ||
| Theorem | nelrnmpt 44076* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| β’ β²π₯π & β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β πΆ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) β β’ (π β Β¬ πΆ β ran πΉ) | ||
| Theorem | iuneq1i 44077* | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| β’ π΄ = π΅ β β’ βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ πΆ | ||
| Theorem | nssrex 44078* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| β’ (Β¬ π΄ β π΅ β βπ₯ β π΄ Β¬ π₯ β π΅) | ||
| Theorem | ssinc 44079* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π..^π)) β (πΉβπ) β (πΉβ(π + 1))) β β’ (π β (πΉβπ) β (πΉβπ)) | ||
| Theorem | ssdec 44080* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π..^π)) β (πΉβ(π + 1)) β (πΉβπ)) β β’ (π β (πΉβπ) β (πΉβπ)) | ||
| Theorem | elixpconstg 44081* | Membership in an infinite Cartesian product of a constant π΅. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ (πΉ β π β (πΉ β Xπ₯ β π΄ π΅ β πΉ:π΄βΆπ΅)) | ||
| Theorem | iineq1d 44082* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ (π β π΄ = π΅) β β’ (π β β© π₯ β π΄ πΆ = β© π₯ β π΅ πΆ) | ||
| Theorem | metpsmet 44083 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ (π· β (Metβπ) β π· β (PsMetβπ)) | ||
| Theorem | ixpssixp 44084 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β πΆ) β β’ (π β Xπ₯ β π΄ π΅ β Xπ₯ β π΄ πΆ) | ||
| Theorem | ballss3 44085* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ β²π₯π & β’ (π β π· β (PsMetβπ)) & β’ (π β π β π) & β’ (π β π β β*) & β’ ((π β§ π₯ β π β§ (ππ·π₯) < π ) β π₯ β π΄) β β’ (π β (π(ballβπ·)π ) β π΄) | ||
| Theorem | iunincfi 44086* | Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π..^π)) β (πΉβπ) β (πΉβ(π + 1))) β β’ (π β βͺ π β (π...π)(πΉβπ) = (πΉβπ)) | ||
| Theorem | nsstr 44087 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ ((Β¬ π΄ β π΅ β§ πΆ β π΅) β Β¬ π΄ β πΆ) | ||
| Theorem | rexanuz3 44088* | Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ β²ππ & β’ π = (β€β₯βπ) & β’ (π β βπ β π βπ β (β€β₯βπ)π) & β’ (π β βπ β π βπ β (β€β₯βπ)π) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) β β’ (π β βπ β π (π β§ π)) | ||
| Theorem | cbvmpo2 44089* | Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ β²π¦π΄ & β’ β²π€π΄ & β’ β²π€πΆ & β’ β²π¦πΈ & β’ (π¦ = π€ β πΆ = πΈ) β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π₯ β π΄, π€ β π΅ β¦ πΈ) | ||
| Theorem | cbvmpo1 44090* | Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ β²π₯π΅ & β’ β²π§π΅ & β’ β²π§πΆ & β’ β²π₯πΈ & β’ (π₯ = π§ β πΆ = πΈ) β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π§ β π΄, π¦ β π΅ β¦ πΈ) | ||
| Theorem | eliuniin 44091* | Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ π΄ = βͺ π₯ β π΅ β© π¦ β πΆ π· β β’ (π β π β (π β π΄ β βπ₯ β π΅ βπ¦ β πΆ π β π·)) | ||
| Theorem | ssabf 44092 | Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ β²π₯π΄ β β’ (π΄ β {π₯ β£ π} β βπ₯(π₯ β π΄ β π)) | ||
| Theorem | pssnssi 44093 | A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ π΄ β π΅ β β’ Β¬ π΅ β π΄ | ||
| Theorem | rabidim2 44094 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ (π₯ β {π₯ β π΄ β£ π} β π) | ||
| Theorem | eluni2f 44095* | Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ β βͺ π΅ β βπ₯ β π΅ π΄ β π₯) | ||
| Theorem | eliin2f 44096* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ β²π₯π΅ β β’ (π΅ β β β (π΄ β β© π₯ β π΅ πΆ β βπ₯ β π΅ π΄ β πΆ)) | ||
| Theorem | nssd 44097 | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ (π β π β π΄) & β’ (π β Β¬ π β π΅) β β’ (π β Β¬ π΄ β π΅) | ||
| Theorem | iineq12dv 44098* | Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΅) β πΆ = π·) β β’ (π β β© π₯ β π΄ πΆ = β© π₯ β π΅ π·) | ||
| Theorem | supxrcld 44099 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ (π β π΄ β β*) β β’ (π β sup(π΄, β*, < ) β β*) | ||
| Theorem | elrestd 44100 | A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| β’ (π β π½ β π) & β’ (π β π΅ β π) & β’ (π β π β π½) & β’ π΄ = (π β© π΅) β β’ (π β π΄ β (π½ βΎt π΅)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |