![]() |
Metamath
Proof Explorer Theorem List (p. 444 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 | elunif 44301* | A version of eluni 4906 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ β βͺ π΅ β βπ₯(π΄ β π₯ β§ π₯ β π΅)) | ||
Theorem | rzalf 44302 | A version of rzal 4504 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π₯ π΄ = β β β’ (π΄ = β β βπ₯ β π΄ π) | ||
Theorem | fvelrnbf 44303 | 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 44304 | 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 44305* | 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 44306* | 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 44307 | The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (((π΄ β β β§ π΄ < 0) β§ (π΅ β β β§ 0 < π΅)) β (π΄ Β· π΅) < 0) | ||
Theorem | rspcegf 44308 | A version of rspcev 3607 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π₯ = π΄ β (π β π)) β β’ ((π΄ β π΅ β§ π) β βπ₯ β π΅ π) | ||
Theorem | rabexgf 44309 | A version of rabexg 5327 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π₯π΄ β β’ (π΄ β π β {π₯ β π΄ β£ π} β V) | ||
Theorem | fcnre 44310 | 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 44311* | A sum of a singleton is the term. The deduction version of sumsn 15716. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ (π β β²ππ΅) & β’ β²ππ & β’ ((π β§ π = π) β π΄ = π΅) & β’ (π β π β π) & β’ (π β π΅ β β) β β’ (π β Ξ£π β {π}π΄ = π΅) | ||
Theorem | evthf 44312* | A version of evth 24872 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π₯πΉ & β’ β²π¦πΉ & β’ β²π₯π & β’ β²π¦π & β’ β²π₯π & β’ β²π¦π & β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β βπ₯ β π βπ¦ β π (πΉβπ¦) β€ (πΉβπ₯)) | ||
Theorem | cnfex 44313 | The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ ((π½ β Top β§ πΎ β Top) β (π½ Cn πΎ) β V) | ||
Theorem | fnchoice 44314* | 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 44315* | 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 24775 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²π₯π & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (π½ Cn πΎ)) | ||
Theorem | rfcnpre2 44316 | 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 44317* | 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 44318* | 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 44319* | 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 44320* | 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 44321* | 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 44322* | This is the core Lemma for refsum2cn 44323: 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 44323* | 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 44324 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π β§ π) β§ π) β§ π) β π) β β’ (((((π β§ π) β§ π) β§ π) β§ π) β π) | ||
Theorem | 3adantlr3 44325 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π β§ (π β§ π)) β§ π) β π) β β’ (((π β§ (π β§ π β§ π)) β§ π) β π) | ||
Theorem | 3adantll2 44326 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π β§ π) β§ π) β§ π) β π) β β’ ((((π β§ π β§ π) β§ π) β§ π) β π) | ||
Theorem | 3adantll3 44327 | Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π β§ π) β§ π) β§ π) β π) β β’ ((((π β§ π β§ π) β§ π) β§ π) β π) | ||
Theorem | ssnel 44328 | If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β π΅ β§ Β¬ πΆ β π΅) β Β¬ πΆ β π΄) | ||
Theorem | sncldre 44329 | 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 44330 | 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 44331 | Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (Β¬ π β π) & β’ (Β¬ π β Β¬ π) β β’ π | ||
Theorem | pwssfi 44332 | 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 44333 | Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β βͺ π₯ β π΄ π΅ = βͺ π₯ β π΄ πΆ) | ||
Theorem | nnfoctb 44334* | There exists a mapping from β onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π΄ βΌ Ο β§ π΄ β β ) β βπ π:ββontoβπ΄) | ||
Theorem | ssinss1d 44335 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β πΆ) β β’ (π β (π΄ β© π΅) β πΆ) | ||
Theorem | elpwinss 44336 | An element of the powerset of π΅ intersected with anything, is a subset of π΅. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π΄ β (π« π΅ β© πΆ) β π΄ β π΅) | ||
Theorem | unidmex 44337 | If πΉ is a set, then βͺ dom πΉ is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ β π) & β’ π = βͺ dom πΉ β β’ (π β π β V) | ||
Theorem | ndisj2 44338* | A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π₯ = π¦ β π΅ = πΆ) β β’ (Β¬ Disj π₯ β π΄ π΅ β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β§ (π΅ β© πΆ) β β )) | ||
Theorem | zenom 44339 | The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β€ β Ο | ||
Theorem | uzwo4 44340* | 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 44341 | The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ βͺ {β } = β | ||
Theorem | ssin0 44342 | If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (((π΄ β© π΅) = β β§ πΆ β π΄ β§ π· β π΅) β (πΆ β© π·) = β ) | ||
Theorem | inabs3 44343 | Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (πΆ β π΅ β ((π΄ β© π΅) β© πΆ) = (π΄ β© πΆ)) | ||
Theorem | pwpwuni 44344 | Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π΄ β π β (π΄ β π« π« π΅ β βͺ π΄ β π« π΅)) | ||
Theorem | disjiun2 44345* | In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β Disj π₯ β π΄ π΅) & β’ (π β πΆ β π΄) & β’ (π β π· β (π΄ β πΆ)) & β’ (π₯ = π· β π΅ = πΈ) β β’ (π β (βͺ π₯ β πΆ π΅ β© πΈ) = β ) | ||
Theorem | 0pwfi 44346 | The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β β (π« π΄ β© Fin) | ||
Theorem | ssinss2d 44347 | Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΅ β πΆ) β β’ (π β (π΄ β© π΅) β πΆ) | ||
Theorem | zct 44348 | The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β€ βΌ Ο | ||
Theorem | pwfin0 44349 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π« π΄ β© Fin) β β | ||
Theorem | uzct 44350 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ π = (β€β₯βπ) β β’ π βΌ Ο | ||
Theorem | iunxsnf 44351* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯πΆ & β’ π΄ β V & β’ (π₯ = π΄ β π΅ = πΆ) β β’ βͺ π₯ β {π΄}π΅ = πΆ | ||
Theorem | fiiuncl 44352* | 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 44353* | 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 44354* | 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 44355 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ = πΆ) β β’ (π β Xπ₯ β π΄ π΅ = Xπ₯ β π΄ πΆ) | ||
Theorem | disjxp1 44356* | 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 44357* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ Disj π β π΄ ({π} Γ π΅) | ||
Theorem | eliind 44358* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β© π₯ β π΅ πΆ) & β’ (π β πΎ β π΅) & β’ (π₯ = πΎ β (π΄ β πΆ β π΄ β π·)) β β’ (π β π΄ β π·) | ||
Theorem | rspcef 44359 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ & β’ (π₯ = π΄ β (π β π)) β β’ ((π΄ β π΅ β§ π) β βπ₯ β π΅ π) | ||
Theorem | inn0f 44360 | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ ((π΄ β© π΅) β β β βπ₯ β π΄ π₯ β π΅) | ||
Theorem | ixpssmapc 44361* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β²π₯π & β’ (π β πΆ β π) & β’ ((π β§ π₯ β π΄) β π΅ β πΆ) β β’ (π β Xπ₯ β π΄ π΅ β (πΆ βm π΄)) | ||
Theorem | inn0 44362* | A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ ((π΄ β© π΅) β β β βπ₯ β π΄ π₯ β π΅) | ||
Theorem | elintd 44363* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΅) β π΄ β π₯) β β’ (π β π΄ β β© π΅) | ||
Theorem | ssdf 44364* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π₯ β π΅) β β’ (π β π΄ β π΅) | ||
Theorem | brneqtrd 44365 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β Β¬ π΄π π΅) & β’ (π β π΅ = πΆ) β β’ (π β Β¬ π΄π πΆ) | ||
Theorem | ssnct 44366 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β Β¬ π΄ βΌ Ο) & β’ (π β π΄ β π΅) β β’ (π β Β¬ π΅ βΌ Ο) | ||
Theorem | ssuniint 44367* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΅) β π΄ β π₯) β β’ (π β π΄ β βͺ β© π΅) | ||
Theorem | elintdv 44368* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΅) β π΄ β π₯) β β’ (π β π΄ β β© π΅) | ||
Theorem | ssd 44369* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ ((π β§ π₯ β π΄) β π₯ β π΅) β β’ (π β π΄ β π΅) | ||
Theorem | ralimralim 44370 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (βπ₯ β π΄ π β βπ₯ β π΄ (π β π)) | ||
Theorem | snelmap 44371 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β β ) & β’ (π β (π΄ Γ {π₯}) β (π΅ βm π΄)) β β’ (π β π₯ β π΅) | ||
Theorem | xrnmnfpnf 44372 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β Β¬ π΄ β β) & β’ (π β π΄ β -β) β β’ (π β π΄ = +β) | ||
Theorem | nelrnmpt 44373* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯π & β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β πΆ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) β β’ (π β Β¬ πΆ β ran πΉ) | ||
Theorem | iuneq1i 44374* | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ π΄ = π΅ β β’ βͺ π₯ β π΄ πΆ = βͺ π₯ β π΅ πΆ | ||
Theorem | nssrex 44375* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (Β¬ π΄ β π΅ β βπ₯ β π΄ Β¬ π₯ β π΅) | ||
Theorem | ssinc 44376* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π..^π)) β (πΉβπ) β (πΉβ(π + 1))) β β’ (π β (πΉβπ) β (πΉβπ)) | ||
Theorem | ssdec 44377* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π..^π)) β (πΉβ(π + 1)) β (πΉβπ)) β β’ (π β (πΉβπ) β (πΉβπ)) | ||
Theorem | elixpconstg 44378* | Membership in an infinite Cartesian product of a constant π΅. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (πΉ β π β (πΉ β Xπ₯ β π΄ π΅ β πΉ:π΄βΆπ΅)) | ||
Theorem | iineq1d 44379* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ = π΅) β β’ (π β β© π₯ β π΄ πΆ = β© π₯ β π΅ πΆ) | ||
Theorem | metpsmet 44380 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π· β (Metβπ) β π· β (PsMetβπ)) | ||
Theorem | ixpssixp 44381 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β πΆ) β β’ (π β Xπ₯ β π΄ π΅ β Xπ₯ β π΄ πΆ) | ||
Theorem | ballss3 44382* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²π₯π & β’ (π β π· β (PsMetβπ)) & β’ (π β π β π) & β’ (π β π β β*) & β’ ((π β§ π₯ β π β§ (ππ·π₯) < π ) β π₯ β π΄) β β’ (π β (π(ballβπ·)π ) β π΄) | ||
Theorem | iunincfi 44383* | 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 44384 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ ((Β¬ π΄ β π΅ β§ πΆ β π΅) β Β¬ π΄ β πΆ) | ||
Theorem | rexanuz3 44385* | Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²ππ & β’ π = (β€β₯βπ) & β’ (π β βπ β π βπ β (β€β₯βπ)π) & β’ (π β βπ β π βπ β (β€β₯βπ)π) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) β β’ (π β βπ β π (π β§ π)) | ||
Theorem | cbvmpo2 44386* | Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π¦π΄ & β’ β²π€π΄ & β’ β²π€πΆ & β’ β²π¦πΈ & β’ (π¦ = π€ β πΆ = πΈ) β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π₯ β π΄, π€ β π΅ β¦ πΈ) | ||
Theorem | cbvmpo1 44387* | Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π΅ & β’ β²π§π΅ & β’ β²π§πΆ & β’ β²π₯πΈ & β’ (π₯ = π§ β πΆ = πΈ) β β’ (π₯ β π΄, π¦ β π΅ β¦ πΆ) = (π§ β π΄, π¦ β π΅ β¦ πΈ) | ||
Theorem | eliuniin 44388* | Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π΄ = βͺ π₯ β π΅ β© π¦ β πΆ π· β β’ (π β π β (π β π΄ β βπ₯ β π΅ βπ¦ β πΆ π β π·)) | ||
Theorem | ssabf 44389 | Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π΄ β β’ (π΄ β {π₯ β£ π} β βπ₯(π₯ β π΄ β π)) | ||
Theorem | pssnssi 44390 | A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π΄ β π΅ β β’ Β¬ π΅ β π΄ | ||
Theorem | rabidim2 44391 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π₯ β {π₯ β π΄ β£ π} β π) | ||
Theorem | eluni2f 44392* | Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ (π΄ β βͺ π΅ β βπ₯ β π΅ π΄ β π₯) | ||
Theorem | eliin2f 44393* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π₯π΅ β β’ (π΅ β β β (π΄ β β© π₯ β π΅ πΆ β βπ₯ β π΅ π΄ β πΆ)) | ||
Theorem | nssd 44394 | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β π΄) & β’ (π β Β¬ π β π΅) β β’ (π β Β¬ π΄ β π΅) | ||
Theorem | iineq12dv 44395* | Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π₯ β π΅) β πΆ = π·) β β’ (π β β© π₯ β π΄ πΆ = β© π₯ β π΅ π·) | ||
Theorem | supxrcld 44396 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β sup(π΄, β*, < ) β β*) | ||
Theorem | elrestd 44397 | A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π½ β π) & β’ (π β π΅ β π) & β’ (π β π β π½) & β’ π΄ = (π β© π΅) β β’ (π β π΄ β (π½ βΎt π΅)) | ||
Theorem | eliuniincex 44398* | Counterexample to show that the additional conditions in eliuniin 44388 and eliuniin2 44409 are actually needed. Notice that the definition of π΄ is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π΅ = {β } & β’ πΆ = β & β’ π· = β & β’ π = V β β’ Β¬ (π β π΄ β βπ₯ β π΅ βπ¦ β πΆ π β π·) | ||
Theorem | eliincex 44399* | Counterexample to show that the additional conditions in eliin 4996 and eliin2 44405 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π΄ = V & β’ π΅ = β β β’ Β¬ (π΄ β β© π₯ β π΅ πΆ β βπ₯ β π΅ π΄ β πΆ) | ||
Theorem | eliinid 44400* | Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ ((π΄ β β© π₯ β π΅ πΆ β§ π₯ β π΅) β π΄ β πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |