---

Step * of Lemma allsetmem_functionality

∀A:coSet{i:l}. ∀P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ. ∀B:coSet{i:l}.
  (set-predicate{i:l}(A;a.P[a]) ⇒ seteq(A;B) ⇒ (∀a∈A.P[a] ⇐⇒ ∀a∈B.P[a]))
BY
{ (RepeatFor 3 (Intro)
   THEN (D 0 THENA (UniverseIsType THEN Fold `member` 0 THEN BLemma `set-predicate_wf` THEN Auto))
   THEN Intro
   THEN (Assert set-predicate{i:l}(B;a.P[a]) BY
               (RepeatFor 2 (ParallelOp -2) THEN ParallelLast THEN RWO "5<" 0 THEN Auto))) }

1
1. A : coSet{i:l}
2. P : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. B : coSet{i:l}
4. set-predicate{i:l}(A;a.P[a])
5. seteq(A;B)
6. set-predicate{i:l}(B;a.P[a])
⊢ ∀a∈A.P[a] ⇐⇒ ∀a∈B.P[a]

---

Latex:

---

Latex:
\mforall{}A:coSet\{i:l\}.  \mforall{}P:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  \mBbbP{}.  \mforall{}B:coSet\{i:l\}.
    (set-predicate\{i:l\}(A;a.P[a])  {}\mRightarrow{}  seteq(A;B)  {}\mRightarrow{}  (\mforall{}a\mmember{}A.P[a]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}a\mmember{}B.P[a]))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (D  0  THENA  (UniverseIsType  THEN  Fold  `member`  0  THEN  BLemma  `set-predicate\_wf`  THEN  Auto))
  THEN  Intro
  THEN  (Assert  set-predicate\{i:l\}(B;a.P[a])  BY
                          (RepeatFor  2  (ParallelOp  -2)  THEN  ParallelLast  THEN  RWO  "5<"  0  THEN  Auto)))

---

Home Index