Step
*
2
of Lemma
filter_is_singleton2
.....falsecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ||filter(P;v)|| = 1 ∈ ℤ 
⇐⇒ ∃i:ℕ||v||. ((↑(P v[i])) ∧ (∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])))
6. ¬↑(P u)
⊢ ||filter(P;v)|| = 1 ∈ ℤ 
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))
BY
{ (ParallelOp (-2) THEN ExRepD) }
1
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ¬↑(P u)
6. ||filter(P;v)|| = 1 ∈ ℤ
7. i : ℕ||v||
8. ↑(P v[i])
9. ∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])
⊢ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))
2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ¬↑(P u)
6. i : ℕ||v|| + 1
7. ↑(P [u / v][i])
8. ∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])
⊢ ∃i:ℕ||v||. ((↑(P v[i])) ∧ (∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])))
Latex:
Latex:
.....falsecase..... 
1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  ||filter(P;v)||  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(P  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}||v||.  i  =  j  supposing  \muparrow{}(P  v[j])))
6.  \mneg{}\muparrow{}(P  u)
\mvdash{}  ||filter(P;v)||  =  1
\mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}(P  [u  /  v][i]))  \mwedge{}  (\mforall{}j:\mBbbN{}||v||  +  1.  i  =  j  supposing  \muparrow{}(P  [u  /  v][j])))
By
Latex:
(ParallelOp  (-2)  THEN  ExRepD)
Home
Index