### Nuprl Lemma : equiv-class_wf

`∀[A:Type]. ∀[E:A ⟶ A ⟶ 𝔹].`
`  ∀[t:x,y:A//(↑E[x;y])]. (equiv-class(A;x,y.E[x;y];t) ∈ Type) supposing EquivRel(A;x,y.↑E[x;y])`

Proof

Definitions occuring in Statement :  equiv-class: `equiv-class(A;a,b.E[a; b];t)` equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` equiv-class: `equiv-class(A;a,b.E[a; b];t)` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` iff: `P `⇐⇒` Q` implies: `P `` Q` rev_implies: `P `` Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` all: `∀x:A. B[x]` sym: `Sym(T;x,y.E[x; y])`
Lemmas referenced :  assert_wf squash_wf true_wf bool_wf equal-wf-base quotient_wf equiv_rel_wf iff_imp_equal_bool
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut pointwiseFunctionalityForEquality universeEquality sqequalHypSubstitution sqequalRule pertypeElimination productElimination thin setEquality hypothesisEquality applyEquality lambdaEquality imageElimination extract_by_obid isectElimination equalityTransitivity hypothesis equalitySymmetry natural_numberEquality imageMemberEquality baseClosed productEquality because_Cache functionExtensionality cumulativity axiomEquality independent_isectElimination isect_memberEquality functionEquality independent_pairFormation lambdaFormation dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[t:x,y:A//(\muparrow{}E[x;y])].  (equiv-class(A;x,y.E[x;y];t)  \mmember{}  Type)  supposing  EquivRel(A;x,y.\muparrow{}E[x;y])

Date html generated: 2016_10_21-AM-09_43_50
Last ObjectModification: 2016_08_07-PM-06_00_35

Theory : quot_1

Home Index