### Nuprl Lemma : uequiv_rel_functionality_wrt_iff

`∀[T,T':Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[E':T' ⟶ T' ⟶ ℙ].`
`  (∀[x,y:T].  (E[x;y] `⇐⇒` E'[x;y])) `` (UniformEquivRel(T;x,y.E[x;y]) `⇐⇒` UniformEquivRel(T';x,y.E'[x;y])) `
`  supposing T = T' ∈ Type`

Proof

Definitions occuring in Statement :  uequiv_rel: `UniformEquivRel(T;x,y.E[x; y])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` uequiv_rel: `UniformEquivRel(T;x,y.E[x; y])` urefl: `UniformlyRefl(T;x,y.E[x; y])` so_apply: `x[s1;s2]` usym: `UniformlySym(T;x,y.E[x; y])` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` prop: `ℙ` utrans: `UniformlyTrans(T;x,y.E[x; y])` so_lambda: `λ2x y.t[x; y]` so_lambda: `λ2x.t[x]` guard: `{T}` so_apply: `x[s]`
Lemmas referenced :  subtype_rel_self uequiv_rel_wf uall_wf iff_wf subtype_rel_weakening ext-eq_weakening equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction axiomEquality hypothesis thin rename lambdaFormation independent_pairFormation sqequalHypSubstitution productElimination promote_hyp isectElimination hyp_replacement hypothesisEquality equalitySymmetry because_Cache independent_functionElimination applyEquality sqequalRule instantiate extract_by_obid lambdaEquality independent_isectElimination universeEquality functionEquality cumulativity

Latex:
\mforall{}[T,T':Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[E':T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}].
(\mforall{}[x,y:T].    (E[x;y]  \mLeftarrow{}{}\mRightarrow{}  E'[x;y]))
{}\mRightarrow{}  (UniformEquivRel(T;x,y.E[x;y])  \mLeftarrow{}{}\mRightarrow{}  UniformEquivRel(T';x,y.E'[x;y]))
supposing  T  =  T'

Date html generated: 2019_06_20-PM-00_29_04
Last ObjectModification: 2018_08_25-AM-08_25_07

Theory : rel_1

Home Index