### Nuprl Lemma : bag-extensionality1

`∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].`
`  ∀[as,bs:bag(T)].  uiff(as = bs ∈ bag(T);∀x:T. (#([y∈as|eq x y]) = #([y∈bs|eq x y]) ∈ ℤ)) `
`  supposing ∀[x,y:T].  (↑(eq x y) `⇐⇒` x = y ∈ T)`

Proof

Definitions occuring in Statement :  bag-size: `#(bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` assert: `↑b` bool: `𝔹` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` apply: `f a` function: `x:A ⟶ B[x]` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` all: `∀x:A. B[x]` squash: `↓T` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` true: `True` subtype_rel: `A ⊆r B` bag: `bag(T)` quotient: `x,y:A//B[x; y]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` guard: `{T}` bag-filter: `[x∈b|p[x]]` bag-size: `#(bs)`
Lemmas referenced :  bag-size_wf set_wf assert_wf bag-filter_wf equal_wf bag_wf all_wf uall_wf iff_wf bool_wf list_wf permutation_wf permutation_weakening quotient-member-eq permutation-equiv equal-wf-base list-subtype-bag squash_wf true_wf permutation-iff-count1 filter_functionality eta_conv length_wf filter_wf5 subtype_rel_dep_function l_member_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination because_Cache hypothesis sqequalRule functionExtensionality hypothesisEquality cumulativity imageMemberEquality baseClosed natural_numberEquality dependent_functionElimination axiomEquality intEquality setEquality productElimination independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality promote_hyp independent_isectElimination pointwiseFunctionality pertypeElimination independent_functionElimination productEquality universeEquality hyp_replacement setElimination rename

Latex:
\mforall{}[T:Type].  \mforall{}[eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[as,bs:bag(T)].    uiff(as  =  bs;\mforall{}x:T.  (\#([y\mmember{}as|eq  x  y])  =  \#([y\mmember{}bs|eq  x  y])))
supposing  \mforall{}[x,y:T].    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y)

Date html generated: 2017_10_01-AM-08_59_27
Last ObjectModification: 2017_07_26-PM-04_41_37

Theory : bags

Home Index