Nuprl Lemma : bag-eq-subtype1

[A:Type]. ∀[B:A ⟶ ℙ]. ∀[d1,d2:bag({a:A| B[a]} )].  d1 d2 ∈ bag({a:A| B[a]} supposing d1 d2 ∈ bag(A)


Proof




Definitions occuring in Statement :  bag: bag(T) uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s] set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B so_apply: x[s] prop: uimplies: supposing a squash: T exists: x:A. B[x] all: x:A. B[x] implies:  Q guard: {T} true: True iff: ⇐⇒ Q and: P ∧ Q bag: bag(T) quotient: x,y:A//B[x; y] cand: c∧ B so_lambda: λ2x.t[x] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  equal_wf bag_wf subtype_rel_bag bag_to_squash_list equal_functionality_wrt_subtype_rel2 subtype_rel_wf squash_wf true_wf iff_weakening_equal list-subtype-bag subtype_rel_self permutation-strong-subtype strong-subtype-set2 quotient-member-eq list_wf permutation_wf permutation-equiv member_wf subtype_rel_list
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis applyEquality setEquality functionExtensionality lambdaEquality sqequalRule universeEquality independent_isectElimination setElimination rename because_Cache functionEquality isect_memberFormation isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry imageElimination productElimination lambdaFormation independent_functionElimination dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed hyp_replacement applyLambdaEquality pertypeElimination productEquality

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d1,d2:bag(\{a:A|  B[a]\}  )].    d1  =  d2  supposing  d1  =  d2



Date html generated: 2017_10_01-AM-08_57_42
Last ObjectModification: 2017_07_26-PM-04_39_47

Theory : bags


Home Index