Nuprl Lemma : dep-isect_wf
∀A:𝕌'. ∀B:A ⟶ 𝕌'. (x:A ⋂ B[x] ∈ 𝕌')
Proof
Definitions occuring in Statement :
dep-isect: x:A ⋂ B[x],
so_apply: x[s],
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
so_apply: x[s]
Rules used in proof :
universeEquality,
hypothesisEquality,
cumulativity,
functionEquality,
hypothesis,
sqequalHypSubstitution,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
dependentIntersectionEquality,
applyEquality
Latex:
\mforall{}A:\mBbbU{}'. \mforall{}B:A {}\mrightarrow{} \mBbbU{}'. (x:A \mcap{} B[x] \mmember{} \mBbbU{}')
Date html generated:
2019_06_20-PM-00_35_01
Last ObjectModification:
2019_01_11-PM-03_19_39
Theory : dependent!intersection
Home
Index