Step
*
1
1
2
1
1
1
2
of Lemma
cut-of-singleton
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e})
8. ∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c'
9. {e} ⊆ cut(X;f;{e})
10. ∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c'
11. ↑e ∈b prior(X)
12. ¬((f e) = e ∈ E)
13. {prior(X)(e)} ⊆ cut(X;f;{prior(X)(e)})
14. ∀[c':Cut(X;f)]. cut(X;f;{prior(X)(e)}) ⊆ c' supposing {prior(X)(e)} ⊆ c'
15. ¬((f e) = e ∈ E(X))@i
⊢ f e ∈ cut(X;f;{f e}) ∪ cut(X;f;{prior(X)(e)})
BY
{ ((BLemma `member-fset-union` THENM OrLeft THENM BackThruHyp' 7) THEN Auto)⋅ }
Latex:
Latex:
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
6. \mforall{}[s:fset(E(X))]. (s \msubseteq{} cut(X;f;s) \mwedge{} (\mforall{}[c':Cut(X;f)]. cut(X;f;s) \msubseteq{} c' supposing s \msubseteq{} c'))
7. \{f e\} \msubseteq{} cut(X;f;\{f e\})
8. \mforall{}[c':Cut(X;f)]. cut(X;f;\{f e\}) \msubseteq{} c' supposing \{f e\} \msubseteq{} c'
9. \{e\} \msubseteq{} cut(X;f;\{e\})
10. \mforall{}[c':Cut(X;f)]. cut(X;f;\{e\}) \msubseteq{} c' supposing \{e\} \msubseteq{} c'
11. \muparrow{}e \mmember{}\msubb{} prior(X)
12. \mneg{}((f e) = e)
13. \{prior(X)(e)\} \msubseteq{} cut(X;f;\{prior(X)(e)\})
14. \mforall{}[c':Cut(X;f)]. cut(X;f;\{prior(X)(e)\}) \msubseteq{} c' supposing \{prior(X)(e)\} \msubseteq{} c'
15. \mneg{}((f e) = e)@i
\mvdash{} f e \mmember{} cut(X;f;\{f e\}) \mcup{} cut(X;f;\{prior(X)(e)\})
By
Latex:
((BLemma `member-fset-union` THENM OrLeft THENM BackThruHyp' 7) THEN Auto)\mcdot{}
Home
Index