---

Step * 1 1 1 1 of Lemma setmem-piset-1


1. T : Type
2. f : T ⟶ coSet{i:l}
3. B : {a:coSet{i:l}| (a ∈ mk-coset(T;f))}  ⟶ coSet{i:l}
4. x : coSet{i:l}
5. b : t:T ⟶ set-dom(B[f t])
6. seteq(x;mk-coset(T;λt@0.(f t@0,set-item(B[f t@0];b t@0))))
7. ∀i:T. (f i ∈ {a:coSet{i:l}| (a ∈ mk-coset(T;f))} )
8. ∀i:T. (set-item(B[f i];b i) ∈ B[f i])
9. ∀i:T. (set-item(B[f i];b i) ∈ {b:coSet{i:l}| (b ∈ B[f i])} )
⊢ ∀z:coSet{i:l}. ((z ∈ mk-coset(T;λt@0.(f t@0,set-item(B[f t@0];b t@0)))) ⇐⇒ ∃t:T. seteq(z;(f t,set-item(B[f t];b t))))
BY
{ Auto }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. B : {a:coSet{i:l}| (a ∈ mk-coset(T;f))}  ⟶ coSet{i:l}
4. x : coSet{i:l}
5. b : t:T ⟶ set-dom(B[f t])
6. seteq(x;mk-coset(T;λt@0.(f t@0,set-item(B[f t@0];b t@0))))
7. ∀i:T. (f i ∈ {a:coSet{i:l}| (a ∈ mk-coset(T;f))} )
8. ∀i:T. (set-item(B[f i];b i) ∈ B[f i])
9. ∀i:T. (set-item(B[f i];b i) ∈ {b:coSet{i:l}| (b ∈ B[f i])} )
10. z : coSet{i:l}
11. (z ∈ mk-coset(T;λt@0.(f t@0,set-item(B[f t@0];b t@0))))
⊢ ∃t:T. seteq(z;(f t,set-item(B[f t];b t)))

2
1. T : Type
2. f : T ⟶ coSet{i:l}
3. B : {a:coSet{i:l}| (a ∈ mk-coset(T;f))}  ⟶ coSet{i:l}
4. x : coSet{i:l}
5. b : t:T ⟶ set-dom(B[f t])
6. seteq(x;mk-coset(T;λt@0.(f t@0,set-item(B[f t@0];b t@0))))
7. ∀i:T. (f i ∈ {a:coSet{i:l}| (a ∈ mk-coset(T;f))} )
8. ∀i:T. (set-item(B[f i];b i) ∈ B[f i])
9. ∀i:T. (set-item(B[f i];b i) ∈ {b:coSet{i:l}| (b ∈ B[f i])} )
10. z : coSet{i:l}
11. ∃t:T. seteq(z;(f t,set-item(B[f t];b t)))
⊢ (z ∈ mk-coset(T;λt@0.(f t@0,set-item(B[f t@0];b t@0))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  B  :  \{a:coSet\{i:l\}|  (a  \mmember{}  mk-coset(T;f))\}    {}\mrightarrow{}  coSet\{i:l\}
4.  x  :  coSet\{i:l\}
5.  b  :  t:T  {}\mrightarrow{}  set-dom(B[f  t])
6.  seteq(x;mk-coset(T;\mlambda{}t@0.(f  t@0,set-item(B[f  t@0];b  t@0))))
7.  \mforall{}i:T.  (f  i  \mmember{}  \{a:coSet\{i:l\}|  (a  \mmember{}  mk-coset(T;f))\}  )
8.  \mforall{}i:T.  (set-item(B[f  i];b  i)  \mmember{}  B[f  i])
9.  \mforall{}i:T.  (set-item(B[f  i];b  i)  \mmember{}  \{b:coSet\{i:l\}|  (b  \mmember{}  B[f  i])\}  )
\mvdash{}  \mforall{}z:coSet\{i:l\}
        ((z  \mmember{}  mk-coset(T;\mlambda{}t@0.(f  t@0,set-item(B[f  t@0];b  t@0))))
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:T.  seteq(z;(f  t,set-item(B[f  t];b  t))))


By

---

Latex:
Auto

---

Home Index