---

Step * 1 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])
⊢ ∀a:A. ∀b:B.  P[<a, b>]
BY
{ ((BHyp 3 THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto)) THEN BHyp 6  THEN Auto) }

1
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>])
⊢ P[<j, j1>]

---

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])
\mvdash{}  \mforall{}a:A.  \mforall{}b:B.    P[<a,  b>]


By

---

Latex:
((BHyp  3  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto))  THEN  BHyp  6    THEN  Auto)

---

Home Index