---

Step * 1 2 of Lemma product_well_fnd


1. [A] : Type
2. [B] : Type
3. [Ra] : A ⟶ A ⟶ ℙ
4. [Rb] : B ⟶ B ⟶ ℙ
5. ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (Ra[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:A. P[n]})
6. ∀[P:B ⟶ ℙ]. ((∀j:B. ((∀k:B. (Rb[k;j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:B. P[n]})
7. [P] : (A × B) ⟶ ℙ
8. ∀j:A × B. ((∀k:A × B. (let a1,b1 = k in let a2,b2 = j in Ra[a1;a2] ∨ ((a1 = a2 ∈ A) ∧ Rb[b1;b2]) ⇒ P[k])) ⇒ P[j])
9. ∀n:A. ∀b:B.  P[<n, b>]
⊢ {∀n:A × B. P[n]}
BY
{ ((D 0 THEN Auto) THEN D -1 THEN BHyp 9 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [Ra]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  [Rb]  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:A.  ((\mforall{}k:A.  (Ra[k;j]  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j]))  {}\mRightarrow{}  \{\mforall{}n:A.  P[n]\})
6.  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}j:B.  ((\mforall{}k:B.  (Rb[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.  (let  a1,b1  =  k  in  let  a2,b2  =  j  in  Ra[a1;a2]  \mvee{}  ((a1  =  a2)  \mwedge{}  Rb[b1;b2])  {}\mRightarrow{}  P[k]))
          {}\mRightarrow{}  P[j])
9.  \mforall{}n:A.  \mforall{}b:B.    P[<n,  b>]
\mvdash{}  \{\mforall{}n:A  \mtimes{}  B.  P[n]\}


By

---

Latex:
((D  0  THEN  Auto)  THEN  D  -1  THEN  BHyp  9  THEN  Auto)

---

Home Index