---

Step * 2 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. x : coSet{i:l}
7. p1 : (x ∈ <T, b1>)
8. seteq(y;(x,f <x, p1>))
⊢ ∃t:T. seteq(y;(b1 t,f <b1 t, mem-mk-set(b1;t)>))
BY
{ ((Assert p1 ∈ (x ∈ <T, b1>) BY
          Declaration)
   THEN Fold `mk-coset` (-3)
   THEN (RWO "setmem-mk-coset" (-3) THENA Auto)
   THEN ParallelOp -3) }

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. x : coSet{i:l}
7. t : T
8. p2 : seteq(x;b1 t)
9. seteq(y;(x,f <x, t, p2>))
10. <t, p2> ∈ (x ∈ <T, b1>)
⊢ seteq(y;(b1 t,f <b1 t, mem-mk-set(b1;t)>))

---

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.  x  :  coSet\{i:l\}
7.  p1  :  (x  \mmember{}  <T,  b1>)
8.  seteq(y;(x,f  <x,  p1>))
\mvdash{}  \mexists{}t:T.  seteq(y;(b1  t,f  <b1  t,  mem-mk-set(b1;t)>))


By

---

Latex:
((Assert  p1  \mmember{}  (x  \mmember{}  <T,  b1>)  BY
                Declaration)
  THEN  Fold  `mk-coset`  (-3)
  THEN  (RWO  "setmem-mk-coset"  (-3)  THENA  Auto)
  THEN  ParallelOp  -3)

---

Home Index