Nuprl Lemma : bsubmset_functionality_wrt_bsubmset
∀s:DSet. ∀a,a',b,b':MSet{s}. ((↑(a ⊇bs b)) ⇒ (↑(a' ⊆b b')) ⇒ (↑(a ⊆b a' ⇒b (b ⊆b b'))))
Proof
Definitions occuring in Statement :
bsupmset: a ⊇bs b,
bsubmset: a ⊆b b,
mset: MSet{s},
bimplies: p ⇒b q,
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
dset: DSet
Definitions unfolded in proof :
all: ∀x:A. B[x],
bsupmset: a ⊇bs b,
member: t ∈ T,
rev_implies: P ⇐ Q,
so_lambda: λ2x.t[x],
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
prop: ℙ,
so_apply: x[s],
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
dset: DSet,
guard: {T},
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
dset_wf,
all_mset_elim,
rev_implies_wf,
assert_wf,
bimplies_wf,
bsubmset_wf,
mk_mset_wf,
mset_wf,
sq_stable__all,
sq_stable_from_decidable,
decidable__assert,
all_wf,
list_wf,
set_car_wf,
iff_weakening_uiff,
isect_wf,
assert_of_bimplies,
assert_functionality_wrt_uiff,
bsublist_wf,
bsubmset_elim,
bsublist_transitivity,
assert_witness
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalRule,
universeIsType,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
lambdaEquality_alt,
isectElimination,
because_Cache,
isect_memberEquality_alt,
independent_functionElimination,
productElimination,
inhabitedIsType,
functionEquality,
setElimination,
rename,
isect_memberFormation_alt,
independent_isectElimination
Latex:
\mforall{}s:DSet. \mforall{}a,a',b,b':MSet\{s\}. ((\muparrow{}(a \msupseteq{}\msubb{}s b)) {}\mRightarrow{} (\muparrow{}(a' \msubseteq{}\msubb{} b')) {}\mRightarrow{} (\muparrow{}(a \msubseteq{}\msubb{} a' {}\mRightarrow{}\msubb{} (b \msubseteq{}\msubb{} b'))))
Date html generated:
2019_10_16-PM-01_06_48
Last ObjectModification:
2018_10_15-PM-08_51_11
Theory : mset
Home
Index