---

Step * 2 of Lemma sys-antecedent-filter-image

.....set predicate..... 
1. Info : Type
2. A : Type
3. B : Type
4. g : A ─→ bag(B)
5. es : EO+(Info)
6. X : EClass(A)
7. f : E(X) ─→ E(X)
8. ∀x:E(X). f x c≤ x
9. ∀a:E(X). ((¬((f a) = a ∈ E(X))) ⇒ (#(g X(a)) = 1 ∈ ℤ) ⇒ (#(g X(f a)) = 1 ∈ ℤ))
⊢ ∀x:E(g[X]). f x c≤ x
BY
{ (Auto THEN BackThruSomeHyp THEN DoSubsume THEN Auto THEN BLemma `es-E-filter-image` THEN Auto)⋅ }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  g  :  A  {}\mrightarrow{}  bag(B)
5.  es  :  EO+(Info)
6.  X  :  EClass(A)
7.  f  :  E(X)  {}\mrightarrow{}  E(X)
8.  \mforall{}x:E(X).  f  x  c\mleq{}  x
9.  \mforall{}a:E(X).  ((\mneg{}((f  a)  =  a))  {}\mRightarrow{}  (\#(g  X(a))  =  1)  {}\mRightarrow{}  (\#(g  X(f  a))  =  1))
\mvdash{}  \mforall{}x:E(g[X]).  f  x  c\mleq{}  x


By

---

Latex:
(Auto  THEN  BackThruSomeHyp  THEN  DoSubsume  THEN  Auto  THEN  BLemma  `es-E-filter-image`  THEN  Auto)\mcdot{}

---

Home Index