Nuprl Lemma : le_int-wf-partial2

[x,y:partial(ℤ)].  (x ≤y ∈ partial(𝔹))


Proof




Definitions occuring in Statement :  partial: partial(T) le_int: i ≤j bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uimplies: supposing a
Lemmas referenced :  le_int-wf-partial subtype_rel_partial base_wf int_subtype_base partial_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality intEquality hypothesis independent_isectElimination sqequalRule because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[x,y:partial(\mBbbZ{})].    (x  \mleq{}z  y  \mmember{}  partial(\mBbbB{}))



Date html generated: 2016_05_14-AM-06_10_36
Last ObjectModification: 2015_12_26-AM-11_51_46

Theory : partial_1


Home Index