Nuprl Lemma : test-model3

[Dom:Type]. ∀[A,B:Dom ⟶ ℙ].
  ((∀x:Dom. ∃y:Dom. (A[y] ∨ B[y]))
   (∀x,y,z:Dom.  ((A[y] ∧ A[z])  A[x]))
   (∀x,y,z:Dom.  ((B[y] ∧ B[z])  A[x]))
   (∀x:Dom. A[x]))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T exists: x:A. B[x] or: P ∨ Q and: P ∧ Q prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  all_wf and_wf exists_wf or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation rename cut hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination unionElimination because_Cache independent_functionElimination independent_pairFormation lemma_by_obid isectElimination sqequalRule lambdaEquality functionEquality applyEquality cumulativity universeEquality

Latex:
\mforall{}[Dom:Type].  \mforall{}[A,B:Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:Dom.  \mexists{}y:Dom.  (A[y]  \mvee{}  B[y]))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((A[y]  \mwedge{}  A[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((B[y]  \mwedge{}  B[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  A[x]))



Date html generated: 2016_05_15-PM-03_19_30
Last ObjectModification: 2015_12_27-PM-01_03_56

Theory : general


Home Index