### 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: `b 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: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` prop: `ℙ` uimplies: `b supposing a` squash: `↓T` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}` true: `True` iff: `P `⇐⇒` Q` and: `P ∧ Q` bag: `bag(T)` quotient: `x,y:A//B[x; y]` cand: `A c∧ B` so_lambda: `λ2x.t[x]` so_lambda: `λ2x y.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