---

Step * of Lemma set-predicate-iff

∀[s:Set{i:l}]. ∀[P:{x:Set{i:l}| (x ∈ s)}  ⟶ ℙ'].
  (set-predicate{i:l}(s;x.P[x]) ⇐⇒ ∀a1,a2:Set{i:l}.  ((a1 ∈ s) ⇒ (a2 ∈ s) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2]))
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. [s] : Set{i:l}
2. [P] : {x:Set{i:l}| (x ∈ s)}  ⟶ ℙ'
3. set-predicate{i:l}(s;x.P[x])
⊢ ∀a1,a2:Set{i:l}.  ((a1 ∈ s) ⇒ (a2 ∈ s) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2])

2
1. [s] : Set{i:l}
2. [P] : {x:Set{i:l}| (x ∈ s)}  ⟶ ℙ'
3. ∀a1,a2:Set{i:l}.  ((a1 ∈ s) ⇒ (a2 ∈ s) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2])
⊢ set-predicate{i:l}(s;x.P[x])

---

Latex:

---

Latex:
\mforall{}[s:Set\{i:l\}].  \mforall{}[P:\{x:Set\{i:l\}|  (x  \mmember{}  s)\}    {}\mrightarrow{}  \mBbbP{}'].
    (set-predicate\{i:l\}(s;x.P[x])
    \mLeftarrow{}{}\mRightarrow{}  \mforall{}a1,a2:Set\{i:l\}.    ((a1  \mmember{}  s)  {}\mRightarrow{}  (a2  \mmember{}  s)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  P[a1]  {}\mRightarrow{}  P[a2]))


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index