Step
*
of Lemma
exists_functionality_wrt_implies
∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ]. (∀x:S. {P[x]
⇒ Q[x]})
⇒ {(∃x:S. P[x])
⇒ (∃y:T. Q[y])} supposing S = T ∈ Type
BY
{ ((Unfold `guard` 0 THEN UnivCD) THENA Auto) }
1
1. [S] : Type
2. [T] : Type
3. [P] : S ⟶ ℙ
4. [Q] : S ⟶ ℙ
5. S = T ∈ Type
6. ∀x:S. (P[x]
⇒ Q[x])@i
7. ∃x:S. P[x]@i
⊢ ∃y:T. Q[y]
Latex:
Latex:
\mforall{}[S,T:Type]. \mforall{}[P,Q:S {}\mrightarrow{} \mBbbP{}].
(\mforall{}x:S. \{P[x] {}\mRightarrow{} Q[x]\}) {}\mRightarrow{} \{(\mexists{}x:S. P[x]) {}\mRightarrow{} (\mexists{}y:T. Q[y])\} supposing S = T
By
Latex:
((Unfold `guard` 0 THEN UnivCD) THENA Auto)
Home
Index