---

Step * 1 of Lemma function-graph-fun-graph


1. b : coSet{i:l}
2. f : (x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}
3. ∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
4. x : coSet{i:l}
5. (set-image(f;b) ⊆ x)
6. ∀p:x:coSet{i:l} × (x ∈ b). (f p ∈ x)
⊢ (fun-graph(b;f) ⊆ Σ_:b.x)
BY
{ ((RWW "setsubset-iff setmem-fun-graph setmem-sigmaset" 0 THEN Auto) THEN ExRepD) }

1
1. b : coSet{i:l}
2. f : (x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}
3. ∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
4. x : coSet{i:l}
5. (set-image(f;b) ⊆ x)
6. ∀p:x:coSet{i:l} × (x ∈ b). (f p ∈ x)
7. x1 : coSet{i:l}
8. p : x:coSet{i:l} × (x ∈ b)
9. seteq(x1;(fst(p),f p))
⊢ ∃_:coSet{i:l}. ((_ ∈ b) ∧ (∃b:coSet{i:l}. ((b ∈ x) ∧ seteq(x1;(_,b)))))

---

Latex:

---

Latex:

1.  b  :  coSet\{i:l\}
2.  f  :  (x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
3.  \mforall{}z1,z2:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2))
4.  x  :  coSet\{i:l\}
5.  (set-image(f;b)  \msubseteq{}  x)
6.  \mforall{}p:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).  (f  p  \mmember{}  x)
\mvdash{}  (fun-graph(b;f)  \msubseteq{}  \mSigma{}$_{}$:b.x)


By

---

Latex:
((RWW  "setsubset-iff  setmem-fun-graph  setmem-sigmaset"  0  THEN  Auto)  THEN  ExRepD)

---

Home Index