Nuprl Lemma : pair-lex_wf
∀[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ]. (pair-lex(A;Ra;Rb) ∈ (A × B) ⟶ (A × B) ⟶ ℙ)
Proof
Definitions occuring in Statement :
pair-lex: pair-lex(A;Ra;Rb),
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
pair-lex: pair-lex(A;Ra;Rb),
pi1: fst(t),
prop: ℙ,
and: P ∧ Q,
pi2: snd(t),
subtype_rel: A ⊆r B
Lemmas referenced :
or_wf,
equal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
lambdaEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
applyEquality,
functionExtensionality,
hypothesisEquality,
cumulativity,
productElimination,
productEquality,
because_Cache,
hypothesis,
universeEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
functionEquality,
isect_memberEquality
Latex:
\mforall{}[A,B:Type]. \mforall{}[Ra:A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}]. \mforall{}[Rb:B {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}]. (pair-lex(A;Ra;Rb) \mmember{} (A \mtimes{} B) {}\mrightarrow{} (A \mtimes{} B) {}\mrightarrow{} \mBbbP{})
Date html generated:
2017_04_14-AM-07_13_57
Last ObjectModification:
2017_02_27-PM-02_49_45
Theory : well_fnd
Home
Index