---

Step * of Lemma bl-exists-filter

∀[P,Q,L:Top].  ((∃x∈filter(P;L).Q[x])_b ~ (∃x∈L.(P x) ∧b Q[x])_b)
BY
{ ListIndSq `L' }

1
1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. (∃x∈r1.Q[x])_b ≤ r2
⊢ (∃x∈if P x then [x / r1] else r1 fi .Q[x])_b ≤ ((P x) ∧b Q[x]) ∨br2

2
1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. r1 ≤ (∃x∈r2.Q[x])_b
⊢ ((P x) ∧b Q[x]) ∨br1 ≤ (∃x∈if P x then [x / r2] else r2 fi .Q[x])_b

---

Latex:

---

Latex:
\mforall{}[P,Q,L:Top].    ((\mexists{}x\mmember{}filter(P;L).Q[x])\_b  \msim{}  (\mexists{}x\mmember{}L.(P  x)  \mwedge{}\msubb{}  Q[x])\_b)


By

---

Latex:
ListIndSq  `L'

---

Home Index