---

Step * 1 of Lemma sub-powerset-lattice_wf


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)
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.  P  :  fset(T)  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:T.  x  \mmember{}  whole
6.  \mforall{}a,b:fset(T).    ((P  a)  {}\mRightarrow{}  (P  b)  {}\mRightarrow{}  ((P  a  \mcup{}  b)  \mwedge{}  (P  a  \mcap{}  b)))
7.  P  \{\}
8.  P  whole
9.  \mforall{}[a,b:\{s:fset(T)|  P  s\}  ].    (\mlambda{}a,b.  a  \mcap{}  b[a;b]  =  \mlambda{}a,b.  a  \mcap{}  b[b;a])
10.  \mforall{}[a,b:\{s:fset(T)|  P  s\}  ].    (\mlambda{}a,b.  a  \mcup{}  b[a;b]  =  \mlambda{}a,b.  a  \mcup{}  b[b;a])
11.  \mforall{}[a,b,c:\{s:fset(T)|  P  s\}  ].    (\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])
12.  \mforall{}[a,b,c:\{s:fset(T)|  P  s\}  ].    (\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])
13.  \mforall{}[a,b:\{s:fset(T)|  P  s\}  ].    (\mlambda{}a,b.  a  \mcup{}  b[a;\mlambda{}a,b.  a  \mcap{}  b[a;b]]  =  a)
14.  \mforall{}[a,b:\{s:fset(T)|  P  s\}  ].    (\mlambda{}a,b.  a  \mcap{}  b[a;\mlambda{}a,b.  a  \mcup{}  b[a;b]]  =  a)
15.  a  :  fset(T)
16.  P  a
\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