---

Step * 1 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])
⊢ {∀n:A × B. P[n]}
BY
{ (InstHyp [⌜λ2a.∀b:B. P[<a, b>]⌝] 5⋅ THENA Auto) }

1
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. j : A@i
10. ∀k:A. (Ra[k;j] ⇒ (∀b:B. P[<k, b>]))
11. b : B@i
⊢ P[<j, b>]

2
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]}

---

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


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}a.\mforall{}b:B.  P[<a,  b>]\mkleeneclose{}]  5\mcdot{}  THENA  Auto)

---

Home Index