---

Step * 1 1 2 of Lemma wellfounded-lex


1. [A] : Type
2. [<A] : A ⟶ A ⟶ ℙ
3. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (<A[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:A. P[n]})
4. [B] : Type
5. [<B] : B ⟶ B ⟶ ℙ
6. ∀[P:B ⟶ ℙ]. ((∀j:B. ((∀k:B. (<B[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:B. P[n]})
7. [P] : (A × B) ⟶ ℙ
8. ∀j:A × B. ((∀k:A × B. ((<A[fst(k);fst(j)] ∨ (((fst(k)) = (fst(j)) ∈ A) ∧ <B[snd(k);snd(j)])) ⇒ P[k])) ⇒ P[j])
9. j : A
10. ∀k:A. (<A[k;j] ⇒ (∀b:B. P[<k, b>]))
11. j1 : B
12. ∀k:B. (<B[k;j1] ⇒ P[<j, k>])
13. k1 : A
14. k2 : B
15. (k1 = j ∈ A) ∧ <B[k2;j1]
⊢ P[<k1, k2>]
BY
{ xxx(D -1 THEN HypSubst' (-2) 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<A]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:A.  ((\mforall{}k:A.  (<A[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:A.  P[n]\})
4.  [B]  :  Type
5.  [<B]  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:B.  ((\mforall{}k:B.  (<B[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:B.  P[n]\})
7.  [P]  :  (A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}j:A  \mtimes{}  B
          ((\mforall{}k:A  \mtimes{}  B.  ((<A[fst(k);fst(j)]  \mvee{}  (((fst(k))  =  (fst(j)))  \mwedge{}  <B[snd(k);snd(j)]))  {}\mRightarrow{}  P[k]))
          {}\mRightarrow{}  P[j])
9.  j  :  A
10.  \mforall{}k:A.  (<A[k;j]  {}\mRightarrow{}  (\mforall{}b:B.  P[<k,  b>]))
11.  j1  :  B
12.  \mforall{}k:B.  (<B[k;j1]  {}\mRightarrow{}  P[<j,  k>])
13.  k1  :  A
14.  k2  :  B
15.  (k1  =  j)  \mwedge{}  <B[k2;j1]
\mvdash{}  P[<k1,  k2>]


By

---

Latex:
xxx(D  -1  THEN  HypSubst'  (-2)  0  THEN  Auto)xxx

---

Home Index