---

Step * of Lemma relclosed-iff-funclosed

∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ
  ((∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y)))
  ⇒ (∃f:Set{i:l} ⟶ Set{i:l}. ∀s:Set{i:l}. (closed(x,a.R[x;a])s ⇐⇒ f-closed(s))))
BY
{ (Auto THEN (Skolemize (-1) `f' THENA Auto) THEN (D 0 With ⌜f⌝  THENA Auto) THEN (D 0 THENA Auto)) }

1
1. R : Set{i:l} ⟶ Set{i:l} ⟶ ℙ
2. ∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y))
3. f : x:Set{i:l} ⟶ Set{i:l}
4. ∀x,a:Set{i:l}.  (R[x;a] ⇐⇒ (a ∈ f x))
5. s : Set{i:l}
⊢ closed(x,a.R[x;a])s ⇐⇒ f-closed(s)

---

Latex:

---

Latex:
\mforall{}R:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}
    ((\mforall{}x:Set\{i:l\}.  \mexists{}y:Set\{i:l\}.  \mforall{}a:Set\{i:l\}.  (R[x;a]  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  y)))
    {}\mRightarrow{}  (\mexists{}f:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}.  \mforall{}s:Set\{i:l\}.  (closed(x,a.R[x;a])s  \mLeftarrow{}{}\mRightarrow{}  f-closed(s))))


By

---

Latex:
(Auto  THEN  (Skolemize  (-1)  `f'  THENA  Auto)  THEN  (D  0  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index