### Nuprl Lemma : quotient-isect-base

`∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T//E[x;y] ⋂ Base ≡ T ⋂ Base supposing EquivRel(T;x,y.E[x;y])`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` isect2: `T1 ⋂ T2` quotient: `x,y:A//B[x; y]` ext-eq: `A ≡ B` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` function: `x:A ⟶ B[x]` base: `Base` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` isect2: `T1 ⋂ T2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cand: `A c∧ B` bfalse: `ff` or: `P ∨ Q` prop: `ℙ` quotient: `x,y:A//B[x; y]`
Lemmas referenced :  isect2_decomp quotient_wf istype-universe base_wf isect2_subtype_rel2 bool_wf isect2_wf isect2_subtype_rel3 subtype_quotient subtype_rel_wf equiv_rel_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation Error :lambdaEquality_alt,  isect_memberEquality sqequalHypSubstitution unionElimination thin equalityElimination sqequalRule extract_by_obid isectElimination because_Cache applyEquality hypothesisEquality Error :inhabitedIsType,  hypothesis independent_isectElimination productElimination equalityTransitivity equalitySymmetry Error :universeIsType,  Error :inlFormation_alt,  independent_pairEquality axiomEquality Error :isect_memberEquality_alt,  Error :functionIsType,  universeEquality pertypeElimination Error :productIsType,  Error :equalityIsType4,  instantiate

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    x,y:T//E[x;y]  \mcap{}  Base  \mequiv{}  T  \mcap{}  Base  supposing  EquivRel(T;x,y.E[x;y])

Date html generated: 2019_06_20-PM-00_32_20
Last ObjectModification: 2018_10_06-PM-03_56_25

Theory : quot_1

Home Index