Home | Metamath
Proof Explorer Theorem List (p. 345 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 | dfsingles2 34401* | Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Singletons = {π₯ β£ βπ¦ π₯ = {π¦}} | ||
Theorem | snelsingles 34402 | A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.) |
β’ π΄ β V β β’ {π΄} β Singletons | ||
Theorem | dfiota3 34403 | A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.) |
β’ (β©π₯π) = βͺ βͺ ({{π₯ β£ π}} β© Singletons ) | ||
Theorem | dffv5 34404 | Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.) |
β’ (πΉβπ΄) = βͺ βͺ ({(πΉ β {π΄})} β© Singletons ) | ||
Theorem | unisnif 34405 | Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ βͺ {π΄} = if(π΄ β V, π΄, β ) | ||
Theorem | brimage 34406 | Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ π΄ β V & β’ π΅ β V β β’ (π΄Imageπ π΅ β π΅ = (π β π΄)) | ||
Theorem | brimageg 34407 | Closed form of brimage 34406. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄Imageπ π΅ β π΅ = (π β π΄))) | ||
Theorem | funimage 34408 | Imageπ΄ is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun Imageπ΄ | ||
Theorem | fnimage 34409* | 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 34410* | 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 34411 | Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β π β§ (π β π΄) β π) β (Imageπ βπ΄) = (π β π΄)) | ||
Theorem | brcart 34412 | 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 34413 | 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 34414 | 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 34415 | Closed form of brdomain 34413. (Contributed by Scott Fenton, 2-May-2014.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄Domainπ΅ β π΅ = dom π΄)) | ||
Theorem | brrangeg 34416 | Closed form of brrange 34414. (Contributed by Scott Fenton, 3-May-2014.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄Rangeπ΅ β π΅ = ran π΄)) | ||
Theorem | brimg 34417 | 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 34418 | 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 34419 | 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 34420 | 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 34421 | 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 34422* | Lemma for funpartfun 34423. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
β’ (π΄ β dom ((ImageπΉ β Singleton) β© (V Γ Singletons )) β βπ₯(πΉ β {π΄}) = {π₯}) | ||
Theorem | funpartfun 34423 | 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 34424 | 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 34425 | 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 34426 | 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 34427 | 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 34428 | 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 34429 | 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 34430 | 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 34431 | 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 34432 | Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.) |
β’ β© π΄ = (V β (β‘(V β E ) β π΄)) | ||
Theorem | imagesset 34433 | 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 34434* | Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
β’ π β V & β’ π΄ β V β β’ (πUBπ π΄ β βπ₯ β π π₯π π΄) | ||
Theorem | brlb 34435* | Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
β’ π β V & β’ π΄ β V β β’ (πLBπ π΄ β βπ₯ β π π΄π π₯) | ||
Syntax | caltop 34436 | Declare the syntax for an alternate ordered pair. |
class βͺπ΄, π΅β« | ||
Syntax | caltxp 34437 | Declare the syntax for an alternate Cartesian product. |
class (π΄ ΓΓ π΅) | ||
Definition | df-altop 34438 | An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 34449), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ βͺπ΄, π΅β« = {{π΄}, {π΄, {π΅}}} | ||
Definition | df-altxp 34439* | Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.) |
β’ (π΄ ΓΓ π΅) = {π§ β£ βπ₯ β π΄ βπ¦ β π΅ π§ = βͺπ₯, π¦β«} | ||
Theorem | altopex 34440 | Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ βͺπ΄, π΅β« β V | ||
Theorem | altopthsn 34441 | 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 34442 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β βͺπ΄, πΆβ« = βͺπ΅, π·β«) | ||
Theorem | altopeq1 34443 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (π΄ = π΅ β βͺπ΄, πΆβ« = βͺπ΅, πΆβ«) | ||
Theorem | altopeq2 34444 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (π΄ = π΅ β βͺπΆ, π΄β« = βͺπΆ, π΅β«) | ||
Theorem | altopth1 34445 | 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 34446 | 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 34447 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ ((π΄ β π β§ π΅ β π) β (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | altopthbg 34448 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ ((π΄ β π β§ π· β π) β (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | altopth 34449 | 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 5431), requires π· to be a set. (Contributed by Scott Fenton, 23-Mar-2012.) |
β’ π΄ β V & β’ π΅ β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altopthb 34450 | Alternate ordered pair theorem with different sethood requirements. See altopth 34449 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ π΄ β V & β’ π· β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altopthc 34451 | Alternate ordered pair theorem with different sethood requirements. See altopth 34449 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ π΅ β V & β’ πΆ β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altopthd 34452 | Alternate ordered pair theorem with different sethood requirements. See altopth 34449 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
β’ πΆ β V & β’ π· β V β β’ (βͺπ΄, π΅β« = βͺπΆ, π·β« β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | altxpeq1 34453 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ (π΄ = π΅ β (π΄ ΓΓ πΆ) = (π΅ ΓΓ πΆ)) | ||
Theorem | altxpeq2 34454 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ (π΄ = π΅ β (πΆ ΓΓ π΄) = (πΆ ΓΓ π΅)) | ||
Theorem | elaltxp 34455* | Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.) |
β’ (π β (π΄ ΓΓ π΅) β βπ₯ β π΄ βπ¦ β π΅ π = βͺπ₯, π¦β«) | ||
Theorem | altopelaltxp 34456 | Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5666, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.) |
β’ (βͺπ, πβ« β (π΄ ΓΓ π΅) β (π β π΄ β§ π β π΅)) | ||
Theorem | altxpsspw 34457 | An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ (π΄ ΓΓ π΅) β π« π« (π΄ βͺ π« π΅) | ||
Theorem | altxpexg 34458 | The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ ΓΓ π΅) β V) | ||
Theorem | rankaltopb 34459 | 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 34460 | Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯βͺπ΄, π΅β« | ||
Theorem | sbcaltop 34461* | Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
β’ (π΄ β V β β¦π΄ / π₯β¦βͺπΆ, π·β« = βͺβ¦π΄ / π₯β¦πΆ, β¦π΄ / π₯β¦π·β«) | ||
Syntax | cofs 34462 | Declare the syntax for the outer five segment configuration. |
class OuterFiveSeg | ||
Definition | df-ofs 34463* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 27685). See brofs 34485 and 5segofs 34486 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 34464 | Deduction form of axcgrrflx 27661. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) β β’ (π β β¨π΄, π΅β©Cgrβ¨π΅, π΄β©) | ||
Theorem | cgrtr4d 34465 | Deduction form of axcgrtr 27662. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ (π β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) & β’ (π β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) β β’ (π β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) | ||
Theorem | cgrtr4and 34466 | Deduction form of axcgrtr 27662. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) | ||
Theorem | cgrrflx 34467 | Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΅β©Cgrβ¨π΄, π΅β©) | ||
Theorem | cgrrflxd 34468 | Deduction form of cgrrflx 34467. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) β β’ (π β β¨π΄, π΅β©Cgrβ¨π΄, π΅β©) | ||
Theorem | cgrcomim 34469 | 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 34470 | Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨πΆ, π·β©Cgrβ¨π΄, π΅β©)) | ||
Theorem | cgrcomand 34471 | Deduction form of cgrcom 34470. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨π΄, π΅β©) | ||
Theorem | cgrtr 34472 | Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β§ β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©)) | ||
Theorem | cgrtrand 34473 | Deduction form of cgrtr 34472. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) & β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) | ||
Theorem | cgrtr3 34474 | Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ)) β§ (π· β (πΌβπ) β§ πΈ β (πΌβπ) β§ πΉ β (πΌβπ))) β ((β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ© β§ β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©)) | ||
Theorem | cgrtr3and 34475 | Deduction form of cgrtr3 34474. (Contributed by Scott Fenton, 13-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΈ, πΉβ©) & β’ ((π β§ π) β β¨πΆ, π·β©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) | ||
Theorem | cgrcoml 34476 | 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 34477 | 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 34478 | Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β β¨π΅, π΄β©Cgrβ¨π·, πΆβ©)) | ||
Theorem | cgrcomland 34479 | Deduction form of cgrcoml 34476. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨π΅, π΄β©Cgrβ¨πΆ, π·β©) | ||
Theorem | cgrcomrand 34480 | Deduction form of cgrcoml 34476. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨π·, πΆβ©) | ||
Theorem | cgrcomlrand 34481 | Deduction form of cgrcomlr 34478. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨πΆ, π·β©) β β’ ((π β§ π) β β¨π΅, π΄β©Cgrβ¨π·, πΆβ©) | ||
Theorem | cgrtriv 34482 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β β¨π΄, π΄β©Cgrβ¨π΅, π΅β©) | ||
Theorem | cgrid2 34483 | Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (β¨π΄, π΄β©Cgrβ¨π΅, πΆβ© β π΅ = πΆ)) | ||
Theorem | cgrdegen 34484 | Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ))) β (β¨π΄, π΅β©Cgrβ¨πΆ, π·β© β (π΄ = π΅ β πΆ = π·))) | ||
Theorem | brofs 34485 | 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 34486 | Rephrase ax5seg 27685 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β ((β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β§ π΄ β π΅) β β¨πΆ, π·β©Cgrβ¨πΊ, π»β©)) | ||
Theorem | ofscom 34487 | The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.) |
β’ (((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ) β§ πΈ β (πΌβπ)) β§ (πΉ β (πΌβπ) β§ πΊ β (πΌβπ) β§ π» β (πΌβπ))) β (β¨β¨π΄, π΅β©, β¨πΆ, π·β©β© OuterFiveSeg β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© β β¨β¨πΈ, πΉβ©, β¨πΊ, π»β©β© OuterFiveSeg β¨β¨π΄, π΅β©, β¨πΆ, π·β©β©)) | ||
Theorem | cgrextend 34488 | 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 34489 | Deduction form of cgrextend 34488. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ (π β π· β (πΌβπ)) & β’ (π β πΈ β (πΌβπ)) & β’ (π β πΉ β (πΌβπ)) & β’ ((π β§ π) β π΅ Btwn β¨π΄, πΆβ©) & β’ ((π β§ π) β πΈ Btwn β¨π·, πΉβ©) & β’ ((π β§ π) β β¨π΄, π΅β©Cgrβ¨π·, πΈβ©) & β’ ((π β§ π) β β¨π΅, πΆβ©Cgrβ¨πΈ, πΉβ©) β β’ ((π β§ π) β β¨π΄, πΆβ©Cgrβ¨π·, πΉβ©) | ||
Theorem | segconeq 34490 | Two points that satisfy the conclusion of axsegcon 27674 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 34491* | Existential uniqueness version of segconeq 34490. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π· β (πΌβπ)) β§ πΆ β π·)) β β!π β (πΌβπ)(π· Btwn β¨πΆ, πβ© β§ β¨π·, πβ©Cgrβ¨π΄, π΅β©)) | ||
Theorem | btwntriv2 34492 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΅ Btwn β¨π΄, π΅β©) | ||
Theorem | btwncomim 34493 | Betweenness commutes. Implication version. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Btwn β¨π΅, πΆβ© β π΄ Btwn β¨πΆ, π΅β©)) | ||
Theorem | btwncom 34494 | Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β (π΄ Btwn β¨π΅, πΆβ© β π΄ Btwn β¨πΆ, π΅β©)) | ||
Theorem | btwncomand 34495 | Deduction form of btwncom 34494. (Contributed by Scott Fenton, 14-Oct-2013.) |
β’ (π β π β β) & β’ (π β π΄ β (πΌβπ)) & β’ (π β π΅ β (πΌβπ)) & β’ (π β πΆ β (πΌβπ)) & β’ ((π β§ π) β π΄ Btwn β¨π΅, πΆβ©) β β’ ((π β§ π) β π΄ Btwn β¨πΆ, π΅β©) | ||
Theorem | btwntriv1 34496 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
β’ ((π β β β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β π΄ Btwn β¨π΄, π΅β©) | ||
Theorem | btwnswapid 34497 | 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 34498 | 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 34499 | 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 34500 | 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 β¨π΅, π·β©)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |