Nuprl Lemma : ppcc-test3
∀[T:Type]
∀f:T ⟶ T
∀[Q,P:T ⟶ T ⟶ ℙ].
((∀a,b:T. (Q[f[a];b] ⇐⇒ P[a;f[b]]))
⇒ Trans(T;a,b.P[a;b])
⇒ (∀a,b,c,d,e,x:T. (P[a;c] ⇒ Q[d;b] ⇒ P[a;e]) supposing ((f[b] = e ∈ T) and (f[x] = d ∈ T) and (c = x ∈ T))))
Proof
Definitions occuring in Statement :
trans: Trans(T;x,y.E[x; y]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2],
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
member: t ∈ T,
prop: ℙ,
so_apply: x[s1;s2],
so_apply: x[s],
so_lambda: λ2x y.t[x; y],
so_lambda: λ2x.t[x],
guard: {T},
and: P ∧ Q,
iff: P ⇐⇒ Q,
trans: Trans(T;x,y.E[x; y])
Lemmas referenced :
equal_wf,
trans_wf,
all_wf,
iff_wf,
and_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
axiomEquality,
hypothesis,
thin,
rename,
applyEquality,
functionExtensionality,
hypothesisEquality,
cumulativity,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
sqequalRule,
lambdaEquality,
functionEquality,
universeEquality,
hyp_replacement,
equalitySymmetry,
dependent_set_memberEquality,
independent_pairFormation,
setElimination,
productElimination,
setEquality,
equalityTransitivity,
dependent_functionElimination,
independent_functionElimination
Latex:
\mforall{}[T:Type]
\mforall{}f:T {}\mrightarrow{} T
\mforall{}[Q,P:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}].
((\mforall{}a,b:T. (Q[f[a];b] \mLeftarrow{}{}\mRightarrow{} P[a;f[b]]))
{}\mRightarrow{} Trans(T;a,b.P[a;b])
{}\mRightarrow{} (\mforall{}a,b,c,d,e,x:T.
(P[a;c] {}\mRightarrow{} Q[d;b] {}\mRightarrow{} P[a;e]) supposing ((f[b] = e) and (f[x] = d) and (c = x))))
Date html generated:
2016_10_25-AM-10_43_39
Last ObjectModification:
2016_07_12-AM-06_53_57
Theory : general
Home
Index