---

Step * of Lemma sub-powerset-lattice_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)]. ∀[P:fset(T) ⟶ ℙ].
  sub-powerset-lattice(T;eq;whole;P) ∈ BoundedDistributiveLattice 
  supposing (∀x:T. x ∈ whole) ∧ (∀a,b:fset(T).  ((P a) ⇒ (P b) ⇒ ((P a ⋃ b) ∧ (P a ⋂ b)))) ∧ (P {}) ∧ (P whole)
BY
{ (ProveWfLemma
   THEN RepUR ``so_apply`` 0
   THEN Auto
   THEN (DSetVars THEN EqTypeCD)
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. whole : fset(T)
4. P : fset(T) ⟶ ℙ
5. ∀x:T. x ∈ whole
6. ∀a,b:fset(T).  ((P a) ⇒ (P b) ⇒ ((P a ⋃ b) ∧ (P a ⋂ b)))
7. P {}
8. P whole
9. ∀[a,b:{s:fset(T)| P s} ].  (λa,b. a ⋂ b[a;b] = λa,b. a ⋂ b[b;a] ∈ {s:fset(T)| P s} )
10. ∀[a,b:{s:fset(T)| P s} ].  (λa,b. a ⋃ b[a;b] = λa,b. a ⋃ b[b;a] ∈ {s:fset(T)| P s} )
11. ∀[a,b,c:{s:fset(T)| P s} ].  (λa,b. a ⋂ b[a;λa,b. a ⋂ b[b;c]] = λa,b. a ⋂ b[λa,b. a ⋂ b[a;b];c] ∈ {s:fset(T)| P s} )
12. ∀[a,b,c:{s:fset(T)| P s} ].  (λa,b. a ⋃ b[a;λa,b. a ⋃ b[b;c]] = λa,b. a ⋃ b[λa,b. a ⋃ b[a;b];c] ∈ {s:fset(T)| P s} )
13. ∀[a,b:{s:fset(T)| P s} ].  (λa,b. a ⋃ b[a;λa,b. a ⋂ b[a;b]] = a ∈ {s:fset(T)| P s} )
14. ∀[a,b:{s:fset(T)| P s} ].  (λa,b. a ⋂ b[a;λa,b. a ⋃ b[a;b]] = a ∈ {s:fset(T)| P s} )
15. a : fset(T)
16. P a
⊢ a ⋂ whole = a ∈ fset(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[whole:fset(T)].  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbP{}].
    sub-powerset-lattice(T;eq;whole;P)  \mmember{}  BoundedDistributiveLattice 
    supposing  (\mforall{}x:T.  x  \mmember{}  whole)
    \mwedge{}  (\mforall{}a,b:fset(T).    ((P  a)  {}\mRightarrow{}  (P  b)  {}\mRightarrow{}  ((P  a  \mcup{}  b)  \mwedge{}  (P  a  \mcap{}  b))))
    \mwedge{}  (P  \{\})
    \mwedge{}  (P  whole)


By

---

Latex:
(ProveWfLemma
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto
  THEN  (DSetVars  THEN  EqTypeCD)
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Auto)))

---

Home Index