### Nuprl Lemma : sq_stable__and

`∀[P:ℙ]. ∀[Q:⋂p:P. ℙ].  (SqStable(P) `` (P `` SqStable(Q)) `` SqStable(P ∧ Q))`

Proof

Definitions occuring in Statement :  sq_stable: `SqStable(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` and: `P ∧ Q` isect: `⋂x:A. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` sq_stable: `SqStable(P)` member: `t ∈ T` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` squash: `↓T` cand: `A c∧ B`
Lemmas referenced :  sq_stable_wf squash_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin productEquality cumulativity hypothesisEquality hypothesis rename sqequalRule equalityTransitivity equalitySymmetry functionEquality applyEquality lambdaEquality isectEquality universeEquality independent_functionElimination imageElimination introduction productElimination imageMemberEquality baseClosed independent_pairFormation

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}[Q:\mcap{}p:P.  \mBbbP{}].    (SqStable(P)  {}\mRightarrow{}  (P  {}\mRightarrow{}  SqStable(Q))  {}\mRightarrow{}  SqStable(P  \mwedge{}  Q))

Date html generated: 2016_05_13-PM-03_09_40
Last ObjectModification: 2016_01_06-PM-05_49_10

Theory : core_2

Home Index