Nuprl Lemma : tbar_wf

[T:Type]. ∀[X:(T List) ⟶ ℙ].  (tbar(T;X) ∈ ℙ)


Proof




Definitions occuring in Statement :  tbar: tbar(T;X) list: List uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T tbar: tbar(T;X) so_lambda: λ2x.t[x] nat: subtype_rel: A ⊆B so_apply: x[s] uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: all: x:A. B[x]
Lemmas referenced :  all_wf nat_wf exists_wf map_wf int_seg_wf subtype_rel_dep_function int_seg_subtype_nat false_wf upto_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin functionEquality hypothesis cumulativity hypothesisEquality lambdaEquality because_Cache applyEquality natural_numberEquality setElimination rename independent_isectElimination independent_pairFormation lambdaFormation axiomEquality equalityTransitivity equalitySymmetry universeEquality isect_memberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[X:(T  List)  {}\mrightarrow{}  \mBbbP{}].    (tbar(T;X)  \mmember{}  \mBbbP{})



Date html generated: 2016_05_14-PM-04_09_11
Last ObjectModification: 2015_12_26-PM-07_54_41

Theory : fan-theorem


Home Index