Nuprl Lemma : test-exists-example1

[D:ℙ]. ∀[P,Q,R:D ⟶ ℙ].
  ((∀x:D. ((R x)  (Q x)))  (∀x:D. ((P x)  ((Q x) ∨ (R x))))  (∃x:D. (P x))  (∃x:D. (Q x)))


Proof




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

Latex:
\mforall{}[D:\mBbbP{}].  \mforall{}[P,Q,R:D  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:D.  ((R  x)  {}\mRightarrow{}  (Q  x)))  {}\mRightarrow{}  (\mforall{}x:D.  ((P  x)  {}\mRightarrow{}  ((Q  x)  \mvee{}  (R  x))))  {}\mRightarrow{}  (\mexists{}x:D.  (P  x))  {}\mRightarrow{}  (\mexists{}x:D.  (Q  x)))



Date html generated: 2016_05_15-PM-03_18_54
Last ObjectModification: 2015_12_27-PM-01_03_23

Theory : general


Home Index