Nuprl Lemma : isect-rel_wf

[T,A:Type]. ∀[R:T ⟶ A ⟶ A ⟶ ℙ].  (isect-rel(T;i.R[i]) ∈ A ⟶ A ⟶ ℙ)


Proof




Definitions occuring in Statement :  isect-rel: isect-rel(T;i.R[i]) uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T isect-rel: isect-rel(T;i.R[i]) so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[T,A:Type].  \mforall{}[R:T  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (isect-rel(T;i.R[i])  \mmember{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{})



Date html generated: 2016_05_14-AM-06_04_52
Last ObjectModification: 2015_12_26-AM-11_32_58

Theory : relations


Home Index