Step
*
1
1
of Lemma
page55-again
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. ∀x:U. (P x)@i
5. x : U@i
6. (P x) 
⇒ (Q x)@i
⊢ Q x
BY
{ D 6 }
1
.....antecedent..... 
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. ∀x:U. (P x)@i
5. x : U@i
⊢ P x
2
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. ∀x:U. (P x)@i
5. x : U@i
6. Q x@i
⊢ Q x
Latex:
Latex:
1.  U  :  Type@i'
2.  P  :  U  {}\mrightarrow{}  \mBbbP{}@i'
3.  Q  :  U  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mforall{}x:U.  (P  x)@i
5.  x  :  U@i
6.  (P  x)  {}\mRightarrow{}  (Q  x)@i
\mvdash{}  Q  x
By
Latex:
D  6
Home
Index