---

Step * 1 1 1 of Lemma W-uwellfounded_witness


1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
5. a : A
6. f1 : B[a] ⟶ W(A;a.B[a])
7. ∀w:W(A;a.B[a]). ((w <  Wsup(a;f1)) ⇒ (fix(f) ∈ P[w]))
8. w : W(A;a.B[a])
9. v : w ≤  Wsup(a;f1)
⊢ f fix(f) ∈ P[w]
BY
{ (Assert fix(f) ∈ ⋂k:{k:W(A;a.B[a])| k <  w} . P[k] BY
         (ProveMemberIsect
          THEN Auto
          THEN D -1
          THEN BackThruSomeHyp
          THEN Using [`w2',⌜w⌝] (BLemma `Wcmp_transitivity`)⋅
          THEN Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
5. a : A
6. f1 : B[a] ⟶ W(A;a.B[a])
7. ∀w:W(A;a.B[a]). ((w <  Wsup(a;f1)) ⇒ (fix(f) ∈ P[w]))
8. w : W(A;a.B[a])
9. v : w ≤  Wsup(a;f1)
10. fix(f) ∈ ⋂k:{k:W(A;a.B[a])| k <  w} . P[k]
⊢ f fix(f) ∈ P[w]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  P  :  W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}
4.  f  :  \mcap{}j:W(A;a.B[a]).  ((\mcap{}k:\{k:W(A;a.B[a])|  k  <    j\}  .  P[k])  {}\mRightarrow{}  P[j])
5.  a  :  A
6.  f1  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
7.  \mforall{}w:W(A;a.B[a]).  ((w  <    Wsup(a;f1))  {}\mRightarrow{}  (fix(f)  \mmember{}  P[w]))
8.  w  :  W(A;a.B[a])
9.  v  :  w  \mleq{}    Wsup(a;f1)
\mvdash{}  f  fix(f)  \mmember{}  P[w]


By

---

Latex:
(Assert  fix(f)  \mmember{}  \mcap{}k:\{k:W(A;a.B[a])|  k  <    w\}  .  P[k]  BY
              (ProveMemberIsect
                THEN  Auto
                THEN  D  -1
                THEN  BackThruSomeHyp
                THEN  Using  [`w2',\mkleeneopen{}w\mkleeneclose{}]  (BLemma  `Wcmp\_transitivity`)\mcdot{}
                THEN  Auto))

---

Home Index