---

Step * 1 of Lemma fset-union-closed


1. T : Type
2. eq : EqDecider(T)
3. fs : (T ⟶ T) List
4. as : fset(T)
5. bs : fset(T)
6. ∀f:T ⟶ T. ((f ∈ fs) ⇒ (∀x:T. f x ∈ as supposing x ∈ as))
7. ∀f:T ⟶ T. ((f ∈ fs) ⇒ (∀x:T. f x ∈ bs supposing x ∈ bs))
8. f : T ⟶ T@i
9. (f ∈ fs)@i
10. x : T@i
11. x ∈ as ⋃ bs
⊢ f x ∈ as ⋃ bs
BY
{ (((RWO "member-fset-union" (-1) THENM RWO "member-fset-union" 0) THENA Auto) THEN ParallelLast THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  fs  :  (T  {}\mrightarrow{}  T)  List
4.  as  :  fset(T)
5.  bs  :  fset(T)
6.  \mforall{}f:T  {}\mrightarrow{}  T.  ((f  \mmember{}  fs)  {}\mRightarrow{}  (\mforall{}x:T.  f  x  \mmember{}  as  supposing  x  \mmember{}  as))
7.  \mforall{}f:T  {}\mrightarrow{}  T.  ((f  \mmember{}  fs)  {}\mRightarrow{}  (\mforall{}x:T.  f  x  \mmember{}  bs  supposing  x  \mmember{}  bs))
8.  f  :  T  {}\mrightarrow{}  T@i
9.  (f  \mmember{}  fs)@i
10.  x  :  T@i
11.  x  \mmember{}  as  \mcup{}  bs
\mvdash{}  f  x  \mmember{}  as  \mcup{}  bs


By

---

Latex:
(((RWO  "member-fset-union"  (-1)  THENM  RWO  "member-fset-union"  0)  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto)\mcdot{}

---

Home Index