![]() |
Metamath
Proof Explorer Theorem List (p. 348 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | shftvalg 34701 | Value of a sequence shifted by π΄. (Contributed by Scott Fenton, 16-Dec-2017.) |
β’ ((πΉ β π β§ π΄ β β β§ π΅ β β) β ((πΉ shift π΄)βπ΅) = (πΉβ(π΅ β π΄))) | ||
Theorem | divcnvlin 34702* | Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β β) & β’ (π β π΅ β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = ((π + π΄) / (π + π΅))) β β’ (π β πΉ β 1) | ||
Theorem | climlec3 34703* | Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΅ β β) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ π΅) β β’ (π β π΄ β€ π΅) | ||
Theorem | logi 34704 | Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
β’ (logβi) = (i Β· (Ο / 2)) | ||
Theorem | iexpire 34705 | i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.) |
β’ (iβπi) β β | ||
Theorem | bcneg1 34706 | The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.) |
β’ (π β β0 β (πC-1) = 0) | ||
Theorem | bcm1nt 34707 | The proportion of one bionmial coefficient to another with π decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.) |
β’ ((π β β β§ πΎ β (0...(π β 1))) β (πCπΎ) = (((π β 1)CπΎ) Β· (π / (π β πΎ)))) | ||
Theorem | bcprod 34708* | A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.) |
β’ (π β β β βπ β (1...(π β 1))((π β 1)Cπ) = βπ β (1...(π β 1))(πβ((2 Β· π) β π))) | ||
Theorem | bccolsum 34709* | A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.) |
β’ ((π β β0 β§ πΆ β β0) β Ξ£π β (0...π)(πCπΆ) = ((π + 1)C(πΆ + 1))) | ||
Theorem | iprodefisumlem 34710 | Lemma for iprodefisum 34711. (Contributed by Scott Fenton, 11-Feb-2018.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) β β’ (π β seqπ( Β· , (exp β πΉ)) = (exp β seqπ( + , πΉ))) | ||
Theorem | iprodefisum 34711* | Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β βπ β π (expβπ΅) = (expβΞ£π β π π΅)) | ||
Theorem | iprodgam 34712* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
β’ (π β π΄ β (β β (β€ β β))) β β’ (π β (Ξβπ΄) = (βπ β β (((1 + (1 / π))βππ΄) / (1 + (π΄ / π))) / π΄)) | ||
Theorem | faclimlem1 34713* | Lemma for faclim 34716. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.) |
β’ (π β β0 β seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) = (π₯ β β β¦ ((π + 1) Β· ((π₯ + 1) / (π₯ + (π + 1)))))) | ||
Theorem | faclimlem2 34714* | Lemma for faclim 34716. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
β’ (π β β0 β seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) β (π + 1)) | ||
Theorem | faclimlem3 34715 | Lemma for faclim 34716. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.) |
β’ ((π β β0 β§ π΅ β β) β (((1 + (1 / π΅))β(π + 1)) / (1 + ((π + 1) / π΅))) = ((((1 + (1 / π΅))βπ) / (1 + (π / π΅))) Β· (((1 + (π / π΅)) Β· (1 + (1 / π΅))) / (1 + ((π + 1) / π΅))))) | ||
Theorem | faclim 34716* | An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.) |
β’ πΉ = (π β β β¦ (((1 + (1 / π))βπ΄) / (1 + (π΄ / π)))) β β’ (π΄ β β0 β seq1( Β· , πΉ) β (!βπ΄)) | ||
Theorem | iprodfac 34717* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
β’ (π΄ β β0 β (!βπ΄) = βπ β β (((1 + (1 / π))βπ΄) / (1 + (π΄ / π)))) | ||
Theorem | faclim2 34718* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
β’ πΉ = (π β β β¦ (((!βπ) Β· ((π + 1)βπ)) / (!β(π + π)))) β β’ (π β β0 β πΉ β 1) | ||
Theorem | gcd32 34719 | Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β ((π΄ gcd π΅) gcd πΆ) = ((π΄ gcd πΆ) gcd π΅)) | ||
Theorem | gcdabsorb 34720 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅) gcd π΅) = (π΄ gcd π΅)) | ||
Theorem | dftr6 34721 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
β’ π΄ β V β β’ (Tr π΄ β π΄ β (V β ran (( E β E ) β E ))) | ||
Theorem | coep 34722* | Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄( E β π )π΅ β βπ₯ β π΅ π΄π π₯) | ||
Theorem | coepr 34723* | Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄(π β β‘ E )π΅ β βπ₯ β π΄ π₯π π΅) | ||
Theorem | dffr5 34724 | A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.) |
β’ (π Fr π΄ β (π« π΄ β {β }) β ran ( E β ( E β β‘π ))) | ||
Theorem | dfso2 34725 | Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
β’ (π Or π΄ β (π Po π΄ β§ (π΄ Γ π΄) β (π βͺ ( I βͺ β‘π )))) | ||
Theorem | br8 34726* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
β’ (π = π΄ β (π β π)) & β’ (π = π΅ β (π β π)) & β’ (π = πΆ β (π β π)) & β’ (π = π· β (π β π)) & β’ (π = πΈ β (π β π)) & β’ (π = πΉ β (π β π)) & β’ (π = πΊ β (π β π)) & β’ (β = π» β (π β π)) & β’ (π₯ = π β π = π) & β’ π = {β¨π, πβ© β£ βπ₯ β π βπ β π βπ β π βπ β π βπ β π βπ β π βπ β π βπ β π ββ β π (π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π, πβ©, β¨π, ββ©β© β§ π)} β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π β§ πΈ β π) β§ (πΉ β π β§ πΊ β π β§ π» β π)) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©π β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β π)) | ||
Theorem | br6 34727* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
β’ (π = π΄ β (π β π)) & β’ (π = π΅ β (π β π)) & β’ (π = πΆ β (π β π)) & β’ (π = π· β (π β π)) & β’ (π = πΈ β (π β π)) & β’ (π = πΉ β (π β π)) & β’ (π₯ = π β π = π) & β’ π = {β¨π, πβ© β£ βπ₯ β π βπ β π βπ β π βπ β π βπ β π βπ β π βπ β π (π = β¨π, β¨π, πβ©β© β§ π = β¨π, β¨π, πβ©β© β§ π)} β β’ ((π β π β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π· β π β§ πΈ β π β§ πΉ β π)) β (β¨π΄, β¨π΅, πΆβ©β©π β¨π·, β¨πΈ, πΉβ©β© β π)) | ||
Theorem | br4 34728* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
β’ (π = π΄ β (π β π)) & β’ (π = π΅ β (π β π)) & β’ (π = πΆ β (π β π)) & β’ (π = π· β (π β π)) & β’ (π₯ = π β π = π) & β’ π = {β¨π, πβ© β£ βπ₯ β π βπ β π βπ β π βπ β π βπ β π (π = β¨π, πβ© β§ π = β¨π, πβ© β§ π)} β β’ ((π β π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (β¨π΄, π΅β©π β¨πΆ, π·β© β π)) | ||
Theorem | cnvco1 34729 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
β’ β‘(β‘π΄ β π΅) = (β‘π΅ β π΄) | ||
Theorem | cnvco2 34730 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
β’ β‘(π΄ β β‘π΅) = (π΅ β β‘π΄) | ||
Theorem | eldm3 34731 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
β’ (π΄ β dom π΅ β (π΅ βΎ {π΄}) β β ) | ||
Theorem | elrn3 34732 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
β’ (π΄ β ran π΅ β (π΅ β© (V Γ {π΄})) β β ) | ||
Theorem | pocnv 34733 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π Po π΄ β β‘π Po π΄) | ||
Theorem | socnv 34734 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π Or π΄ β β‘π Or π΄) | ||
Theorem | sotrd 34735 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ (π β π Or π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β ππ π) & β’ (π β ππ π) β β’ (π β ππ π) | ||
Theorem | elintfv 34736* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ π β V β β’ ((πΉ Fn π΄ β§ π΅ β π΄) β (π β β© (πΉ β π΅) β βπ¦ β π΅ π β (πΉβπ¦))) | ||
Theorem | funpsstri 34737 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
β’ ((Fun π» β§ (πΉ β π» β§ πΊ β π») β§ (dom πΉ β dom πΊ β¨ dom πΊ β dom πΉ)) β (πΉ β πΊ β¨ πΉ = πΊ β¨ πΊ β πΉ)) | ||
Theorem | fundmpss 34738 | If a class πΉ is a proper subset of a function πΊ, then dom πΉ β dom πΊ. (Contributed by Scott Fenton, 20-Apr-2011.) |
β’ (Fun πΊ β (πΉ β πΊ β dom πΉ β dom πΊ)) | ||
Theorem | funsseq 34739 | Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
β’ ((Fun πΉ β§ Fun πΊ β§ dom πΉ = dom πΊ) β (πΉ = πΊ β πΉ β πΊ)) | ||
Theorem | fununiq 34740 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (Fun πΉ β ((π΄πΉπ΅ β§ π΄πΉπΆ) β π΅ = πΆ)) | ||
Theorem | funbreq 34741 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ ((Fun πΉ β§ π΄πΉπ΅) β (π΄πΉπΆ β π΅ = πΆ)) | ||
Theorem | br1steq 34742 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
β’ π΄ β V & β’ π΅ β V β β’ (β¨π΄, π΅β©1st πΆ β πΆ = π΄) | ||
Theorem | br2ndeq 34743 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
β’ π΄ β V & β’ π΅ β V β β’ (β¨π΄, π΅β©2nd πΆ β πΆ = π΅) | ||
Theorem | dfdm5 34744 | Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ dom π΄ = ((1st βΎ (V Γ V)) β π΄) | ||
Theorem | dfrn5 34745 | Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ ran π΄ = ((2nd βΎ (V Γ V)) β π΄) | ||
Theorem | opelco3 34746 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
β’ (β¨π΄, π΅β© β (πΆ β π·) β π΅ β (πΆ β (π· β {π΄}))) | ||
Theorem | elima4 34747 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
β’ (π΄ β (π β π΅) β (π β© (π΅ Γ {π΄})) β β ) | ||
Theorem | fv1stcnv 34748 | The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
β’ ((π β π΄ β§ π β π) β (β‘(1st βΎ (π΄ Γ {π}))βπ) = β¨π, πβ©) | ||
Theorem | fv2ndcnv 34749 | The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
β’ ((π β π β§ π β π΄) β (β‘(2nd βΎ ({π} Γ π΄))βπ) = β¨π, πβ©) | ||
Theorem | setinds 34750* | Principle of set induction (or E-induction). If a property passes from all elements of π₯ to π₯ itself, then it holds for all π₯. (Contributed by Scott Fenton, 10-Mar-2011.) |
β’ (βπ¦ β π₯ [π¦ / π₯]π β π) β β’ π | ||
Theorem | setinds2f 34751* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π & β’ (π₯ = π¦ β (π β π)) & β’ (βπ¦ β π₯ π β π) β β’ π | ||
Theorem | setinds2 34752* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) |
β’ (π₯ = π¦ β (π β π)) & β’ (βπ¦ β π₯ π β π) β β’ π | ||
Theorem | elpotr 34753* | A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.) |
β’ (βπ§ β π΄ Tr π§ β E Po π΄) | ||
Theorem | dford5reg 34754 | Given ax-reg 9587, an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011.) |
β’ (Ord π΄ β (Tr π΄ β§ E Or π΄)) | ||
Theorem | dfon2lem1 34755 | Lemma for dfon2 34764. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ Tr βͺ {π₯ β£ (π β§ Tr π₯ β§ π)} | ||
Theorem | dfon2lem2 34756* | Lemma for dfon2 34764. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ βͺ {π₯ β£ (π₯ β π΄ β§ π β§ π)} β π΄ | ||
Theorem | dfon2lem3 34757* | Lemma for dfon2 34764. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ (π΄ β π β (βπ₯((π₯ β π΄ β§ Tr π₯) β π₯ β π΄) β (Tr π΄ β§ βπ§ β π΄ Β¬ π§ β π§))) | ||
Theorem | dfon2lem4 34758* | Lemma for dfon2 34764. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ π΄ β V & β’ π΅ β V β β’ ((βπ₯((π₯ β π΄ β§ Tr π₯) β π₯ β π΄) β§ βπ¦((π¦ β π΅ β§ Tr π¦) β π¦ β π΅)) β (π΄ β π΅ β¨ π΅ β π΄)) | ||
Theorem | dfon2lem5 34759* | Lemma for dfon2 34764. Two sets satisfying the new definition also satisfy trichotomy with respect to β. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ π΄ β V & β’ π΅ β V β β’ ((βπ₯((π₯ β π΄ β§ Tr π₯) β π₯ β π΄) β§ βπ¦((π¦ β π΅ β§ Tr π¦) β π¦ β π΅)) β (π΄ β π΅ β¨ π΄ = π΅ β¨ π΅ β π΄)) | ||
Theorem | dfon2lem6 34760* | Lemma for dfon2 34764. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ ((Tr π β§ βπ₯ β π βπ§((π§ β π₯ β§ Tr π§) β π§ β π₯)) β βπ¦((π¦ β π β§ Tr π¦) β π¦ β π)) | ||
Theorem | dfon2lem7 34761* | Lemma for dfon2 34764. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ π΄ β V β β’ (βπ₯((π₯ β π΄ β§ Tr π₯) β π₯ β π΄) β (π΅ β π΄ β βπ¦((π¦ β π΅ β§ Tr π¦) β π¦ β π΅))) | ||
Theorem | dfon2lem8 34762* | Lemma for dfon2 34764. The intersection of a nonempty class π΄ of new ordinals is itself a new ordinal and is contained within π΄ (Contributed by Scott Fenton, 26-Feb-2011.) |
β’ ((π΄ β β β§ βπ₯ β π΄ βπ¦((π¦ β π₯ β§ Tr π¦) β π¦ β π₯)) β (βπ§((π§ β β© π΄ β§ Tr π§) β π§ β β© π΄) β§ β© π΄ β π΄)) | ||
Theorem | dfon2lem9 34763* | Lemma for dfon2 34764. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.) |
β’ (βπ₯ β π΄ βπ¦((π¦ β π₯ β§ Tr π¦) β π¦ β π₯) β E Fr π΄) | ||
Theorem | dfon2 34764* | On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.) |
β’ On = {π₯ β£ βπ¦((π¦ β π₯ β§ Tr π¦) β π¦ β π₯)} | ||
Theorem | rdgprc0 34765 | The value of the recursive definition generator at β when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (Β¬ πΌ β V β (rec(πΉ, πΌ)ββ ) = β ) | ||
Theorem | rdgprc 34766 | The value of the recursive definition generator when πΌ is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (Β¬ πΌ β V β rec(πΉ, πΌ) = rec(πΉ, β )) | ||
Theorem | dfrdg2 34767* | Alternate definition of the recursive function generator when πΌ is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (πΌ β π β rec(πΉ, πΌ) = βͺ {π β£ βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = if(π¦ = β , πΌ, if(Lim π¦, βͺ (π β π¦), (πΉβ(πββͺ π¦)))))}) | ||
Theorem | dfrdg3 34768* | Generalization of dfrdg2 34767 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ rec(πΉ, πΌ) = βͺ {π β£ βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = if(π¦ = β , if(πΌ β V, πΌ, β ), if(Lim π¦, βͺ (π β π¦), (πΉβ(πββͺ π¦)))))} | ||
Theorem | axextdfeq 34769 | A version of ax-ext 2704 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ βπ§((π§ β π₯ β π§ β π¦) β ((π§ β π¦ β π§ β π₯) β (π₯ β π€ β π¦ β π€))) | ||
Theorem | ax8dfeq 34770 | A version of ax-8 2109 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ βπ§((π§ β π₯ β π§ β π¦) β (π€ β π₯ β π€ β π¦)) | ||
Theorem | axextdist 34771 | ax-ext 2704 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ ((Β¬ βπ§ π§ = π₯ β§ Β¬ βπ§ π§ = π¦) β (βπ§(π§ β π₯ β π§ β π¦) β π₯ = π¦)) | ||
Theorem | axextbdist 34772 | axextb 2707 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ ((Β¬ βπ§ π§ = π₯ β§ Β¬ βπ§ π§ = π¦) β (π₯ = π¦ β βπ§(π§ β π₯ β π§ β π¦))) | ||
Theorem | 19.12b 34773* | Version of 19.12vv 2344 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ β²π¦π & β’ β²π₯π β β’ (βπ₯βπ¦(π β π) β βπ¦βπ₯(π β π)) | ||
Theorem | exnel 34774 | There is always a set not in π¦. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ βπ₯ Β¬ π₯ β π¦ | ||
Theorem | distel 34775 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5438 and elirrv 9591.) (Contributed by Scott Fenton, 15-Dec-2010.) |
β’ (Β¬ βπ¦ π¦ = π₯ β Β¬ βπ¦ Β¬ π₯ β π¦) | ||
Theorem | axextndbi 34776 | axextnd 10586 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
β’ βπ§(π₯ = π¦ β (π§ β π₯ β π§ β π¦)) | ||
Theorem | hbntg 34777 | A more general form of hbnt 2291. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (βπ₯(π β βπ₯π) β (Β¬ π β βπ₯ Β¬ π)) | ||
Theorem | hbimtg 34778 | A more general and closed form of hbim 2296. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ ((βπ₯(π β βπ₯π) β§ (π β βπ₯π)) β ((π β π) β βπ₯(π β π))) | ||
Theorem | hbaltg 34779 | A more general and closed form of hbal 2168. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (βπ₯(π β βπ¦π) β (βπ₯π β βπ¦βπ₯π)) | ||
Theorem | hbng 34780 | A more general form of hbn 2292. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (π β βπ₯π) β β’ (Β¬ π β βπ₯ Β¬ π) | ||
Theorem | hbimg 34781 | A more general form of hbim 2296. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (π β βπ₯π) & β’ (π β βπ₯π) β β’ ((π β π) β βπ₯(π β π)) | ||
Syntax | cwsuc 34782 | Declare the syntax for well-founded successor. |
class wsuc(π , π΄, π) | ||
Syntax | cwlim 34783 | Declare the syntax for well-founded limit class. |
class WLim(π , π΄) | ||
Definition | df-wsuc 34784 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ wsuc(π , π΄, π) = inf(Pred(β‘π , π΄, π), π΄, π ) | ||
Definition | df-wlim 34785* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ WLim(π , π΄) = {π₯ β π΄ β£ (π₯ β inf(π΄, π΄, π ) β§ π₯ = sup(Pred(π , π΄, π₯), π΄, π ))} | ||
Theorem | wsuceq123 34786 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ ((π = π β§ π΄ = π΅ β§ π = π) β wsuc(π , π΄, π) = wsuc(π, π΅, π)) | ||
Theorem | wsuceq1 34787 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β wsuc(π , π΄, π) = wsuc(π, π΄, π)) | ||
Theorem | wsuceq2 34788 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π΄ = π΅ β wsuc(π , π΄, π) = wsuc(π , π΅, π)) | ||
Theorem | wsuceq3 34789 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β wsuc(π , π΄, π) = wsuc(π , π΄, π)) | ||
Theorem | nfwsuc 34790 | Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π β β’ β²π₯wsuc(π , π΄, π) | ||
Theorem | wlimeq12 34791 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ ((π = π β§ π΄ = π΅) β WLim(π , π΄) = WLim(π, π΅)) | ||
Theorem | wlimeq1 34792 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
β’ (π = π β WLim(π , π΄) = WLim(π, π΄)) | ||
Theorem | wlimeq2 34793 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
β’ (π΄ = π΅ β WLim(π , π΄) = WLim(π , π΅)) | ||
Theorem | nfwlim 34794 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ β²π₯π & β’ β²π₯π΄ β β’ β²π₯WLim(π , π΄) | ||
Theorem | elwlim 34795 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ (π β WLim(π , π΄) β (π β π΄ β§ π β inf(π΄, π΄, π ) β§ π = sup(Pred(π , π΄, π), π΄, π ))) | ||
Theorem | wzel 34796 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ ((π We π΄ β§ π Se π΄ β§ π΄ β β ) β inf(π΄, π΄, π ) β π΄) | ||
Theorem | wsuclem 34797* | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) & β’ (π β βπ€ β π΄ ππ π€) β β’ (π β βπ₯ β π΄ (βπ¦ β Pred (β‘π , π΄, π) Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β Pred (β‘π , π΄, π)π§π π¦))) | ||
Theorem | wsucex 34798 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ (π β π Or π΄) β β’ (π β wsuc(π , π΄, π) β V) | ||
Theorem | wsuccl 34799* | If π is a set with an π successor in π΄, then its well-founded successor is a member of π΄. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) & β’ (π β βπ¦ β π΄ ππ π¦) β β’ (π β wsuc(π , π΄, π) β π΄) | ||
Theorem | wsuclb 34800 | A well-founded successor is a lower bound on points after π. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β ππ π) β β’ (π β Β¬ ππ wsuc(π , π΄, π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |