---

Step * 2 1 1 1 of Lemma setmem-image


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. x1 : coSet{i:l}
7. t : T
8. x3 : seteq(x1;b1 t)
9. seteq(y;f <x1, t, x3>)
10. <t, x3> ∈ (x1 ∈ mk-coset(T;b1))
⊢ seteq(y;f <b1 t, mem-mk-set(b1;t)>)
BY
{ (InstLemma `seteqweaken_wf` [⌜b1 t⌝;⌜b1 t⌝]⋅ THENA Auto) }

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. x1 : coSet{i:l}
7. t : T
8. x3 : seteq(x1;b1 t)
9. seteq(y;f <x1, t, x3>)
10. <t, x3> ∈ (x1 ∈ mk-coset(T;b1))
11. seteqweaken(b1 t) ∈ ((b1 t) = (b1 t) ∈ coSet{i:l}) ⇒ seteq(b1 t;b1 t)
⊢ seteq(y;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.  x1  :  coSet\{i:l\}
7.  t  :  T
8.  x3  :  seteq(x1;b1  t)
9.  seteq(y;f  <x1,  t,  x3>)
10.  <t,  x3>  \mmember{}  (x1  \mmember{}  mk-coset(T;b1))
\mvdash{}  seteq(y;f  <b1  t,  mem-mk-set(b1;t)>)


By

---

Latex:
(InstLemma  `seteqweaken\_wf`  [\mkleeneopen{}b1  t\mkleeneclose{};\mkleeneopen{}b1  t\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index