### Nuprl Lemma : stable__all

[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Stable{P[x]})  Stable{∀x:T. P[x]})

Proof

Definitions occuring in Statement :  stable: Stable{P} uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  guard: {T} prop: all: x:A. B[x] so_apply: x[s] so_lambda: λ2x.t[x] false: False not: ¬A member: t ∈ T uimplies: supposing a stable: Stable{P} implies:  Q uall: [x:A]. B[x]
Lemmas referenced :  stable_wf all_wf not_wf
Rules used in proof :  independent_functionElimination independent_isectElimination universeEquality functionEquality rename hypothesis functionExtensionality applyEquality cumulativity isectElimination extract_by_obid voidElimination hypothesisEquality thin dependent_functionElimination lambdaEquality sqequalHypSubstitution sqequalRule introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:T.  Stable\{P[x]\})  {}\mRightarrow{}  Stable\{\mforall{}x:T.  P[x]\})

Date html generated: 2016_10_21-AM-09_34_56
Last ObjectModification: 2016_09_26-PM-00_47_01

Theory : core_2

Home Index