Nuprl Lemma : disjoint-union-comb-single-val

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (single-valued-classrel(es;X (+) Y;A + B)) supposing
     (disjoint-classrel(es;A;X;B;Y) and
     single-valued-classrel(es;Y;B) and
     single-valued-classrel(es;X;A))

Proof

Definitions occuring in Statement : disjoint-union-comb: X (+) Y, single-valued-classrel: single-valued-classrel(es;X;T), disjoint-classrel: disjoint-classrel(es;A;X;B;Y), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), uimplies: b supposing a, uall: ∀[x:A]. B[x], union: left + right, universe: Type
Definitions unfolded in proof : disjoint-union-comb: X (+) Y, uall: ∀[x:A]. B[x], member: t ∈ T, all: ∀x:A. B[x], uimplies: b supposing a, implies: P ⇒ Q, prop: ℙ, subtype_rel: A ⊆r B, so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], single-valued-classrel: single-valued-classrel(es;X;T)

Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. (single-valued-classrel(es;X (+) Y;A + B)) supposing (disjoint-classrel(es;A;X;B;Y) and single-valued-classrel(es;Y;B) and single-valued-classrel(es;X;A)) Date html generated: 2016_05_17-AM-09_34_20 Last ObjectModification: 2015_12_29-PM-03_59_07 Theory : classrel!lemmas Home Index