Nuprl Lemma : setmem-Piset
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A) 
⇒ (a2 ∈ A) 
⇒ seteq(a1;a2) 
⇒ seteq(B[a1];B[a2])))
  
⇒ ((x ∈ Πa:A.B[a]) 
⇐⇒ function-graph{i:l}(A;a.B[a];x)))
Proof
Definitions occuring in Statement : 
function-graph: function-graph{i:l}(A;a.B[a];grph)
, 
Piset: Πa:A.B[a]
, 
setmem: (x ∈ s)
, 
seteq: seteq(s1;s2)
, 
coSet: coSet{i:l}
, 
so_apply: x[s]
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
Definitions unfolded in proof : 
guard: {T}
, 
subtype_rel: A ⊆r B
, 
cand: A c∧ B
, 
function-graph: function-graph{i:l}(A;a.B[a];grph)
, 
set-predicate: set-predicate{i:l}(s;a.P[a])
, 
rev_implies: P 
⇐ Q
, 
so_apply: x[s]
, 
so_lambda: λ2x.t[x]
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
member: t ∈ T
, 
and: P ∧ Q
, 
iff: P 
⇐⇒ Q
, 
Piset: Πa:A.B[a]
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
Lemmas referenced : 
implies-setmem-piset, 
Set_wf, 
set-subtype-coSet, 
orderedpairset_wf, 
singlevalued-graph-iff, 
setmem-piset-implies, 
all_wf, 
iff_wf, 
sub-set_wf, 
seteq_wf, 
singlevalued-graph_functionality, 
setmem-sub-coset, 
function-graph_wf, 
singlevalued-graph_wf, 
coSet_wf, 
piset_wf, 
setmem_wf
Rules used in proof : 
because_Cache, 
dependent_set_memberEquality, 
functionEquality, 
instantiate, 
independent_functionElimination, 
rename, 
setElimination, 
impliesFunctionality, 
productElimination, 
addLevel, 
dependent_functionElimination, 
cumulativity, 
hypothesis, 
setEquality, 
applyEquality, 
lambdaEquality, 
sqequalRule, 
hypothesisEquality, 
thin, 
isectElimination, 
sqequalHypSubstitution, 
extract_by_obid, 
introduction, 
productEquality, 
independent_pairFormation, 
cut, 
lambdaFormation, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution
Latex:
\mforall{}A:coSet\{i:l\}.  \mforall{}B:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}.  \mforall{}x:coSet\{i:l\}.
    ((\mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2])))
    {}\mRightarrow{}  ((x  \mmember{}  \mPi{}a:A.B[a])  \mLeftarrow{}{}\mRightarrow{}  function-graph\{i:l\}(A;a.B[a];x)))
Date html generated:
2018_07_29-AM-10_05_19
Last ObjectModification:
2018_07_18-PM-04_38_54
Theory : constructive!set!theory
Home
Index