Step
*
of Lemma
not_over_exists
∀[T:Type]. ∀[Q:T ⟶ ℙ].  uiff(¬(∃x:T. Q[x]);∀x:T. (¬Q[x]))
BY
{ (GenRepD THENA Auto) }
1
1. T : Type
2. Q : T ⟶ ℙ
3. ¬(∃x:T. Q[x])
4. x : T
⊢ ¬Q[x]
2
1. T : Type
2. Q : T ⟶ ℙ
3. ∀x:T. (¬Q[x])
⊢ ¬(∃x:T. Q[x])
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].    uiff(\mneg{}(\mexists{}x:T.  Q[x]);\mforall{}x:T.  (\mneg{}Q[x]))
By
Latex:
(GenRepD  THENA  Auto)
Home
Index