Nuprl Lemma : set_blt_functionality_wrt_set_lt_r
∀[s:QOSet]. ∀[a,b,b':|s|]. ↑(a <b b ⇒b (a <b b')) supposing b <s b'
Proof
Definitions occuring in Statement :
qoset: QOSet,
set_lt: a <p b,
set_blt: a <b b,
set_car: |p|,
bimplies: p ⇒b q,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
qoset: QOSet,
dset: DSet,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
set_lt: a <p b,
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
guard: {T}
Lemmas referenced :
set_lt_wf,
set_car_wf,
qoset_wf,
assert_wf,
bimplies_wf,
set_blt_wf,
isect_wf,
assert_witness,
iff_transitivity,
iff_weakening_uiff,
assert_of_bimplies,
assert_of_set_lt,
set_lt_transitivity_2,
set_leq_weakening_lt
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
setElimination,
rename,
because_Cache,
hypothesis,
hypothesisEquality,
inhabitedIsType,
sqequalRule,
isect_memberEquality_alt,
lambdaEquality_alt,
isectIsType,
independent_functionElimination,
independent_pairFormation,
lambdaFormation_alt,
independent_isectElimination,
productElimination
Latex:
\mforall{}[s:QOSet]. \mforall{}[a,b,b':|s|]. \muparrow{}(a <\msubb{} b {}\mRightarrow{}\msubb{} (a <\msubb{} b')) supposing b <s b'
Date html generated:
2019_10_15-AM-10_32_31
Last ObjectModification:
2018_10_15-PM-08_50_01
Theory : sets_1
Home
Index