Nuprl Lemma : squash_thru_implies_dec

[P,Q:ℙ].  uiff(↓ Q;P  (↓Q)) supposing Dec(P)


Proof




Definitions occuring in Statement :  decidable: Dec(P) uiff: uiff(P;Q) uimplies: supposing a uall: [x:A]. B[x] prop: squash: T implies:  Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q implies:  Q squash: T prop: decidable: Dec(P) or: P ∨ Q not: ¬A false: False
Lemmas referenced :  decidable_wf squash_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation sqequalHypSubstitution imageElimination independent_functionElimination thin hypothesis sqequalRule imageMemberEquality hypothesisEquality baseClosed lambdaEquality dependent_functionElimination lemma_by_obid isectElimination functionEquality unionElimination voidElimination productElimination independent_pairEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[P,Q:\mBbbP{}].    uiff(\mdownarrow{}P  {}\mRightarrow{}  Q;P  {}\mRightarrow{}  (\mdownarrow{}Q))  supposing  Dec(P)



Date html generated: 2016_05_13-PM-03_16_22
Last ObjectModification: 2016_01_06-PM-05_50_09

Theory : core_2


Home Index