### Nuprl Lemma : infinite-domain-example-ext

`∀[A,D:Type]. ∀[R,Eq:D ⟶ D ⟶ ℙ].`
`  ((∀x,y,z:D.  (R[x;y] `` (R[y;z] ∨ Eq[y;z]) `` R[x;z]))`
`  `` (∀x:D. (R[x;x] `` A))`
`  `` (∀x:D. ∃y:D. R[x;y])`
`  `` (∃m:D. ∀x:D. ((Eq[x;m] `` A) `` R[x;m]))`
`  `` A)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` infinite-domain-example
Lemmas referenced :  infinite-domain-example
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A,D:Type].  \mforall{}[R,Eq:D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x,y,z:D.    (R[x;y]  {}\mRightarrow{}  (R[y;z]  \mvee{}  Eq[y;z])  {}\mRightarrow{}  R[x;z]))
{}\mRightarrow{}  (\mforall{}x:D.  (R[x;x]  {}\mRightarrow{}  A))
{}\mRightarrow{}  (\mforall{}x:D.  \mexists{}y:D.  R[x;y])
{}\mRightarrow{}  (\mexists{}m:D.  \mforall{}x:D.  ((Eq[x;m]  {}\mRightarrow{}  A)  {}\mRightarrow{}  R[x;m]))
{}\mRightarrow{}  A)

Date html generated: 2018_05_21-PM-08_55_24
Last ObjectModification: 2018_05_19-PM-05_07_46

Theory : general

Home Index