---

Step * of Lemma sys-antecedent-filter-image

∀[Info,A,B:Type]. ∀[g:A ⟶ bag(B)]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[f:sys-antecedent(es;X)].
  f ∈ sys-antecedent(es;g[X]) supposing ∀a:E(X). ((¬((f a) = a ∈ E(X))) ⇒ (#(g X(a)) = 1 ∈ ℤ) ⇒ (#(g X(f a)) = 1 ∈ ℤ))
BY
{ ((UnivCD THENA Auto) THEN D -2 THEN Unfold `sys-antecedent` 0 THEN MemTypeCD) }

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 ∈ ℤ))
⊢ f ∈ E(g[X]) ⟶ E(g[X])

2
.....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

3
.....wf..... 
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. f1 : E(g[X]) ⟶ E(g[X])
⊢ ∀x:E(g[X]). f1 x c≤ x ∈ Type

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[g:A  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[f:sys-antecedent(es;X)].
    f  \mmember{}  sys-antecedent(es;g[X]) 
    supposing  \mforall{}a:E(X).  ((\mneg{}((f  a)  =  a))  {}\mRightarrow{}  (\#(g  X(a))  =  1)  {}\mRightarrow{}  (\#(g  X(f  a))  =  1))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -2  THEN  Unfold  `sys-antecedent`  0  THEN  MemTypeCD)

---

Home Index