Nuprl Lemma : indep-function_functionality_wrt_equipollent
∀[A,B,C,D:Type]. (A ~ B ⇒ C ~ D ⇒ C ⟶ A ~ D ⟶ B)
Proof
Definitions occuring in Statement :
equipollent: A ~ B,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
guard: {T}
Lemmas referenced :
equipollent_transitivity,
function_functionality_wrt_equipollent_right,
function_functionality_wrt_equipollent_left,
equipollent_wf
Rules used in proof :
universeEquality,
because_Cache,
hypothesis,
independent_functionElimination,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
lemma_by_obid,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
functionEquality
Latex:
\mforall{}[A,B,C,D:Type]. (A \msim{} B {}\mRightarrow{} C \msim{} D {}\mRightarrow{} C {}\mrightarrow{} A \msim{} D {}\mrightarrow{} B)
Date html generated:
2016_10_21-AM-10_57_51
Last ObjectModification:
2016_08_06-PM-02_55_16
Theory : equipollence!!cardinality!
Home
Index