Nuprl Lemma : sp-meet-top

[x:Sierpinski]. (x ∧ ⊤ x ∈ Sierpinski)


Proof




Definitions occuring in Statement :  sp-meet: f ∧ g Sierpinski: Sierpinski Sierpinski-top: uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a iff: ⇐⇒ Q implies:  Q prop: rev_implies:  Q cand: c∧ B
Lemmas referenced :  Sierpinski-equal2 sp-meet_wf Sierpinski-top_wf subtype-Sierpinski sp-meet-is-top equal_wf Sierpinski_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality sqequalRule productElimination independent_isectElimination independent_pairFormation lambdaFormation because_Cache equalityTransitivity equalitySymmetry independent_functionElimination

Latex:
\mforall{}[x:Sierpinski].  (x  \mwedge{}  \mtop{}  =  x)



Date html generated: 2019_10_31-AM-06_36_39
Last ObjectModification: 2015_12_28-AM-11_20_44

Theory : synthetic!topology


Home Index