Nuprl Lemma : ex-approx-context
∀[e:Atom2]. ∀[a,b,g:Base]. (ex-approx(e;g a;g b)) supposing (ex-approx(e;a;b) and e#g:Base)
Proof
Definitions occuring in Statement :
ex-approx: ex-approx(e;t;t'),
free-from-atom: a#x:T,
atom: Atom$n,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a,
base: Base
Definitions unfolded in proof :
prop: ℙ,
squash: ↓T,
implies: P ⇒ Q,
sq_stable: SqStable(P),
member: t ∈ T,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
ex-approx: ex-approx(e;t;t'),
all: ∀x:A. B[x],
compose: f o g
Lemmas referenced :
base_wf,
free-from-atom_wf2,
ex-approx_wf,
sq_stable__ex-approx,
istype-universe
Rules used in proof :
atomnEquality,
because_Cache,
imageElimination,
imageMemberEquality,
independent_functionElimination,
hypothesis,
baseClosed,
closedConclusion,
baseApply,
sqequalRule,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
lambdaFormation_alt,
inhabitedIsType,
dependent_functionElimination,
freeFromAtomApplication,
freeFromAtomTriviality,
lambdaEquality_alt,
functionExtensionality
Latex:
\mforall{}[e:Atom2]. \mforall{}[a,b,g:Base]. (ex-approx(e;g a;g b)) supposing (ex-approx(e;a;b) and e\#g:Base)
Date html generated:
2020_05_20-AM-09_08_06
Last ObjectModification:
2020_01_10-PM-03_37_42
Theory : minimal-first-order-logic
Home
Index