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