### Nuprl Lemma : strict_part_wf

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (strict_part(x,y.R[x;y];a;b) ∈ ℙ)

Proof

Definitions occuring in Statement :  strict_part: strict_part(x,y.R[x; y];a;b) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T strict_part: strict_part(x,y.R[x; y];a;b) prop: and: P ∧ Q so_apply: x[s1;s2] subtype_rel: A ⊆B
Lemmas referenced :  subtype_rel_self not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule productEquality applyEquality hypothesisEquality hypothesis thin instantiate extract_by_obid sqequalHypSubstitution isectElimination universeEquality axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  isect_memberEquality Error :universeIsType,  because_Cache Error :functionIsType,  functionEquality cumulativity

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[a,b:T].    (strict\_part(x,y.R[x;y];a;b)  \mmember{}  \mBbbP{})

Date html generated: 2019_06_20-PM-00_29_16
Last ObjectModification: 2018_09_26-AM-11_46_43

Theory : rel_1

Home Index