Nuprl Lemma : preima_of_equiv_rel

`∀A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.  (EquivRel(B;x,y.x R y) `` EquivRel(A;x,y.x R_f y))`

Proof

Definitions occuring in Statement :  preima_of_rel: `R_f` equiv_rel: `EquivRel(T;x,y.E[x; y])` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  preima_of_rel: `R_f` equiv_rel: `EquivRel(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` cand: `A c∧ B` member: `t ∈ T` subtype_rel: `A ⊆r B` prop: `ℙ` uall: `∀[x:A]. B[x]` guard: `{T}`
Lemmas referenced :  subtype_rel_self istype-universe
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :lambdaFormation_alt,  sqequalHypSubstitution productElimination thin cut Error :universeIsType,  hypothesisEquality independent_pairFormation hypothesis applyEquality instantiate introduction extract_by_obid isectElimination universeEquality because_Cache Error :productIsType,  Error :functionIsType,  Error :inhabitedIsType,  dependent_functionElimination independent_functionElimination

Latex:
\mforall{}A,B:Type.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.    (EquivRel(B;x,y.x  R  y)  {}\mRightarrow{}  EquivRel(A;x,y.x  R\_f  y))

Date html generated: 2019_06_20-PM-00_33_11
Last ObjectModification: 2019_01_17-PM-00_44_38

Theory : quot_1

Home Index