---

Step * 1 of Lemma page55'


1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. f : ∀x:U. (P[x] ⇒ Q[x])@i
5. g : ∀x:U. P[x]@i
6. x : U@i
⊢ Q[x]
BY
{ (With ⌜x⌝ (D 4)⋅ THENA Auto) }

1
1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. f : x:U ⟶ (P[x] ⇒ Q[x])
5. g : ∀x:U. P[x]@i
6. x : U@i
7. y : P[x] ⇒ Q[x]@i
8. y = (f x) ∈ (P[x] ⇒ Q[x])
⊢ Q[x]

---

Latex:

---

Latex:

1.  [U]  :  Type
2.  [P]  :  U  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  U  {}\mrightarrow{}  \mBbbP{}
4.  f  :  \mforall{}x:U.  (P[x]  {}\mRightarrow{}  Q[x])@i
5.  g  :  \mforall{}x:U.  P[x]@i
6.  x  :  U@i
\mvdash{}  Q[x]


By

---

Latex:
(With  \mkleeneopen{}x\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)

---

Home Index