---

Step * 2 of Lemma setmem-sub-coset


1. T : Type
2. s1 : T ⟶ coSet{i:l}
3. [P] : {a:coSet{i:l}| ∃b:T. seteq(a;s1 b)}  ⟶ ℙ
4. set-predicate{i:l}(<T, s1>;a.P[a])
5. a : coSet{i:l}
6. b : T
7. seteq(a;s1 b)
8. P[a]
⊢ ∃b:t:T × P[s1 t]. seteq(a;s1 (fst(b)))
BY
{ (Unfold `set-predicate` 4
   THEN ((FHyp 4 [-2] THEN Auto)
         THENA (Fold `mk-coset` 0
                THEN (RWO "setmem-iff" 0 THEN Auto)
                THEN RepUR ``mk-coset set-dom set-item`` 0
                THEN Auto)
         )
   ) }

1
1. T : Type
2. s1 : T ⟶ coSet{i:l}
3. [P] : {a:coSet{i:l}| ∃b:T. seteq(a;s1 b)}  ⟶ ℙ
4. ∀a1,a2:coSet{i:l}.  ((a1 ∈ <T, s1>) ⇒ (a2 ∈ <T, s1>) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2])
5. a : coSet{i:l}
6. b : T
7. seteq(a;s1 b)
8. P[a]
9. P[s1 b]
⊢ ∃b:t:T × P[s1 t]. seteq(a;s1 (fst(b)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  s1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  [P]  :  \{a:coSet\{i:l\}|  \mexists{}b:T.  seteq(a;s1  b)\}    {}\mrightarrow{}  \mBbbP{}
4.  set-predicate\{i:l\}(<T,  s1>a.P[a])
5.  a  :  coSet\{i:l\}
6.  b  :  T
7.  seteq(a;s1  b)
8.  P[a]
\mvdash{}  \mexists{}b:t:T  \mtimes{}  P[s1  t].  seteq(a;s1  (fst(b)))


By

---

Latex:
(Unfold  `set-predicate`  4
  THEN  ((FHyp  4  [-2]  THEN  Auto)
              THENA  (Fold  `mk-coset`  0
                            THEN  (RWO  "setmem-iff"  0  THEN  Auto)
                            THEN  RepUR  ``mk-coset  set-dom  set-item``  0
                            THEN  Auto)
              )
  )

---

Home Index