---

Step * 1 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
⊢ <oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)> ∈ MCopower(s;g↓hgrp)
BY
{ MemTypeCD }

1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ <oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)> ∈ mcopower_sig{i:l}(s;g↓hgrp)

2
.....set predicate..... 
1. s : LOSet@i'
2. g : OGrp@i'
⊢ (∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j))
∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g↓hgrp,h).
     (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.umap h f) = !v:|<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mo\000Cn| ⟶ |h|
                                                            (IsMonHom{<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mo\000Cn,h}(v)
                                                            ∧ (∀j:|s|
                                                                 ((f j)
                                                                 = (v o (<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>\000C.inj j))
                                                                 ∈ (|(g↓hgrp)| ⟶ |h|)))))

3
.....wf..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. c : mcopower_sig{i:l}(s;g↓hgrp)
⊢ (∀j:|s|. IsMonHom{g↓hgrp,c.mon}(c.inj j))
  ∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g↓hgrp,h).
       (c.umap h f) = !v:|c.mon| ⟶ |h|
                        (IsMonHom{c.mon,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|(g↓hgrp)| ⟶ |h|))))) ∈ 𝕌'

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
\mvdash{}  <oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>  \mmember{}  MCopower(s;g\mdownarrow{}hgrp)


By

---

Latex:
MemTypeCD

---

Home Index