---

Step * of Lemma setmem-setimages-2

No Annotations
∀A,b,x:coSet{i:l}.  ((A ∈ setimages(b;x)) ⇐⇒ setimage{i:l}(A;b) ∧ (A ⊆ x))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "setmem-setimages setimage-iff" 0 THENA Auto)
   THEN Auto
   THEN ExRepD
   THEN ∀h:hyp. (Unfold `function-graph` h THEN ExRepD) ) }

1
1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. (f ⊆ Σ_: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))))
⊢ ∃f:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
   ((∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))) ∧ seteq(A;set-image(f;b)))

2
1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. (f ⊆ Σ_: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))))
⊢ (A ⊆ x)

3
1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : (z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
5. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
6. seteq(A;set-image(f;b))
7. (A ⊆ x)
⊢ ∃f:coSet{i:l}
   (function-graph{i:l}(b;_.x;f) ∧ (∀z:coSet{i:l}. ((z ∈ A) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}A,b,x:coSet\{i:l\}.    ((A  \mmember{}  setimages(b;x))  \mLeftarrow{}{}\mRightarrow{}  setimage\{i:l\}(A;b)  \mwedge{}  (A  \msubseteq{}  x))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "setmem-setimages  setimage-iff"  0  THENA  Auto)
  THEN  Auto
  THEN  ExRepD
  THEN  \mforall{}h:hyp.  (Unfold  `function-graph`  h  THEN  ExRepD)  )

---

Home Index