Step
*
1
1
1
2
1
1
1
1
1
1
3
1
1
1
1
1
1
2
1
2
1
1
1
1
1
1
of Lemma
free-dl-basis
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T))
4. [%58] : ↑fset-antichain(eq;x)
5. ∀s:fset(T). ({s} ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
6. x ∈ fset(fset(T))
7. deq-fset(deq-fset(eq)) ∈ EqDecider({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
8. ∀[x@0:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]. x@0 ≤ \/(λs.{s}"(x)) supposing x@0 ∈ λs.{s}"(x)
9. ∀[u:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]
((∀x@0:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} . (x@0 ∈ λs.{s}"(x) ⇒ x@0 ≤ u)) ⇒ \/(λs.{s}"(x)) ≤ u)
10. \/(λs.{s}"(x)) ≤ x
11. \/(λs.{s}"(x)) ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
12. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
13. b : fset(T)
14. b ∈ \/(λs.{s}"(x))
15. ∀x:fset(fset(T)). (\/(λs.{s}"(x)) ∈ fset(fset(T)))
16. ∀p:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} . ∀b:fset(T). (b ∈ p ∈ ℙ)
17. X : fset({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
18. x1 : fset(fset(T))
19. [%56] : ↑fset-antichain(eq;x1)
20. ∀a:fset(T). (a ∈ \/(X) ⇒ (↓∃p:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} . (p ∈ X ∧ a ∈ p)))
21. ¬x1 ∈ X
22. a : fset(T)
23. v : fset(fset(T))
24. [%54] : ↑fset-antichain(eq;v)
25. \/({x1}) = v ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
26. v1 : fset(fset(T))
27. [%52] : ↑fset-antichain(eq;v1)
28. \/(X) = v1 ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
29. a ∈ v ∨ v1
⊢ a ∈ v ∨ a ∈ v1
BY
{ (RWO "free-dl-join" (-1) THENA Auto) }
1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T))
4. [%58] : ↑fset-antichain(eq;x)
5. ∀s:fset(T). ({s} ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
6. x ∈ fset(fset(T))
7. deq-fset(deq-fset(eq)) ∈ EqDecider({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
8. ∀[x@0:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]. x@0 ≤ \/(λs.{s}"(x)) supposing x@0 ∈ λs.{s}"(x)
9. ∀[u:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]
((∀x@0:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} . (x@0 ∈ λs.{s}"(x) ⇒ x@0 ≤ u)) ⇒ \/(λs.{s}"(x)) ≤ u)
10. \/(λs.{s}"(x)) ≤ x
11. \/(λs.{s}"(x)) ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
12. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
13. b : fset(T)
14. b ∈ \/(λs.{s}"(x))
15. ∀x:fset(fset(T)). (\/(λs.{s}"(x)) ∈ fset(fset(T)))
16. ∀p:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} . ∀b:fset(T). (b ∈ p ∈ ℙ)
17. X : fset({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
18. x1 : fset(fset(T))
19. [%56] : ↑fset-antichain(eq;x1)
20. ∀a:fset(T). (a ∈ \/(X) ⇒ (↓∃p:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} . (p ∈ X ∧ a ∈ p)))
21. ¬x1 ∈ X
22. a : fset(T)
23. v : fset(fset(T))
24. [%54] : ↑fset-antichain(eq;v)
25. \/({x1}) = v ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
26. v1 : fset(fset(T))
27. [%52] : ↑fset-antichain(eq;v1)
28. \/(X) = v1 ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)}
29. a ∈ fset-ac-lub(eq;v;v1)
⊢ a ∈ v ∨ a ∈ v1
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T))
4. [\%58] : \muparrow{}fset-antichain(eq;x)
5. \mforall{}s:fset(T). (\{s\} \mmember{} \{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} )
6. x \mmember{} fset(fset(T))
7. deq-fset(deq-fset(eq)) \mmember{} EqDecider(\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} )
8. \mforall{}[x@0:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ]
x@0 \mleq{} \mbackslash{}/(\mlambda{}s.\{s\}"(x)) supposing x@0 \mmember{} \mlambda{}s.\{s\}"(x)
9. \mforall{}[u:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ]
((\mforall{}x@0:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} . (x@0 \mmember{} \mlambda{}s.\{s\}"(x) {}\mRightarrow{} x@0 \mleq{} u))
{}\mRightarrow{} \mbackslash{}/(\mlambda{}s.\{s\}"(x)) \mleq{} u)
10. \mbackslash{}/(\mlambda{}s.\{s\}"(x)) \mleq{} x
11. \mbackslash{}/(\mlambda{}s.\{s\}"(x)) \mmember{} \{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\}
12. \mforall{}[P:fset(T) {}\mrightarrow{} \mBbbB{}]. \mforall{}[s:fset(fset(T))].
uiff(\{x \mmember{} s | P[x]\} = \{\};\mneg{}(\mexists{}x:fset(T). (x \mmember{} s \mwedge{} (\muparrow{}P[x]))))
13. b : fset(T)
14. b \mmember{} \mbackslash{}/(\mlambda{}s.\{s\}"(x))
15. \mforall{}x:fset(fset(T)). (\mbackslash{}/(\mlambda{}s.\{s\}"(x)) \mmember{} fset(fset(T)))
16. \mforall{}p:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} . \mforall{}b:fset(T). (b \mmember{} p \mmember{} \mBbbP{})
17. X : fset(\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} )
18. x1 : fset(fset(T))
19. [\%56] : \muparrow{}fset-antichain(eq;x1)
20. \mforall{}a:fset(T). (a \mmember{} \mbackslash{}/(X) {}\mRightarrow{} (\mdownarrow{}\mexists{}p:\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} . (p \mmember{} X \mwedge{} a \mmember{} p)))
21. \mneg{}x1 \mmember{} X
22. a : fset(T)
23. v : fset(fset(T))
24. [\%54] : \muparrow{}fset-antichain(eq;v)
25. \mbackslash{}/(\{x1\}) = v
26. v1 : fset(fset(T))
27. [\%52] : \muparrow{}fset-antichain(eq;v1)
28. \mbackslash{}/(X) = v1
29. a \mmember{} v \mvee{} v1
\mvdash{} a \mmember{} v \mvee{} a \mmember{} v1
By
Latex:
(RWO "free-dl-join" (-1) THENA Auto)
Home
Index