Nuprl Lemma : sq_stable__uiff

[P,Q:ℙ].  (SqStable(P)  SqStable(Q)  SqStable(uiff(P;Q)))


Proof




Definitions occuring in Statement :  sq_stable: SqStable(P) uiff: uiff(P;Q) uall: [x:A]. B[x] prop: implies:  Q
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q member: t ∈ T prop: uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] uiff: uiff(P;Q) and: P ∧ Q
Lemmas referenced :  sq_stable_wf sq_stable__and isect_wf sq_stable__uimplies
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  Error :universeIsType,  universeEquality cumulativity sqequalRule lambdaEquality isect_memberEquality independent_functionElimination because_Cache

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



Date html generated: 2019_06_20-AM-11_15_21
Last ObjectModification: 2018_09_26-AM-09_59_32

Theory : core_2


Home Index