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


1. coSet{i:l}
2. coSet{i:l}
3. coSet{i:l}
4. (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)
8. coSet{i:l}
9. pr coSet{i:l}
10. x:coSet{i:l} × (x ∈ b)
11. seteq(pr;(fst(p),f p))
12. seteq(z;snd(pr))
⊢ seteq(z;f p)
BY
((RWO "-1" THENA Auto) THEN (RWO "-2" THENA Auto)) }

1
1. coSet{i:l}
2. coSet{i:l}
3. coSet{i:l}
4. (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)
8. coSet{i:l}
9. pr coSet{i:l}
10. x:coSet{i:l} × (x ∈ b)
11. seteq(pr;(fst(p),f p))
12. seteq(z;snd(pr))
⊢ seteq(snd((fst(p),f p));f p)


Latex:


Latex:

1.  A  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  (z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
5.  \mforall{}z1,z2:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2))
6.  seteq(A;set-image(f;b))
7.  (A  \msubseteq{}  x)
8.  z  :  coSet\{i:l\}
9.  pr  :  coSet\{i:l\}
10.  p  :  x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b)
11.  seteq(pr;(fst(p),f  p))
12.  seteq(z;snd(pr))
\mvdash{}  seteq(z;f  p)


By


Latex:
((RWO  "-1"  0  THENA  Auto)  THEN  (RWO  "-2"  0  THENA  Auto))




Home Index