Nuprl Lemma : antecedent-function_functionality_wrt_iff
∀es:EO
  ∀[P,Q,P',Q':E ⟶ ℙ].
    ∀f:{e:E| P e}  ⟶ {e:E| Q e} . ((∀e:E. (P e 
⇐⇒ P' e)) 
⇒ (∀e:E. (Q e 
⇐⇒ Q' e)) 
⇒ (Q ⟵─f── P 
⇐⇒ Q' ⟵─f── P'))
Proof
Definitions occuring in Statement : 
antecedent-function: Q ⟵─f── P
, 
es-E: E
, 
event_ordering: EO
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
function: x:A ⟶ B[x]
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ Q
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
member: t ∈ T
, 
prop: ℙ
, 
rev_implies: P 
⇐ Q
, 
subtype_rel: A ⊆r B
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
uimplies: b supposing a
, 
antecedent-function: Q ⟵─f── P
, 
cand: A c∧ B
, 
guard: {T}
Latex:
\mforall{}es:EO
    \mforall{}[P,Q,P',Q':E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\} 
            ((\mforall{}e:E.  (P  e  \mLeftarrow{}{}\mRightarrow{}  P'  e))  {}\mRightarrow{}  (\mforall{}e:E.  (Q  e  \mLeftarrow{}{}\mRightarrow{}  Q'  e))  {}\mRightarrow{}  (Q  \mleftarrow{}{}{}f{}{}  P  \mLeftarrow{}{}\mRightarrow{}  Q'  \mleftarrow{}{}{}f{}{}  P'))
Date html generated:
2016_05_16-AM-10_27_44
Last ObjectModification:
2015_12_28-PM-09_19_06
Theory : new!event-ordering
Home
Index