---

Step * 1 1 of Lemma setmem-fun-graph


1. T : Type
2. b1 : T ⟶ coSet{i:l}
3. f : (x:coSet{i:l} × (x ∈ <T, b1>)) ⟶ coSet{i:l}
4. ∀z1,z2:x:coSet{i:l} × (x ∈ <T, b1>).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
5. y : coSet{i:l}
6. t : set-dom(<T, λt.(b1 t,f <b1 t, mem-mk-set(b1;t)>)>)
7. seteq(y;set-item(<T, λt.(b1 t,f <b1 t, mem-mk-set(b1;t)>)>;t))
⊢ ∃p:x:coSet{i:l} × (x ∈ <T, b1>). seteq(y;(fst(p),f p))
BY
{ (RepUR ``set-item`` -1 THEN RepUR ``set-dom`` -2) }

1
1. T : Type
2. b1 : T ⟶ coSet{i:l}
3. f : (x:coSet{i:l} × (x ∈ <T, b1>)) ⟶ coSet{i:l}
4. ∀z1,z2:x:coSet{i:l} × (x ∈ <T, b1>).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
5. y : coSet{i:l}
6. t : T
7. seteq(y;(b1 t,f <b1 t, mem-mk-set(b1;t)>))
⊢ ∃p:x:coSet{i:l} × (x ∈ <T, b1>). seteq(y;(fst(p),f p))

---

Latex:

---

Latex:

1.  T  :  Type
2.  b1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  f  :  (x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  <T,  b1>))  {}\mrightarrow{}  coSet\{i:l\}
4.  \mforall{}z1,z2:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  <T,  b1>).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2))
5.  y  :  coSet\{i:l\}
6.  t  :  set-dom(<T,  \mlambda{}t.(b1  t,f  <b1  t,  mem-mk-set(b1;t)>)>)
7.  seteq(y;set-item(<T,  \mlambda{}t.(b1  t,f  <b1  t,  mem-mk-set(b1;t)>)>t))
\mvdash{}  \mexists{}p:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  <T,  b1>).  seteq(y;(fst(p),f  p))


By

---

Latex:
(RepUR  ``set-item``  -1  THEN  RepUR  ``set-dom``  -2)

---

Home Index