---

Step * 2 1 1 1 of Lemma setmem-setimages-2


1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. ∀x1:coSet{i:l}. ((x1 ∈ f) ⇒ (x1 ∈ Σ_:b.x))
6. ∀_:coSet{i:l}. ((_ ∈ b) ⇒ (∃b:coSet{i:l}. ((b ∈ x) ∧ ((_,b) ∈ f))))
7. ∀_,b1,b2:coSet{i:l}.  ((_ ∈ b) ⇒ (b1 ∈ x) ⇒ (b2 ∈ x) ⇒ ((_,b1) ∈ f) ⇒ ((_,b2) ∈ f) ⇒ seteq(b1;b2))
8. ∀z:coSet{i:l}. ((z ∈ A) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))
9. x1 : coSet{i:l}
10. pr : coSet{i:l}
11. (pr ∈ f)
12. seteq(x1;snd(pr))
13. (pr ∈ Σ_:b.x)
⊢ (snd(pr) ∈ x)
BY
{ ((RWO "setmem-sigmaset" (-1) THENA Auto) THEN ExRepD) }

1
1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. ∀x1:coSet{i:l}. ((x1 ∈ f) ⇒ (x1 ∈ Σ_:b.x))
6. ∀_:coSet{i:l}. ((_ ∈ b) ⇒ (∃b:coSet{i:l}. ((b ∈ x) ∧ ((_,b) ∈ f))))
7. ∀_,b1,b2:coSet{i:l}.  ((_ ∈ b) ⇒ (b1 ∈ x) ⇒ (b2 ∈ x) ⇒ ((_,b1) ∈ f) ⇒ ((_,b2) ∈ f) ⇒ seteq(b1;b2))
8. ∀z:coSet{i:l}. ((z ∈ A) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))
9. x1 : coSet{i:l}
10. pr : coSet{i:l}
11. (pr ∈ f)
12. seteq(x1;snd(pr))
13. _ : coSet{i:l}
14. (_ ∈ b)
15. b1 : coSet{i:l}
16. (b1 ∈ x)
17. seteq(pr;(_,b1))
⊢ (snd(pr) ∈ x)

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  coSet\{i:l\}
5.  \mforall{}x1:coSet\{i:l\}.  ((x1  \mmember{}  f)  {}\mRightarrow{}  (x1  \mmember{}  \mSigma{}$_{}$:b.x))
6.  \mforall{}$_{}$:coSet\{i:l\}.  (($_{}$  \mmember{}  b)  {}\mRightarrow{}  (\mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  \000Cx)  \mwedge{}  (($_{}$,b)  \mmember{}  f))))
7.  \mforall{}$_{}$,b1,b2:coSet\{i:l\}.
          (($_{}$  \mmember{}  b)  {}\mRightarrow{}  (b1  \mmember{}  x)  {}\mRightarrow{}  (b2  \mmember{}  x)  {}\mRightarrow{}  (($_{}$,b1)  \mmember{}  f\000C)  {}\mRightarrow{}  (($_{}$,b2)  \mmember{}  f)  {}\mRightarrow{}  seteq(b1;b2))
8.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  A)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(z;snd(pr))))
9.  x1  :  coSet\{i:l\}
10.  pr  :  coSet\{i:l\}
11.  (pr  \mmember{}  f)
12.  seteq(x1;snd(pr))
13.  (pr  \mmember{}  \mSigma{}$_{}$:b.x)
\mvdash{}  (snd(pr)  \mmember{}  x)


By

---

Latex:
((RWO  "setmem-sigmaset"  (-1)  THENA  Auto)  THEN  ExRepD)

---

Home Index