### Nuprl Lemma : subtype_rel_not

`∀[P,Q:ℙ].  (¬P) ⊆r (¬Q) supposing Q `` (↓P)`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` not: `¬A` squash: `↓T` implies: `P `` Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` false: `False` implies: `P `` Q` subtype_rel: `A ⊆r B` prop: `ℙ` guard: `{T}` squash: `↓T`
Lemmas referenced :  squash_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality functionEquality sqequalHypSubstitution sqequalRule hypothesisEquality voidEquality axiomEquality hypothesis lemma_by_obid isectElimination thin isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality functionExtensionality independent_functionElimination imageElimination voidElimination

Latex:
\mforall{}[P,Q:\mBbbP{}].    (\mneg{}P)  \msubseteq{}r  (\mneg{}Q)  supposing  Q  {}\mRightarrow{}  (\mdownarrow{}P)

Date html generated: 2016_05_13-PM-03_18_57
Last ObjectModification: 2015_12_26-AM-09_08_05

Theory : subtype_0

Home Index