---

Step * 1 1 1 1 of Lemma page55'

.....antecedent..... 
1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. f : x:U ⟶ (P[x] ⇒ Q[x])
5. g : x:U ⟶ P[x]
6. x : U@i
7. y : P[x] ⟶ Q[x]
8. y = (f x) ∈ (P[x] ⇒ Q[x])
9. y1 : P[x]@i
10. y1 = (g x) ∈ P[x]
⊢ P[x]
BY
{ Auto }

---

Latex:

---

Latex:
.....antecedent..... 
1.  [U]  :  Type
2.  [P]  :  U  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  U  {}\mrightarrow{}  \mBbbP{}
4.  f  :  x:U  {}\mrightarrow{}  (P[x]  {}\mRightarrow{}  Q[x])
5.  g  :  x:U  {}\mrightarrow{}  P[x]
6.  x  :  U@i
7.  y  :  P[x]  {}\mrightarrow{}  Q[x]
8.  y  =  (f  x)
9.  y1  :  P[x]@i
10.  y1  =  (g  x)
\mvdash{}  P[x]


By

---

Latex:
Auto

---

Home Index