Nuprl Lemma : not_over_exists

[T:Type]. ∀[Q:T ⟶ ℙ].  uiff(¬(∃x:T. Q[x]);∀x:T. Q[x]))


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] not: ¬A function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T so_apply: x[s] subtype_rel: A ⊆B prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] exists: x:A. B[x] all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a not: ¬A implies:  Q false: False
Lemmas referenced :  not_wf exists_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity applyEquality hypothesisEquality cut hypothesis thin lambdaEquality sqequalHypSubstitution sqequalRule universeEquality because_Cache Error :universeIsType,  introduction extract_by_obid isectElimination Error :functionIsType,  functionEquality cumulativity Error :isect_memberFormation_alt,  independent_pairFormation lambdaFormation independent_functionElimination voidElimination dependent_functionElimination productElimination independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry dependent_pairFormation

Latex:
\mforall{}[T:Type].  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].    uiff(\mneg{}(\mexists{}x:T.  Q[x]);\mforall{}x:T.  (\mneg{}Q[x]))



Date html generated: 2019_06_20-AM-11_16_33
Last ObjectModification: 2018_09_26-AM-10_24_17

Theory : core_2


Home Index