Home | Metamath
Proof Explorer Theorem List (p. 342 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bcprod 34101* | A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.) |
β’ (π β β β βπ β (1...(π β 1))((π β 1)Cπ) = βπ β (1...(π β 1))(πβ((2 Β· π) β π))) | ||
Theorem | bccolsum 34102* | A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.) |
β’ ((π β β0 β§ πΆ β β0) β Ξ£π β (0...π)(πCπΆ) = ((π + 1)C(πΆ + 1))) | ||
Theorem | iprodefisumlem 34103 | Lemma for iprodefisum 34104. (Contributed by Scott Fenton, 11-Feb-2018.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) β β’ (π β seqπ( Β· , (exp β πΉ)) = (exp β seqπ( + , πΉ))) | ||
Theorem | iprodefisum 34104* | 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 34105* | An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.) |
β’ (π β π΄ β (β β (β€ β β))) β β’ (π β (Ξβπ΄) = (βπ β β (((1 + (1 / π))βππ΄) / (1 + (π΄ / π))) / π΄)) | ||
Theorem | faclimlem1 34106* | Lemma for faclim 34109. 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 34107* | Lemma for faclim 34109. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.) |
β’ (π β β0 β seq1( Β· , (π β β β¦ (((1 + (π / π)) Β· (1 + (1 / π))) / (1 + ((π + 1) / π))))) β (π + 1)) | ||
Theorem | faclimlem3 34108 | Lemma for faclim 34109. 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 34109* | 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 34110* | An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.) |
β’ (π΄ β β0 β (!βπ΄) = βπ β β (((1 + (1 / π))βπ΄) / (1 + (π΄ / π)))) | ||
Theorem | faclim2 34111* | Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.) |
β’ πΉ = (π β β β¦ (((!βπ) Β· ((π + 1)βπ)) / (!β(π + π)))) β β’ (π β β0 β πΉ β 1) | ||
Theorem | gcd32 34112 | 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 34113 | Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅) gcd π΅) = (π΄ gcd π΅)) | ||
Theorem | dftr6 34114 | A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.) |
β’ π΄ β V β β’ (Tr π΄ β π΄ β (V β ran (( E β E ) β E ))) | ||
Theorem | coep 34115* | Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄( E β π )π΅ β βπ₯ β π΅ π΄π π₯) | ||
Theorem | coepr 34116* | Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄(π β β‘ E )π΅ β βπ₯ β π΄ π₯π π΅) | ||
Theorem | dffr5 34117 | A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.) |
β’ (π Fr π΄ β (π« π΄ β {β }) β ran ( E β ( E β β‘π ))) | ||
Theorem | dfso2 34118 | Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.) |
β’ (π Or π΄ β (π Po π΄ β§ (π΄ Γ π΄) β (π βͺ ( I βͺ β‘π )))) | ||
Theorem | br8 34119* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
β’ (π = π΄ β (π β π)) & β’ (π = π΅ β (π β π)) & β’ (π = πΆ β (π β π)) & β’ (π = π· β (π β π)) & β’ (π = πΈ β (π β π)) & β’ (π = πΉ β (π β π)) & β’ (π = πΊ β (π β π)) & β’ (β = π» β (π β π)) & β’ (π₯ = π β π = π) & β’ π = {β¨π, πβ© β£ βπ₯ β π βπ β π βπ β π βπ β π βπ β π βπ β π βπ β π βπ β π ββ β π (π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π, πβ©, β¨π, ββ©β© β§ π)} β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π β§ πΈ β π) β§ (πΉ β π β§ πΊ β π β§ π» β π)) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©π β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β π)) | ||
Theorem | br6 34120* | Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
β’ (π = π΄ β (π β π)) & β’ (π = π΅ β (π β π)) & β’ (π = πΆ β (π β π)) & β’ (π = π· β (π β π)) & β’ (π = πΈ β (π β π)) & β’ (π = πΉ β (π β π)) & β’ (π₯ = π β π = π) & β’ π = {β¨π, πβ© β£ βπ₯ β π βπ β π βπ β π βπ β π βπ β π βπ β π βπ β π (π = β¨π, β¨π, πβ©β© β§ π = β¨π, β¨π, πβ©β© β§ π)} β β’ ((π β π β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π· β π β§ πΈ β π β§ πΉ β π)) β (β¨π΄, β¨π΅, πΆβ©β©π β¨π·, β¨πΈ, πΉβ©β© β π)) | ||
Theorem | br4 34121* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
β’ (π = π΄ β (π β π)) & β’ (π = π΅ β (π β π)) & β’ (π = πΆ β (π β π)) & β’ (π = π· β (π β π)) & β’ (π₯ = π β π = π) & β’ π = {β¨π, πβ© β£ βπ₯ β π βπ β π βπ β π βπ β π βπ β π (π = β¨π, πβ© β§ π = β¨π, πβ© β§ π)} β β’ ((π β π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (β¨π΄, π΅β©π β¨πΆ, π·β© β π)) | ||
Theorem | cnvco1 34122 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
β’ β‘(β‘π΄ β π΅) = (β‘π΅ β π΄) | ||
Theorem | cnvco2 34123 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
β’ β‘(π΄ β β‘π΅) = (π΅ β β‘π΄) | ||
Theorem | eldm3 34124 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
β’ (π΄ β dom π΅ β (π΅ βΎ {π΄}) β β ) | ||
Theorem | elrn3 34125 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
β’ (π΄ β ran π΅ β (π΅ β© (V Γ {π΄})) β β ) | ||
Theorem | pocnv 34126 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π Po π΄ β β‘π Po π΄) | ||
Theorem | socnv 34127 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π Or π΄ β β‘π Or π΄) | ||
Theorem | sotrd 34128 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
β’ (π β π Or π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β ππ π) & β’ (π β ππ π) β β’ (π β ππ π) | ||
Theorem | elintfv 34129* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
β’ π β V β β’ ((πΉ Fn π΄ β§ π΅ β π΄) β (π β β© (πΉ β π΅) β βπ¦ β π΅ π β (πΉβπ¦))) | ||
Theorem | funpsstri 34130 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
β’ ((Fun π» β§ (πΉ β π» β§ πΊ β π») β§ (dom πΉ β dom πΊ β¨ dom πΊ β dom πΉ)) β (πΉ β πΊ β¨ πΉ = πΊ β¨ πΊ β πΉ)) | ||
Theorem | fundmpss 34131 | 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 34132 | 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 34133 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (Fun πΉ β ((π΄πΉπ΅ β§ π΄πΉπΆ) β π΅ = πΆ)) | ||
Theorem | funbreq 34134 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ ((Fun πΉ β§ π΄πΉπ΅) β (π΄πΉπΆ β π΅ = πΆ)) | ||
Theorem | br1steq 34135 | 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 34136 | 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 34137 | 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 34138 | 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 34139 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
β’ (β¨π΄, π΅β© β (πΆ β π·) β π΅ β (πΆ β (π· β {π΄}))) | ||
Theorem | elima4 34140 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
β’ (π΄ β (π β π΅) β (π β© (π΅ Γ {π΄})) β β ) | ||
Theorem | fv1stcnv 34141 | The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
β’ ((π β π΄ β§ π β π) β (β‘(1st βΎ (π΄ Γ {π}))βπ) = β¨π, πβ©) | ||
Theorem | fv2ndcnv 34142 | The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
β’ ((π β π β§ π β π΄) β (β‘(2nd βΎ ({π} Γ π΄))βπ) = β¨π, πβ©) | ||
Theorem | setinds 34143* | 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 34144* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π & β’ (π₯ = π¦ β (π β π)) & β’ (βπ¦ β π₯ π β π) β β’ π | ||
Theorem | setinds2 34145* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) |
β’ (π₯ = π¦ β (π β π)) & β’ (βπ¦ β π₯ π β π) β β’ π | ||
Theorem | elpotr 34146* | A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.) |
β’ (βπ§ β π΄ Tr π§ β E Po π΄) | ||
Theorem | dford5reg 34147 | Given ax-reg 9461, 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 34148 | Lemma for dfon2 34157. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ Tr βͺ {π₯ β£ (π β§ Tr π₯ β§ π)} | ||
Theorem | dfon2lem2 34149* | Lemma for dfon2 34157. (Contributed by Scott Fenton, 28-Feb-2011.) |
β’ βͺ {π₯ β£ (π₯ β π΄ β§ π β§ π)} β π΄ | ||
Theorem | dfon2lem3 34150* | Lemma for dfon2 34157. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ (π΄ β π β (βπ₯((π₯ β π΄ β§ Tr π₯) β π₯ β π΄) β (Tr π΄ β§ βπ§ β π΄ Β¬ π§ β π§))) | ||
Theorem | dfon2lem4 34151* | Lemma for dfon2 34157. 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 34152* | Lemma for dfon2 34157. 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 34153* | Lemma for dfon2 34157. 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 34154* | Lemma for dfon2 34157. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.) |
β’ π΄ β V β β’ (βπ₯((π₯ β π΄ β§ Tr π₯) β π₯ β π΄) β (π΅ β π΄ β βπ¦((π¦ β π΅ β§ Tr π¦) β π¦ β π΅))) | ||
Theorem | dfon2lem8 34155* | Lemma for dfon2 34157. 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 34156* | Lemma for dfon2 34157. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.) |
β’ (βπ₯ β π΄ βπ¦((π¦ β π₯ β§ Tr π¦) β π¦ β π₯) β E Fr π΄) | ||
Theorem | dfon2 34157* | 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 34158 | 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 34159 | 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 34160* | 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 34161* | Generalization of dfrdg2 34160 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 34162 | A version of ax-ext 2708 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ βπ§((π§ β π₯ β π§ β π¦) β ((π§ β π¦ β π§ β π₯) β (π₯ β π€ β π¦ β π€))) | ||
Theorem | ax8dfeq 34163 | A version of ax-8 2108 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
β’ βπ§((π§ β π₯ β π§ β π¦) β (π€ β π₯ β π€ β π¦)) | ||
Theorem | axextdist 34164 | ax-ext 2708 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ ((Β¬ βπ§ π§ = π₯ β§ Β¬ βπ§ π§ = π¦) β (βπ§(π§ β π₯ β π§ β π¦) β π₯ = π¦)) | ||
Theorem | axextbdist 34165 | axextb 2711 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ ((Β¬ βπ§ π§ = π₯ β§ Β¬ βπ§ π§ = π¦) β (π₯ = π¦ β βπ§(π§ β π₯ β π§ β π¦))) | ||
Theorem | 19.12b 34166* | 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 34167 | There is always a set not in π¦. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ βπ₯ Β¬ π₯ β π¦ | ||
Theorem | distel 34168 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5392 and elirrv 9465.) (Contributed by Scott Fenton, 15-Dec-2010.) |
β’ (Β¬ βπ¦ π¦ = π₯ β Β¬ βπ¦ Β¬ π₯ β π¦) | ||
Theorem | axextndbi 34169 | axextnd 10460 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
β’ βπ§(π₯ = π¦ β (π§ β π₯ β π§ β π¦)) | ||
Theorem | hbntg 34170 | A more general form of hbnt 2291. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (βπ₯(π β βπ₯π) β (Β¬ π β βπ₯ Β¬ π)) | ||
Theorem | hbimtg 34171 | A more general and closed form of hbim 2296. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ ((βπ₯(π β βπ₯π) β§ (π β βπ₯π)) β ((π β π) β βπ₯(π β π))) | ||
Theorem | hbaltg 34172 | A more general and closed form of hbal 2167. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (βπ₯(π β βπ¦π) β (βπ₯π β βπ¦βπ₯π)) | ||
Theorem | hbng 34173 | A more general form of hbn 2292. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (π β βπ₯π) β β’ (Β¬ π β βπ₯ Β¬ π) | ||
Theorem | hbimg 34174 | A more general form of hbim 2296. (Contributed by Scott Fenton, 13-Dec-2010.) |
β’ (π β βπ₯π) & β’ (π β βπ₯π) β β’ ((π β π) β βπ₯(π β π)) | ||
Theorem | frpoins3xpg 34175* | Special case of founded partial induction over a cross product. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ ((π₯ β π΄ β§ π¦ β π΅) β (βπ§βπ€(β¨π§, π€β© β Pred(π , (π΄ Γ π΅), β¨π₯, π¦β©) β π) β π)) & β’ (π₯ = π§ β (π β π)) & β’ (π¦ = π€ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π¦ = π β (π β π)) β β’ (((π Fr (π΄ Γ π΅) β§ π Po (π΄ Γ π΅) β§ π Se (π΄ Γ π΅)) β§ (π β π΄ β§ π β π΅)) β π) | ||
Theorem | frpoins3xp3g 34176* | Special case of founded partial recursion over a triple cross product. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ ((π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ) β (βπ€βπ‘βπ’(β¨β¨π€, π‘β©, π’β© β Pred(π , ((π΄ Γ π΅) Γ πΆ), β¨β¨π₯, π¦β©, π§β©) β π) β π)) & β’ (π₯ = π€ β (π β π)) & β’ (π¦ = π‘ β (π β π)) & β’ (π§ = π’ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π¦ = π β (π β π)) & β’ (π§ = π β (π β π)) β β’ (((π Fr ((π΄ Γ π΅) Γ πΆ) β§ π Po ((π΄ Γ π΅) Γ πΆ) β§ π Se ((π΄ Γ π΅) Γ πΆ)) β§ (π β π΄ β§ π β π΅ β§ π β πΆ)) β π) | ||
Theorem | xpord2lem 34177* | Lemma for cross product ordering. Calculate the value of the cross product relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ (β¨π, πβ©πβ¨π, πβ© β ((π β π΄ β§ π β π΅) β§ (π β π΄ β§ π β π΅) β§ ((ππ π β¨ π = π) β§ (πππ β¨ π = π) β§ (π β π β¨ π β π)))) | ||
Theorem | poxp2 34178* | Another way of partially ordering a cross product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ (π β π Po π΄) & β’ (π β π Po π΅) β β’ (π β π Po (π΄ Γ π΅)) | ||
Theorem | frxp2 34179* | Another way of giving a founded order to a cross product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ (π β π Fr π΄) & β’ (π β π Fr π΅) β β’ (π β π Fr (π΄ Γ π΅)) | ||
Theorem | xpord2pred 34180* | Calculate the predecessor class in frxp2 34179. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ ((π β π΄ β§ π β π΅) β Pred(π, (π΄ Γ π΅), β¨π, πβ©) = (((Pred(π , π΄, π) βͺ {π}) Γ (Pred(π, π΅, π) βͺ {π})) β {β¨π, πβ©})) | ||
Theorem | sexp2 34181* | Condition for the relationship in frxp2 34179 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ (π β π Se π΄) & β’ (π β π Se π΅) β β’ (π β π Se (π΄ Γ π΅)) | ||
Theorem | xpord2ind 34182* | Induction over the cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ π Fr π΄ & β’ π Po π΄ & β’ π Se π΄ & β’ π Fr π΅ & β’ π Po π΅ & β’ π Se π΅ & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β π΄ β§ π β π΅) β ((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)π) β π)) β β’ ((π β π΄ β§ π β π΅) β π) | ||
Theorem | xpord3lem 34183* | Lemma for triple ordering. Calculate the value of the relationship. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} β β’ (β¨β¨π, πβ©, πβ©πβ¨β¨π, πβ©, πβ© β ((π β π΄ β§ π β π΅ β§ π β πΆ) β§ (π β π΄ β§ π β π΅ β§ π β πΆ) β§ (((ππ π β¨ π = π) β§ (πππ β¨ π = π) β§ (πππ β¨ π = π)) β§ (π β π β¨ π β π β¨ π β π)))) | ||
Theorem | poxp3 34184* | Triple cross product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π Po π΄) & β’ (π β π Po π΅) & β’ (π β π Po πΆ) β β’ (π β π Po ((π΄ Γ π΅) Γ πΆ)) | ||
Theorem | frxp3 34185* | Give foundedness over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π Fr π΄) & β’ (π β π Fr π΅) & β’ (π β π Fr πΆ) β β’ (π β π Fr ((π΄ Γ π΅) Γ πΆ)) | ||
Theorem | xpord3pred 34186* | Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} β β’ ((π β π΄ β§ π β π΅ β§ π β πΆ) β Pred(π, ((π΄ Γ π΅) Γ πΆ), β¨β¨π, πβ©, πβ©) = ((((Pred(π , π΄, π) βͺ {π}) Γ (Pred(π, π΅, π) βͺ {π})) Γ (Pred(π, πΆ, π) βͺ {π})) β {β¨β¨π, πβ©, πβ©})) | ||
Theorem | sexp3 34187* | Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π Se π΄) & β’ (π β π Se π΅) & β’ (π β π Se πΆ) β β’ (π β π Se ((π΄ Γ π΅) Γ πΆ)) | ||
Theorem | xpord3ind 34188* | Induction over the triple cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ π Fr π΄ & β’ π Po π΄ & β’ π Se π΄ & β’ π Fr π΅ & β’ π Po π΅ & β’ π Se π΅ & β’ π Fr πΆ & β’ π Po πΆ & β’ π Se πΆ & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β π΄ β§ π β π΅ β§ π β πΆ) β (((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, πΆ, π)π) β§ (βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π, π΅, π)π) β§ βπ β Pred (π, πΆ, π)π) β π)) β β’ ((π β π΄ β§ π β π΅ β§ π β πΆ) β π) | ||
Syntax | cwsuc 34189 | Declare the syntax for well-founded successor. |
class wsuc(π , π΄, π) | ||
Syntax | cwlim 34190 | Declare the syntax for well-founded limit class. |
class WLim(π , π΄) | ||
Definition | df-wsuc 34191 | 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 34192* | 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 34193 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ ((π = π β§ π΄ = π΅ β§ π = π) β wsuc(π , π΄, π) = wsuc(π, π΅, π)) | ||
Theorem | wsuceq1 34194 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β wsuc(π , π΄, π) = wsuc(π, π΄, π)) | ||
Theorem | wsuceq2 34195 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π΄ = π΅ β wsuc(π , π΄, π) = wsuc(π , π΅, π)) | ||
Theorem | wsuceq3 34196 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β wsuc(π , π΄, π) = wsuc(π , π΄, π)) | ||
Theorem | nfwsuc 34197 | 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 34198 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ ((π = π β§ π΄ = π΅) β WLim(π , π΄) = WLim(π, π΅)) | ||
Theorem | wlimeq1 34199 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
β’ (π = π β WLim(π , π΄) = WLim(π, π΄)) | ||
Theorem | wlimeq2 34200 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
β’ (π΄ = π΅ β WLim(π , π΄) = WLim(π , π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |