Step
*
1
1
1
of Lemma
page55'
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]@i
8. y = (f x) ∈ (P[x] ⇒ Q[x])
9. y1 : P[x]@i
10. y1 = (g x) ∈ P[x]
⊢ Q[x]
BY
{ D 7 }
1
.....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]
2
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]
11. Q[x]@i
⊢ Q[x]
Latex:
Latex:
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]@i
8. y = (f x)
9. y1 : P[x]@i
10. y1 = (g x)
\mvdash{} Q[x]
By
Latex:
D 7
Home
Index