### Nuprl Lemma : le_int-wf-bar-int

`∀[x,y:bar(ℤ)].  (x ≤z y ∈ bar(𝔹))`

Proof

Definitions occuring in Statement :  bar: `bar(T)` le_int: `i ≤z j` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` guard: `{T}` or: `P ∨ Q` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q`
Lemmas referenced :  subtype_bar2 base_wf int_subtype_base value-type_wf subtype_rel_self bar-base le_int-wf-bar subtype_barSqtype_base int-value-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis independent_isectElimination independent_pairFormation sqequalRule inrFormation because_Cache hypothesisEquality applyEquality dependent_functionElimination independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

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

Date html generated: 2016_07_08-PM-05_18_57
Last ObjectModification: 2015_12_27-PM-05_17_05

Theory : bar!type

Home Index