### Nuprl Lemma : maximal-sub-bag_wf

`∀[T:Type]. ∀[b,m:bag(T)]. ∀[P:bag(T) ⟶ ℙ].  (maximal-sub-bag(T;m;b;s.P[s]) ∈ ℙ)`

Proof

Definitions occuring in Statement :  maximal-sub-bag: `maximal-sub-bag(T;m;b;s.P[s])` bag: `bag(T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` so_apply: `x[s]` implies: `P `` Q` so_lambda: `λ2x.t[x]` and: `P ∧ Q` prop: `ℙ` maximal-sub-bag: `maximal-sub-bag(T;m;b;s.P[s])` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  sub-bag_wf bag_wf all_wf
Rules used in proof :  because_Cache isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality universeEquality functionExtensionality applyEquality functionEquality lambdaEquality hypothesis hypothesisEquality cumulativity thin isectElimination sqequalHypSubstitution extract_by_obid productEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[b,m:bag(T)].  \mforall{}[P:bag(T)  {}\mrightarrow{}  \mBbbP{}].    (maximal-sub-bag(T;m;b;s.P[s])  \mmember{}  \mBbbP{})

Date html generated: 2018_05_21-PM-06_24_43
Last ObjectModification: 2018_01_08-AM-00_34_54

Theory : bags

Home Index