### Nuprl Lemma : product_functionality_wrt_equipollent_dependent

`∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].`
`  ∀f:A ⟶ B. (Bij(A;B;f) `` (∀a:A. C[a] ~ D[f a]) `` a:A × C[a] ~ b:B × D[b])`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` biject: `Bij(A;B;f)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` equipollent: `A ~ B` exists: `∃x:A. B[x]` member: `t ∈ T` so_apply: `x[s]` prop: `ℙ` pi1: `fst(t)` biject: `Bij(A;B;f)` and: `P ∧ Q` inject: `Inj(A;B;f)` surject: `Surj(A;B;f)` pi2: `snd(t)` guard: `{T}` subtype_rel: `A ⊆r B` uimplies: `b supposing a` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  equipollent_wf biject_wf istype-universe equal_wf subtype_rel-equal squash_wf true_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  sqequalHypSubstitution sqequalRule cut hypothesis promote_hyp thin productElimination Error :functionIsType,  Error :universeIsType,  hypothesisEquality introduction extract_by_obid isectElimination applyEquality Error :inhabitedIsType,  instantiate universeEquality because_Cache functionExtensionality rename Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :equalityIsType1,  equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination Error :dependent_pairEquality_alt,  Error :productIsType,  independent_pairFormation productEquality applyLambdaEquality independent_isectElimination Error :dependent_set_memberEquality_alt,  setElimination imageElimination natural_numberEquality imageMemberEquality baseClosed equalityElimination Error :equalityIstype

Latex:
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  Type].  \mforall{}[D:B  {}\mrightarrow{}  Type].
\mforall{}f:A  {}\mrightarrow{}  B.  (Bij(A;B;f)  {}\mRightarrow{}  (\mforall{}a:A.  C[a]  \msim{}  D[f  a])  {}\mRightarrow{}  a:A  \mtimes{}  C[a]  \msim{}  b:B  \mtimes{}  D[b])

Date html generated: 2019_06_20-PM-02_16_49
Last ObjectModification: 2018_11_23-PM-02_55_47

Theory : equipollence!!cardinality!

Home Index