Nuprl Lemma : all_quot_elim

[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E[x;y])
   (∀[F:(x,y:T//E[x;y]) ⟶ ℙ]. ((∀w:x,y:T//E[x;y]. SqStable(F w))  (∀z:x,y:T//E[x;y]. F[z] ⇐⇒ ∀z:T. F[z]))))


Proof




Definitions occuring in Statement :  equiv_rel: EquivRel(T;x,y.E[x; y]) quotient: x,y:A//B[x; y] sq_stable: SqStable(P) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q implies:  Q apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  quotient: x,y:A//B[x; y] squash: T guard: {T} sq_stable: SqStable(P) uall: [x:A]. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q all: x:A. B[x] member: t ∈ T prop: so_lambda: λ2y.t[x; y] uimplies: supposing a so_lambda: λ2x.t[x] rev_implies:  Q subtype_rel: A ⊆B so_apply: x[s] so_apply: x[s1;s2]
Lemmas referenced :  squash_wf equal_wf equal-wf-base subtype_rel_self all_wf quotient_wf subtype_quotient sq_stable_wf equiv_rel_wf
Rules used in proof :  pointwiseFunctionalityForEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry because_Cache rename imageMemberEquality baseClosed productEquality instantiate independent_functionElimination dependent_functionElimination isect_memberFormation lambdaFormation independent_pairFormation hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin lambdaEquality applyEquality independent_isectElimination hypothesis functionEquality cumulativity universeEquality sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(T;x,y.E[x;y])
    {}\mRightarrow{}  (\mforall{}[F:(x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbP{}]
                ((\mforall{}w:x,y:T//E[x;y].  SqStable(F  w))  {}\mRightarrow{}  (\mforall{}z:x,y:T//E[x;y].  F[z]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:T.  F[z]))))



Date html generated: 2019_06_20-PM-01_05_18
Last ObjectModification: 2019_06_20-PM-00_59_36

Theory : quot_1


Home Index