---

Step * 1 of Lemma inductive-set-property


1. [R] : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
2. b1 : ∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ R[x1;a1] ⇒ R[x2;a2])
3. b3 : ∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y))
4. B : Set{i:l}
5. b5 : ∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
6. x : Set{i:l}
7. z : Set{i:l}
⊢ (z ∈ closure-set(B;λz.(fst((b3 z)));x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])
BY
{ (Assert ∀x,a:Set{i:l}.  (R[x;a] ⇐⇒ (a ∈ (λz.(fst((b3 z)))) x)) BY
         (Reduce 0 THEN (D 0 THENA Auto) THEN (GenConclTerm ⌜b3 x1⌝⋅ THENA Auto) THEN (D -2 THEN Reduce 0) THEN Auto)) }

1
1. [R] : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
2. b1 : ∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ R[x1;a1] ⇒ R[x2;a2])
3. b3 : ∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y))
4. B : Set{i:l}
5. b5 : ∀x,a:Set{i:l}.  (R[x;a] ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
6. x : Set{i:l}
7. z : Set{i:l}
8. ∀x,a:Set{i:l}.  (R[x;a] ⇐⇒ (a ∈ (λz.(fst((b3 z)))) x))
⊢ (z ∈ closure-set(B;λz.(fst((b3 z)));x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])

---

Latex:

---

Latex:

1.  [R]  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
2.  b1  :  \mforall{}x1,x2,a1,a2:Set\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  R[x1;a1]  {}\mRightarrow{}  R[x2;a2])
3.  b3  :  \mforall{}x:Set\{i:l\}.  \mexists{}y:Set\{i:l\}.  \mforall{}a:Set\{i:l\}.  (R[x;a]  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  y))
4.  B  :  Set\{i:l\}
5.  b5  :  \mforall{}x,a:Set\{i:l\}.    (R[x;a]  {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  setimage\{i:l\}(x;b))))
6.  x  :  Set\{i:l\}
7.  z  :  Set\{i:l\}
\mvdash{}  (z  \mmember{}  closure-set(B;\mlambda{}z.(fst((b3  z)));x))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}A:Set\{i:l\}.  ((A  \msubseteq{}  x)  \mwedge{}  R[A;z])


By

---

Latex:
(Assert  \mforall{}x,a:Set\{i:l\}.    (R[x;a]  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  (\mlambda{}z.(fst((b3  z))))  x))  BY
              (Reduce  0
                THEN  (D  0  THENA  Auto)
                THEN  (GenConclTerm  \mkleeneopen{}b3  x1\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (D  -2  THEN  Reduce  0)
                THEN  Auto))

---

Home Index