Nuprl Lemma : mk-set_wf

∀[Item:Type]. ∀[set:{s:Type| valueall-type(Item) ⇒ valueall-type(s)} ]. ∀[member:Item ─→ set ─→ 𝔹].
∀[empty:{s:set| ∀x:Item. (¬↑(member x s))} ]. ∀[isEmpty:{f:set ─→ 𝔹| ∀s:set. (↑(f s) ⇐⇒ ∀x:Item. (¬↑(member x s)))} ].
∀[singleton:{f:Item ─→ set| ∀x,y:Item.  (↑(member x (f y)) ⇐⇒ x = y ∈ Item)} ]. ∀[add:{f:Item ─→ set ─→ set| 
                                                                                       ∀s:set. ∀x,y:Item.
                                                                                         (↑(member x (f y s))
                                                                                         ⇐⇒ (x = y ∈ Item)
                                                                                             ∨ (↑(member x s)))} ].
∀[union:{f:set ─→ set ─→ set| ∀s1,s2:set. ∀x:Item.  (↑(member x (f s1 s2)) ⇐⇒ (↑(member x s1)) ∨ (↑(member x s2)))} ].
∀[remove:{f:Item ─→ set ─→ set| ∀s:set. ∀x,y:Item.  (↑(member x (f y s)) ⇐⇒ (¬(x = y ∈ Item)) ∧ (↑(member x s)))} ].
  (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ∈ set-sig{i:l}(Item))


Proof



Definitions occuring in Statement :  mk-set: mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove),  set-sig: set-sig{i:l}(Item),  valueall-type: valueall-type(T),  assert: ↑b,  bool: 𝔹,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  not: ¬A,  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ─→ B[x],  universe: Type,  equal: s = t ∈ T
Lemmas :  eq_atom_wf,  uiff_transitivity,  equal-wf-base,  atom_subtype_base,  assert_wf,  eqtt_to_assert,  assert_of_eq_atom,  subtype_base_sq,  rec_select_update_lemma,  iff_transitivity,  bnot_wf,  not_wf,  iff_weakening_uiff,  eqff_to_assert,  assert_of_bnot,  bool_wf,  set_wf,  all_wf,  iff_wf,  equal_wf,  or_wf,  valueall-type_wf
\mforall{}[Item:Type].  \mforall{}[set:\{s:Type|  valueall-type(Item)  {}\mRightarrow{}  valueall-type(s)\}  ].  \mforall{}[member:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[empty:\{s:set|  \mforall{}x:Item.  (\mneg{}\muparrow{}(member  x  s))\}  ].  \mforall{}[isEmpty:\{f:set  {}\mrightarrow{}  \mBbbB{}| 
                                                                                                                \mforall{}s:set
                                                                                                                    (\muparrow{}(f  s)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:Item.  (\mneg{}\muparrow{}(member  x  s)))\}  ].
\mforall{}[singleton:\{f:Item  {}\mrightarrow{}  set|  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y))  \mLeftarrow{}{}\mRightarrow{}  x  =  y)\}  ].
\mforall{}[add:\{f:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
              \mforall{}s:set.  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y  s))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (\muparrow{}(member  x  s)))\}  ].
\mforall{}[union:\{f:set  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
                  \mforall{}s1,s2:set.  \mforall{}x:Item.    (\muparrow{}(member  x  (f  s1  s2))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(member  x  s1))  \mvee{}  (\muparrow{}(member  x  s2)))\}  ].
\mforall{}[remove:\{f:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
                    \mforall{}s:set.  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y  s))  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}(member  x  s)))\}  ].
    (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove)  \mmember{}  set-sig\{i:l\}(Item))


Date html generated: 2015_07_17-AM-08_21_04
Last ObjectModification: 2015_04_02-PM-05_42_46

Home Index