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