Nuprl Lemma : assert_of_band2

p:𝔹. ∀q:⋂:↑p. 𝔹.  uiff(↑(p ∧b q);(↑p) ∧ (↑q))


Proof




Definitions occuring in Statement :  band: p ∧b q assert: b bool: 𝔹 uiff: uiff(P;Q) all: x:A. B[x] and: P ∧ Q isect: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit member: t ∈ T it: btrue: tt uall: [x:A]. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a assert: b ifthenelse: if then else fi  band: p ∧b q bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb false: False prop: subtype_rel: A ⊆B true: True
Lemmas referenced :  eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot true_wf it_wf subtype_rel_self assert_witness assert_wf istype-void
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut inhabitedIsType hypothesis thin sqequalHypSubstitution unionElimination equalityElimination introduction extract_by_obid isectElimination hypothesisEquality productElimination independent_isectElimination sqequalRule dependent_pairFormation_alt equalityIsType1 promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination because_Cache voidElimination universeIsType isectIsType applyEquality independent_pairFormation isect_memberFormation_alt natural_numberEquality independent_pairEquality axiomEquality productIsType

Latex:
\mforall{}p:\mBbbB{}.  \mforall{}q:\mcap{}:\muparrow{}p.  \mBbbB{}.    uiff(\muparrow{}(p  \mwedge{}\msubb{}  q);(\muparrow{}p)  \mwedge{}  (\muparrow{}q))



Date html generated: 2019_10_15-AM-11_06_04
Last ObjectModification: 2018_10_09-PM-03_14_29

Theory : general


Home Index