Nuprl Lemma : per-union-implies-wf2

[A,B:Type]. ∀[x:per-union(A;B)].  (x inr outr(x)  ∈ ℙ)


Proof




Definitions occuring in Statement :  per-union: per-union(A;B) outr: outr(x) uall: [x:A]. B[x] prop: member: t ∈ T inr: inr  universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T squash: T prop: iff: ⇐⇒ Q and: P ∧ Q implies:  Q uimplies: supposing a per-union: per-union(A;B) has-value: (a)↓ outr: outr(x) uand: uand(A;B) guard: {T} top: Top outl: outl(x) sq_type: SQType(T) all: x:A. B[x] rev_implies:  Q true: True
Lemmas referenced :  sqequal-wf-base member_wf subtype_base_sq subtype_rel_self has-value_wf_base is-exception_wf cbv-sqequal0 istype-top istype-void if-per-void uand_wf equal-wf-base per-void_wf istype-sqequal per-union_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut pointwiseFunctionality introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule baseApply closedConclusion baseClosed hypothesis applyEquality instantiate Error :lambdaEquality_alt,  imageElimination because_Cache universeEquality sqequalExtensionalEquality independent_pairFormation Error :lambdaFormation_alt,  independent_isectElimination pertypeElimination promote_hyp axiomSqleEquality divergentSqle sqleReflexivity isinrCases axiomSqEquality Error :inhabitedIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  voidElimination rename isaxiomCases Error :universeIsType,  independent_functionElimination isectEquality isinlCases dependent_functionElimination equalityTransitivity equalitySymmetry imageMemberEquality natural_numberEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[x:per-union(A;B)].    (x  \msim{}  inr  outr(x)    \mmember{}  \mBbbP{})



Date html generated: 2019_06_20-AM-11_30_45
Last ObjectModification: 2019_01_03-PM-03_56_16

Theory : per!type


Home Index