### Nuprl Lemma : isname_wf

[L:Cname List]. ∀[z:extd-nameset(L)].  (isname(z) ∈ 𝔹)

Proof

Definitions occuring in Statement :  isname: isname(z) extd-nameset: extd-nameset(L) coordinate_name: Cname list: List bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T isname: isname(z) extd-nameset: extd-nameset(L) b-union: A ⋃ B tunion: x:A.B[x] bool: 𝔹 unit: Unit ifthenelse: if then else fi  pi2: snd(t) nameset: nameset(L) coordinate_name: Cname int_upper: {i...} int_seg: {i..j-}
Lemmas referenced :  le_int_wf extd-nameset_wf list_wf coordinate_name_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution imageElimination productElimination thin unionElimination equalityElimination sqequalRule lemma_by_obid isectElimination natural_numberEquality setElimination rename hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[L:Cname  List].  \mforall{}[z:extd-nameset(L)].    (isname(z)  \mmember{}  \mBbbB{})

Date html generated: 2016_05_20-AM-09_29_12
Last ObjectModification: 2015_12_28-PM-04_47_44

Theory : cubical!sets

Home Index