Nuprl Lemma : union_functionality_wrt_uiff3

[P1,P2,Q1,Q2:ℙ].  ((P1 P2 ∈ ℙ {uiff(Q1;Q2)}  {P1 Q1 ⇐⇒ P2 Q2})


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) uall: [x:A]. B[x] prop: guard: {T} iff: ⇐⇒ Q implies:  Q union: left right equal: t ∈ T
Definitions unfolded in proof :  guard: {T} or: P ∨ Q uall: [x:A]. B[x] implies:  Q uiff: uiff(P;Q) and: P ∧ Q iff: ⇐⇒ Q prop: member: t ∈ T uimplies: supposing a rev_implies:  Q
Lemmas referenced :  or_wf uiff_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation sqequalHypSubstitution productElimination thin independent_pairFormation unionElimination inlFormation cut hypothesis hyp_replacement equalitySymmetry hypothesisEquality inrFormation independent_isectElimination introduction extract_by_obid isectElimination instantiate universeEquality Error :inhabitedIsType,  Error :universeIsType

Latex:
\mforall{}[P1,P2,Q1,Q2:\mBbbP{}].    ((P1  =  P2)  {}\mRightarrow{}  \{uiff(Q1;Q2)\}  {}\mRightarrow{}  \{P1  +  Q1  \mLeftarrow{}{}\mRightarrow{}  P2  +  Q2\})



Date html generated: 2019_06_20-AM-11_17_27
Last ObjectModification: 2018_09_26-AM-10_24_53

Theory : core_2


Home Index