Nuprl Lemma : free-from-atom-pair-components
∀[a:Atom1]. ∀[X:Type]. ∀[Y:X ⟶ 𝕌']. ∀[x:X]. ∀[y:Y[x]]. {a#x:X ∧ a#y:Y[x]} supposing a#<x, y>:x:X × Y[x]
Proof
Definitions occuring in Statement :
free-from-atom: a#x:T,
atom: Atom$n,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
so_apply: x[s],
and: P ∧ Q,
function: x:A ⟶ B[x],
pair: <a, b>,
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
guard: {T},
and: P ∧ Q,
prop: ℙ,
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B
Lemmas referenced :
free-from-atom_wf,
equal_wf,
pi1_wf,
subtype_rel_self,
subtype_rel_wf,
set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
independent_pairFormation,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairEquality,
freeFromAtomAxiom,
hypothesis,
instantiate,
extract_by_obid,
isectElimination,
productEquality,
cumulativity,
hypothesisEquality,
applyEquality,
functionExtensionality,
dependent_pairEquality,
functionEquality,
universeEquality,
atomnEquality,
freeFromAtomApplication,
freeFromAtomTriviality,
lambdaEquality,
lambdaFormation,
setElimination,
rename,
hyp_replacement,
equalitySymmetry,
applyLambdaEquality,
because_Cache,
freeFromAtomSet,
dependent_set_memberEquality
Latex:
\mforall{}[a:Atom1]. \mforall{}[X:Type]. \mforall{}[Y:X {}\mrightarrow{} \mBbbU{}']. \mforall{}[x:X]. \mforall{}[y:Y[x]]. \{a\#x:X \mwedge{} a\#y:Y[x]\} supposing a\#<x, y>:x:X \mtimes{}\000C Y[x]
Date html generated:
2017_04_14-AM-07_14_37
Last ObjectModification:
2017_02_27-PM-02_50_16
Theory : atom_1
Home
Index