Nuprl Lemma : preima_of_rel_wf
∀A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ. (R_f ∈ A ⟶ A ⟶ ℙ)
Proof
Definitions occuring in Statement :
preima_of_rel: R_f,
prop: ℙ,
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
preima_of_rel: R_f,
infix_ap: x f y,
prop: ℙ
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
lambdaEquality,
applyEquality,
functionExtensionality,
hypothesisEquality,
cumulativity,
sqequalHypSubstitution,
hypothesis,
functionEquality,
universeEquality
Latex:
\mforall{}A,B:Type. \mforall{}f:A {}\mrightarrow{} B. \mforall{}R:B {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}. (R\_f \mmember{} A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{})
Date html generated:
2016_10_21-AM-09_44_07
Last ObjectModification:
2016_08_08-PM-09_03_12
Theory : quot_1
Home
Index