Nuprl Lemma : sq_stable_iff_stable
XM ⇒ (∀P:ℙ. (SqStable(P) ⇐⇒ Stable{P}))
Proof
Definitions occuring in Statement :
xmiddle: XM,
sq_stable: SqStable(P),
stable: Stable{P},
prop: ℙ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q
Definitions unfolded in proof :
implies: P ⇒ Q,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
rev_implies: P ⇐ Q,
xmiddle: XM
Lemmas referenced :
sq_stable_wf,
sq_stable__from_stable,
stable__from_decidable,
stable_wf,
xmiddle_wf,
xmiddle-implies-stable
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
independent_pairFormation,
Error :universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
independent_functionElimination,
because_Cache,
dependent_functionElimination,
universeEquality
Latex:
XM {}\mRightarrow{} (\mforall{}P:\mBbbP{}. (SqStable(P) \mLeftarrow{}{}\mRightarrow{} Stable\{P\}))
Date html generated:
2019_06_20-AM-11_15_45
Last ObjectModification:
2018_09_27-PM-05_36_21
Theory : core_2
Home
Index