---

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


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 ∈ ℤ))
10. a : E(g[X])
⊢ f a ∈ E(g[X])
BY
{ (D (-1) THEN (RWO "es-is-filter-image" (-1) THENA Auto)) }

1
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 ∈ ℤ))
10. a : E
11. (↑a ∈b X) ∧ (#(g X(a)) = 1 ∈ ℤ)
⊢ f a ∈ E(g[X])

---

Latex:

---

Latex:

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))
10.  a  :  E(g[X])
\mvdash{}  f  a  \mmember{}  E(g[X])


By

---

Latex:
(D  (-1)  THEN  (RWO  "es-is-filter-image"  (-1)  THENA  Auto))

---

Home Index