Nuprl Lemma : p-graph_wf2

[A:Type]. ∀[f:A ⟶ (A Top)].  (p-graph(A;f) ∈ A ⟶ A ⟶ ℙ)


Proof




Definitions occuring in Statement :  p-graph: p-graph(A;f) uall: [x:A]. B[x] top: Top prop: member: t ∈ T function: x:A ⟶ B[x] union: left right universe: Type
Definitions unfolded in proof :  p-graph: p-graph(A;f) uall: [x:A]. B[x] member: t ∈ T prop: cand: c∧ B subtype_rel: A ⊆B uimplies: supposing a top: Top
Lemmas referenced :  assert_wf can-apply_wf subtype_rel_union top_wf equal_wf do-apply_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaEquality productEquality extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality functionExtensionality applyEquality hypothesis because_Cache independent_isectElimination isect_memberEquality voidElimination voidEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality unionEquality universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].    (p-graph(A;f)  \mmember{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{})



Date html generated: 2018_05_21-PM-07_36_33
Last ObjectModification: 2017_07_26-PM-05_10_34

Theory : general


Home Index