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


1. coSet{i:l}
2. coSet{i:l}
3. coSet{i:l}
4. 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))))
9. ∀p:z:coSet{i:l} × (z ∈ b). ∃b:coSet{i:l}. ((b ∈ x) ∧ ((fst(p),b) ∈ f))
10. p:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
11. ∀p:z:coSet{i:l} × (z ∈ b). ((g p ∈ x) ∧ ((fst(p),g p) ∈ f))
12. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2))  seteq(g z1;g z2))
13. coSet{i:l}
14. pr coSet{i:l}
15. (pr ∈ f)
16. seteq(z;snd(pr))
⊢ ∃x:x:coSet{i:l} × (x ∈ b). seteq(snd(pr);g x)
BY
(((RWO  "setsubset-iff" THENA Auto) THEN (InstHyp [⌜pr⌝5⋅ THENA Auto))
   THEN (RWO "setmem-sigmaset" (-1) THENA Auto)
   THEN ExRepD) }

1
1. coSet{i:l}
2. coSet{i:l}
3. coSet{i:l}
4. 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. ∀p:z:coSet{i:l} × (z ∈ b). ∃b:coSet{i:l}. ((b ∈ x) ∧ ((fst(p),b) ∈ f))
10. p:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
11. ∀p:z:coSet{i:l} × (z ∈ b). ((g p ∈ x) ∧ ((fst(p),g p) ∈ f))
12. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2))  seteq(g z1;g z2))
13. coSet{i:l}
14. pr coSet{i:l}
15. (pr ∈ f)
16. seteq(z;snd(pr))
17. coSet{i:l}
18. (_ ∈ b)
19. b1 coSet{i:l}
20. (b1 ∈ x)
21. seteq(pr;(_,b1))
⊢ ∃x:x:coSet{i:l} × (x ∈ b). seteq(snd(pr);g x)


Latex:


Latex:

1.  A  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  coSet\{i:l\}
5.  (f  \msubseteq{}  \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.  \mforall{}p:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).  \mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  x)  \mwedge{}  ((fst(p),b)  \mmember{}  f))
10.  g  :  p:(z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
11.  \mforall{}p:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).  ((g  p  \mmember{}  x)  \mwedge{}  ((fst(p),g  p)  \mmember{}  f))
12.  \mforall{}z1,z2:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(g  z1;g  z2))
13.  z  :  coSet\{i:l\}
14.  pr  :  coSet\{i:l\}
15.  (pr  \mmember{}  f)
16.  seteq(z;snd(pr))
\mvdash{}  \mexists{}x:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).  seteq(snd(pr);g  x)


By


Latex:
(((RWO    "setsubset-iff"  5  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}pr\mkleeneclose{}]  5\mcdot{}  THENA  Auto))
  THEN  (RWO  "setmem-sigmaset"  (-1)  THENA  Auto)
  THEN  ExRepD)




Home Index