Nuprl Lemma : t-sqle-apply-dependent
∀[A:Type]
∀[B:A ⟶ Type]
∀a1,a2:A. ∀f1,f2:a:A ⟶ B[a]. (t-sqle(a:A ⟶ B[a];f1;f2) ⇒ t-sqle(A;a1;a2) ⇒ t-sqle(B[a1];f1 a1;f2 a2))
supposing mono(A)
Proof
Definitions occuring in Statement :
mono: mono(T),
t-sqle: t-sqle(T;a;b),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
t-sqle: t-sqle(T;a;b),
squash: ↓T,
exists: ∃x:A. B[x],
per-class: per-class(T;a),
prop: ℙ,
so_apply: x[s],
mono: mono(T),
is-above: is-above(T;a;z),
and: P ∧ Q,
cand: A c∧ B,
subtype_rel: A ⊆r B
Lemmas referenced :
t-sqle_wf,
istype-universe,
mono_wf,
sqle_wf_base,
subtype_rel-equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
Error :lambdaFormation_alt,
sqequalHypSubstitution,
imageElimination,
productElimination,
thin,
setElimination,
rename,
sqequalRule,
imageMemberEquality,
hypothesisEquality,
baseClosed,
hypothesis,
Error :universeIsType,
extract_by_obid,
isectElimination,
functionEquality,
applyEquality,
Error :inhabitedIsType,
Error :functionIsType,
Error :lambdaEquality_alt,
dependent_functionElimination,
Error :functionIsTypeImplies,
Error :isect_memberEquality_alt,
because_Cache,
equalityTransitivity,
equalitySymmetry,
universeEquality,
independent_functionElimination,
Error :dependent_pairFormation_alt,
independent_pairFormation,
Error :productIsType,
Error :equalityIsType2,
Error :dependent_set_memberEquality_alt,
baseApply,
closedConclusion,
independent_isectElimination,
Error :equalityIsType3,
Error :equalityIsType1,
applyLambdaEquality,
sqleRule,
Error :setIsType
Latex:
\mforall{}[A:Type]
\mforall{}[B:A {}\mrightarrow{} Type]
\mforall{}a1,a2:A. \mforall{}f1,f2:a:A {}\mrightarrow{} B[a].
(t-sqle(a:A {}\mrightarrow{} B[a];f1;f2) {}\mRightarrow{} t-sqle(A;a1;a2) {}\mRightarrow{} t-sqle(B[a1];f1 a1;f2 a2))
supposing mono(A)
Date html generated:
2019_06_20-PM-00_28_25
Last ObjectModification:
2018_10_05-PM-04_01_28
Theory : subtype_1
Home
Index