Nuprl Lemma : coset-relation-setrel
∀R:coSet{i:l}. coSetRelation(setrel(R))
Proof
Definitions occuring in Statement :
setrel: setrel(R),
coset-relation: coSetRelation(R),
coSet: coSet{i:l},
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
setrel: setrel(R),
coset-relation: coSetRelation(R),
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
prop: ℙ
Lemmas referenced :
setmem_functionality_1,
orderedpairset_wf,
orderedpairset_functionality,
seteq_weakening,
seteq_inversion,
setmem_wf,
seteq_wf,
coSet_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
hypothesis,
independent_functionElimination,
because_Cache,
productElimination,
universeIsType,
inhabitedIsType
Latex:
\mforall{}R:coSet\{i:l\}. coSetRelation(setrel(R))
Date html generated:
2020_05_20-PM-01_19_14
Last ObjectModification:
2020_01_06-PM-01_23_37
Theory : constructive!set!theory
Home
Index