![]() |
Metamath
Proof Explorer Theorem List (p. 353 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: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | funimage 35201 | Imageπ΄ is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun Imageπ΄ | ||
Theorem | fnimage 35202* | Imageπ is a function over the set-like portion of π . (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Imageπ Fn {π₯ β£ (π β π₯) β V} | ||
Theorem | imageval 35203* | The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Imageπ = (π₯ β V β¦ (π β π₯)) | ||
Theorem | fvimage 35204 | Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β π β§ (π β π΄) β π) β (Imageπ βπ΄) = (π β π΄)) | ||
Theorem | brcart 35205 | Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (β¨π΄, π΅β©CartπΆ β πΆ = (π΄ Γ π΅)) | ||
Theorem | brdomain 35206 | Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄Domainπ΅ β π΅ = dom π΄) | ||
Theorem | brrange 35207 | Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄Rangeπ΅ β π΅ = ran π΄) | ||
Theorem | brdomaing 35208 | Closed form of brdomain 35206. (Contributed by Scott Fenton, 2-May-2014.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄Domainπ΅ β π΅ = dom π΄)) | ||
Theorem | brrangeg 35209 | Closed form of brrange 35207. (Contributed by Scott Fenton, 3-May-2014.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄Rangeπ΅ β π΅ = ran π΄)) | ||
Theorem | brimg 35210 | Binary relation form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (β¨π΄, π΅β©ImgπΆ β πΆ = (π΄ β π΅)) | ||
Theorem | brapply 35211 | Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (β¨π΄, π΅β©ApplyπΆ β πΆ = (π΄βπ΅)) | ||
Theorem | brcup 35212 | Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (β¨π΄, π΅β©CupπΆ β πΆ = (π΄ βͺ π΅)) | ||
Theorem | brcap 35213 | Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (β¨π΄, π΅β©CapπΆ β πΆ = (π΄ β© π΅)) | ||
Theorem | brsuccf 35214 | Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄Succπ΅ β π΅ = suc π΄) | ||
Theorem | funpartlem 35215* | Lemma for funpartfun 35216. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
β’ (π΄ β dom ((ImageπΉ β Singleton) β© (V Γ Singletons )) β βπ₯(πΉ β {π΄}) = {π₯}) | ||
Theorem | funpartfun 35216 | The functional part of πΉ is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ Fun FunpartπΉ | ||
Theorem | funpartss 35217 | The functional part of πΉ is a subset of πΉ. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ FunpartπΉ β πΉ | ||
Theorem | funpartfv 35218 | The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (FunpartπΉβπ΄) = (πΉβπ΄) | ||
Theorem | fullfunfnv 35219 | The full functional part of πΉ is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ FullFunπΉ Fn V | ||
Theorem | fullfunfv 35220 | The function value of the full function of πΉ agrees with πΉ. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (FullFunπΉβπ΄) = (πΉβπ΄) | ||
Theorem | brfullfun 35221 | A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄FullFunπΉπ΅ β π΅ = (πΉβπ΄)) | ||
Theorem | brrestrict 35222 | Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V & β’ πΆ β V β β’ (β¨π΄, π΅β©RestrictπΆ β πΆ = (π΄ βΎ π΅)) | ||
Theorem | dfrecs2 35223 | A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.) |
β’ recs(πΉ) = βͺ (( Funs β© (β‘Domain β On)) β dom ((β‘ E β Domain) β Fix (β‘Apply β (FullFunπΉ β Restrict)))) | ||
Theorem | dfrdg4 35224 | A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ rec(πΉ, π΄) = βͺ (( Funs β© (β‘Domain β On)) β dom ((β‘ E β Domain) β Fix (β‘Apply β (((V Γ {β }) Γ {βͺ {π΄}}) βͺ ((( Bigcup β Img) βΎ (V Γ Limits )) βͺ ((FullFunπΉ β (Apply β pprod( I , Bigcup ))) βΎ (V Γ ran Succ))))))) | ||
Theorem | dfint3 35225 | Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.) |
β’ β© π΄ = (V β (β‘(V β E ) β π΄)) | ||
Theorem | imagesset 35226 | The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.) |
β’ Imageβ‘ SSet β SSet | ||
Theorem | brub 35227* | Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
β’ π β V & β’ π΄ β V β β’ (πUBπ π΄ β βπ₯ β π π₯π π΄) | ||
Theorem | brlb 35228* | Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
β’ π β V & β’ π΄ β V β β’ (πLBπ π΄ β βπ₯ β π π΄π π₯) | ||
Syntax | caltop 35229 | Declare the syntax for an alternate ordered pair. |
class βͺπ΄, π΅β« | ||
Syntax | caltxp 35230 | Declare the syntax for an alternate Cartesian product. |
class (π΄ ΓΓ π΅) | ||
Definition | df-altop 35231 | An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 35242), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ βͺπ΄, π΅β« = {{π΄}, {π΄, {π΅}}} | ||
Definition | df-altxp 35232* | Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.) |
β’ (π΄ ΓΓ π΅) = {π§ β£ βπ₯ β π΄ βπ¦ β π΅ π§ = βͺπ₯, π¦β«} | ||
Theorem | altopex 35233 | Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ βͺπ΄, π΅β« β V | ||
Theorem | altopthsn 35234 | Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.) |
β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β ({π΄} = {πΆ} β§ {π΅} = {π·})) | ||
Theorem | altopeq12 35235 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β βͺπ΄, πΆβ« = βͺπ΅, π·β«) | ||
Theorem | altopeq1 35236 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (π΄ = π΅ β βͺπ΄, πΆβ« = βͺπ΅, πΆβ«) | ||
Theorem | altopeq2 35237 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (π΄ = π΅ β βͺπΆ, π΄β« = βͺπΆ, π΅β«) | ||
Theorem | altopth1 35238 | Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (π΄ β π β (βͺπ΄, π΅β« = βͺπΆ, π·β« β π΄ = πΆ)) | ||
Theorem | altopth2 35239 | Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (π΅ β π β (βͺπ΄, π΅β« = βͺπΆ, π·β« β π΅ = π·)) | ||
Theorem | altopthg 35240 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ ((π΄ β π β§ π΅ β π) β (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | altopthbg 35241 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ ((π΄ β π β§ π· β π) β (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | altopth 35242 | The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that πΆ and π· are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 5477), requires π· to be a set. (Contributed by Scott Fenton, 23-Mar-2012.) |
β’ π΄ β V & β’ π΅ β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altopthb 35243 | Alternate ordered pair theorem with different sethood requirements. See altopth 35242 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ π΄ β V & β’ π· β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altopthc 35244 | Alternate ordered pair theorem with different sethood requirements. See altopth 35242 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ π΅ β V & β’ πΆ β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altopthd 35245 | Alternate ordered pair theorem with different sethood requirements. See altopth 35242 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ πΆ β V & β’ π· β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altxpeq1 35246 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ (π΄ = π΅ β (π΄ ΓΓ πΆ) = (π΅ ΓΓ πΆ)) | ||
Theorem | altxpeq2 35247 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ (π΄ = π΅ β (πΆ ΓΓ π΄) = (πΆ ΓΓ π΅)) | ||
Theorem | elaltxp 35248* | Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.) |
β’ (π β (π΄ ΓΓ π΅) β βπ₯ β π΄ βπ¦ β π΅ π = βͺπ₯, π¦β«) | ||
Theorem | altopelaltxp 35249 | Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5713, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (βͺπ, πβ« β (π΄ ΓΓ π΅) β (π β π΄ β§ π β π΅)) | ||
Theorem | altxpsspw 35250 | An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ (π΄ ΓΓ π΅) β π« π« (π΄ βͺ π« π΅) | ||
Theorem | altxpexg 35251 | The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ ΓΓ π΅) β V) | ||
Theorem | rankaltopb 35252 | Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β βͺ (π 1 β On) β§ π΅ β βͺ (π 1 β On)) β (rankββͺπ΄, π΅β«) = suc suc ((rankβπ΄) βͺ suc (rankβπ΅))) | ||
Theorem | nfaltop 35253 | Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯βͺπ΄, π΅β« | ||
Theorem | sbcaltop 35254* | Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
β’ (π΄ β V β β¦π΄ / π₯β¦βͺπΆ, π·β« = βͺβ¦π΄ / π₯β¦πΆ, β¦π΄ / π₯β¦π·β«) | ||
Syntax | cofs 35255 | Declare the syntax for the outer five segment configuration. |
class OuterFiveSeg | ||
Definition | df-ofs 35256* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 28460). See brofs 35278 and 5segofs 35279 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
β’ OuterFiveSeg = {β¨π, πβ© β£ βπ β β βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ β (πΌβπ)βπ₯ β (πΌβπ)βπ¦ β (πΌβπ)βπ§ β (πΌβπ)βπ€ β (πΌβπ)(π = β¨β¨π, πβ©, β¨π, πβ©β© β§ π = β¨β¨π₯, π¦β©, β¨π§, π€β©β© β§ ((π Btwn β¨π, πβ© β§ π¦ Btwn β¨π₯, π§β©) β§ (β¨π, πβ©Cgrβ¨π₯, π¦β© β§ β¨π, πβ©Cgrβ¨π¦, π§β©) β§ (β¨π, πβ©Cgrβ¨π₯, π€β© β§ β¨π, πβ©Cgrβ¨π¦, π€β©)))} | ||
Theorem | cgrrflx2d 35257 | Deduction form of axcgrrflx 28436. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) β β’ (π β β¨π΄, π΅β©Cgrβ¨π΅, π΄β©) | ||
Theorem | cgrtr4d 35258 | Deduction form of axcgrtr 28437. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ (π β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) & β’ (π β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) β β’ (π β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) | ||
Theorem | cgrtr4and 35259 | Deduction form of axcgrtr 28437. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) | ||
Theorem | cgrrflx 35260 | Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β©Cgrβ¨π΄, π΅β©) | ||
Theorem | cgrrflxd 35261 | Deduction form of cgrrflx 35260. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) β β’ (π β β¨π΄, π΅β©Cgrβ¨π΄, π΅β©) | ||
Theorem | cgrcomim 35262 | Congruence commutes on the two sides. Implication version. Theorem 2.2 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨πΆ, π·β©Cgrβ¨π΄, π΅β©)) | ||
Theorem | cgrcom 35263 | Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨πΆ, π·β©Cgrβ¨π΄, π΅β©)) | ||
Theorem | cgrcomand 35264 | Deduction form of cgrcom 35263. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨π΄, π΅β©) | ||
Theorem | cgrtr 35265 | Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©)) | ||
Theorem | cgrtrand 35266 | Deduction form of cgrtr 35265. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) & β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) | ||
Theorem | cgrtr3 35267 | Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©)) | ||
Theorem | cgrtr3and 35268 | Deduction form of cgrtr3 35267. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) & β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) | ||
Theorem | cgrcoml 35269 | Congruence commutes on the left. Biconditional version of Theorem 2.4 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨π΅, π΄β©Cgrβ¨πΆ, π·β©)) | ||
Theorem | cgrcomr 35270 | Congruence commutes on the right. Biconditional version of Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨π΄, π΅β©Cgrβ¨π·, πΆβ©)) | ||
Theorem | cgrcomlr 35271 | Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨π΅, π΄β©Cgrβ¨π·, πΆβ©)) | ||
Theorem | cgrcomland 35272 | Deduction form of cgrcoml 35269. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨π΅, π΄β©Cgrβ¨πΆ, π·β©) | ||
Theorem | cgrcomrand 35273 | Deduction form of cgrcoml 35269. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨π·, πΆβ©) | ||
Theorem | cgrcomlrand 35274 | Deduction form of cgrcomlr 35271. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨π΅, π΄β©Cgrβ¨π·, πΆβ©) | ||
Theorem | cgrtriv 35275 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΄β©Cgrβ¨π΅, π΅β©) | ||
Theorem | cgrid2 35276 | Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (β¨π΄, π΄β©Cgrβ¨π΅, πΆβ© β π΅ = πΆ)) | ||
Theorem | cgrdegen 35277 | Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β (π΄ = π΅ β πΆ = π·))) | ||
Theorem | brofs 35278 | Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β ((π΅ Btwn β¨π΄, πΆβ© β§ πΉ Btwn β¨πΈ, πΊβ©) β§ (β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ© β§ β¨π΅, πΆβ©Cgrβ¨πΉ, πΊβ©) β§ (β¨π΄, π·β©Cgrβ¨πΈ, π»β© β§ β¨π΅, π·β©Cgrβ¨πΉ, π»β©)))) | ||
Theorem | 5segofs 35279 | Rephrase ax5seg 28460 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β ((β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β§ π΄ β π΅) β β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)) | ||
Theorem | ofscom 35280 | The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© OuterFiveSeg β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©)) | ||
Theorem | cgrextend 35281 | Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β (((π΅ Btwn β¨π΄, πΆβ© β§ πΈ Btwn β¨π·, πΉβ©) β§ (β¨π΄, π΅β©Cgrβ¨π·, πΈβ© β§ β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©)) β β¨π΄, πΆβ©Cgrβ¨π·, πΉβ©)) | ||
Theorem | cgrextendand 35282 | Deduction form of cgrextend 35281. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β π΅ Btwn β¨π΄, πΆβ©) & β’ ((π β§ π) β πΈ Btwn β¨π·, πΉβ©) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨π·, πΈβ©) & β’ ((π β§ π) β β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨π΄, πΆβ©Cgrβ¨π·, πΉβ©) | ||
Theorem | segconeq 35283 | Two points that satisfy the conclusion of axsegcon 28449 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π β π΄ β§ (π΄ Btwn β¨π, πβ© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ (π΄ Btwn β¨π, πβ© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β π = π)) | ||
Theorem | segconeu 35284* | Existential uniqueness version of segconeq 35283. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β β!π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) | ||
Theorem | btwntriv2 35285 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΅ Btwn β¨π΄, π΅β©) | ||
Theorem | btwncomim 35286 | Betweenness commutes. Implication version. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Btwn β¨π΅, πΆβ© β π΄ Btwn β¨πΆ, π΅β©)) | ||
Theorem | btwncom 35287 | Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Btwn β¨π΅, πΆβ© β π΄ Btwn β¨πΆ, π΅β©)) | ||
Theorem | btwncomand 35288 | Deduction form of btwncom 35287. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ ((π β§ π) β π΄ Btwn β¨π΅, πΆβ©) β β’ ((π β§ π) β π΄ Btwn β¨πΆ, π΅β©) | ||
Theorem | btwntriv1 35289 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Btwn β¨π΄, π΅β©) | ||
Theorem | btwnswapid 35290 | If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π΄ Btwn β¨π΅, πΆβ© β§ π΅ Btwn β¨π΄, πΆβ©) β π΄ = π΅)) | ||
Theorem | btwnswapid2 35291 | If you can swap arguments one and three of a betweenness statement, then those arguments are identical. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π΄ Btwn β¨π΅, πΆβ© β§ πΆ Btwn β¨π΅, π΄β©) β π΄ = πΆ)) | ||
Theorem | btwnintr 35292 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ Btwn β¨π΄, π·β© β§ πΆ Btwn β¨π΅, π·β©) β π΅ Btwn β¨π΄, πΆβ©)) | ||
Theorem | btwnexch3 35293 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ πΆ Btwn β¨π΄, π·β©) β πΆ Btwn β¨π΅, π·β©)) | ||
Theorem | btwnexch3and 35294 | Deduction form of btwnexch3 35293. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β π΅ Btwn β¨π΄, πΆβ©) & β’ ((π β§ π) β πΆ Btwn β¨π΄, π·β©) β β’ ((π β§ π) β πΆ Btwn β¨π΅, π·β©) | ||
Theorem | btwnouttr2 35295 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ β πΆ β§ π΅ Btwn β¨π΄, πΆβ© β§ πΆ Btwn β¨π΅, π·β©) β πΆ Btwn β¨π΄, π·β©)) | ||
Theorem | btwnexch2 35296 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ Btwn β¨π΄, π·β© β§ πΆ Btwn β¨π΅, π·β©) β πΆ Btwn β¨π΄, π·β©)) | ||
Theorem | btwnouttr 35297 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ β πΆ β§ π΅ Btwn β¨π΄, πΆβ© β§ πΆ Btwn β¨π΅, π·β©) β π΅ Btwn β¨π΄, π·β©)) | ||
Theorem | btwnexch 35298 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 24-Sep-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β ((π΅ Btwn β¨π΄, πΆβ© β§ πΆ Btwn β¨π΄, π·β©) β π΅ Btwn β¨π΄, π·β©)) | ||
Theorem | btwnexchand 35299 | Deduction form of btwnexch 35298. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β π΅ Btwn β¨π΄, πΆβ©) & β’ ((π β§ π) β πΆ Btwn β¨π΄, π·β©) β β’ ((π β§ π) β π΅ Btwn β¨π΄, π·β©) | ||
Theorem | btwndiff 35300* | There is always a π distinct from π΅ such that π΅ lies between π΄ and π. Theorem 3.14 of [Schwabhauser] p. 32. (Contributed by Scott Fenton, 24-Sep-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β βπ β (πΌβπ)(π΅ Btwn β¨π΄, πβ© β§ π΅ β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |