Nuprl Lemma : bl-exists-map

[f,L,P:Top].  ((∃x∈map(f;L).P[x])_b (∃x∈L.P[f x])_b)


Proof




Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b map: map(f;as) uall: [x:A]. B[x] top: Top so_apply: x[s] apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bl-exists: (∃x∈L.P[x])_b so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2]
Lemmas referenced :  reduce-map top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality hypothesis sqequalAxiom because_Cache

Latex:
\mforall{}[f,L,P:Top].    ((\mexists{}x\mmember{}map(f;L).P[x])\_b  \msim{}  (\mexists{}x\mmember{}L.P[f  x])\_b)



Date html generated: 2016_05_14-PM-02_11_59
Last ObjectModification: 2015_12_26-PM-05_02_53

Theory : list_1


Home Index