Nuprl Lemma : l_all-l_contains

`∀[T:Type]. ∀[L1,L2:T List].  (L1 ⊆ L2 `` (∀P:T ⟶ ℙ. ((∀x∈L2.P[x]) `` (∀x∈L1.P[x]))))`

Proof

Definitions occuring in Statement :  l_contains: `A ⊆ B` l_all: `(∀x∈L.P[x])` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` l_all: `(∀x∈L.P[x])` l_contains: `A ⊆ B` member: `t ∈ T` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` le: `A ≤ B` prop: `ℙ` cand: `A c∧ B` so_apply: `x[s]` so_lambda: `λ2x.t[x]`
Lemmas referenced :  lelt_wf length_wf and_wf equal_wf int_seg_wf l_all_wf l_member_wf l_contains_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination rename setElimination dependent_set_memberEquality independent_pairFormation hypothesis cut introduction extract_by_obid isectElimination cumulativity addLevel levelHypothesis equalitySymmetry equalityTransitivity applyEquality lambdaEquality setEquality hyp_replacement Error :applyLambdaEquality,  sqequalRule natural_numberEquality functionExtensionality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].    (L1  \msubseteq{}  L2  {}\mRightarrow{}  (\mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}x\mmember{}L2.P[x])  {}\mRightarrow{}  (\mforall{}x\mmember{}L1.P[x]))))

Date html generated: 2016_10_21-AM-10_05_25
Last ObjectModification: 2016_07_12-AM-05_25_17

Theory : list_1

Home Index