---

Step * 1 of Lemma finite-powerset-lattice_wf


1. T : Type
2. eq : EqDecider(T)
3. whole : fset(T)
4. ∀x:T. x ∈ whole
5. ∀[a,b:fset(T)].  (λa,b. a ⋂ b[a;b] = λa,b. a ⋂ b[b;a] ∈ fset(T))
6. ∀[a,b:fset(T)].  (λa,b. a ⋃ b[a;b] = λa,b. a ⋃ b[b;a] ∈ fset(T))
7. ∀[a,b,c:fset(T)].  (λa,b. a ⋂ b[a;λa,b. a ⋂ b[b;c]] = λa,b. a ⋂ b[λa,b. a ⋂ b[a;b];c] ∈ fset(T))
8. ∀[a,b,c:fset(T)].  (λa,b. a ⋃ b[a;λa,b. a ⋃ b[b;c]] = λa,b. a ⋃ b[λa,b. a ⋃ b[a;b];c] ∈ fset(T))
9. ∀[a,b:fset(T)].  (λa,b. a ⋃ b[a;λa,b. a ⋂ b[a;b]] = a ∈ fset(T))
10. ∀[a,b:fset(T)].  (λa,b. a ⋂ b[a;λa,b. a ⋃ b[a;b]] = a ∈ fset(T))
11. a : fset(T)
⊢ a ⋂ whole = a ∈ fset(T)
BY
{ ((UsingVars [`eq'] (BLemma `fset-extensionality`) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RWO "member-fset-intersection" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  whole  :  fset(T)
4.  \mforall{}x:T.  x  \mmember{}  whole
5.  \mforall{}[a,b:fset(T)].    (\mlambda{}a,b.  a  \mcap{}  b[a;b]  =  \mlambda{}a,b.  a  \mcap{}  b[b;a])
6.  \mforall{}[a,b:fset(T)].    (\mlambda{}a,b.  a  \mcup{}  b[a;b]  =  \mlambda{}a,b.  a  \mcup{}  b[b;a])
7.  \mforall{}[a,b,c:fset(T)].    (\mlambda{}a,b.  a  \mcap{}  b[a;\mlambda{}a,b.  a  \mcap{}  b[b;c]]  =  \mlambda{}a,b.  a  \mcap{}  b[\mlambda{}a,b.  a  \mcap{}  b[a;b];c])
8.  \mforall{}[a,b,c:fset(T)].    (\mlambda{}a,b.  a  \mcup{}  b[a;\mlambda{}a,b.  a  \mcup{}  b[b;c]]  =  \mlambda{}a,b.  a  \mcup{}  b[\mlambda{}a,b.  a  \mcup{}  b[a;b];c])
9.  \mforall{}[a,b:fset(T)].    (\mlambda{}a,b.  a  \mcup{}  b[a;\mlambda{}a,b.  a  \mcap{}  b[a;b]]  =  a)
10.  \mforall{}[a,b:fset(T)].    (\mlambda{}a,b.  a  \mcap{}  b[a;\mlambda{}a,b.  a  \mcup{}  b[a;b]]  =  a)
11.  a  :  fset(T)
\mvdash{}  a  \mcap{}  whole  =  a


By

---

Latex:
((UsingVars  [`eq']  (BLemma  `fset-extensionality`)  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RWO  "member-fset-intersection"  0
  THEN  Auto)

---

Home Index