Nuprl Lemma : comb_for_set_blt_wf
λp,a,b,z. (a <b b) ∈ p:PosetSig ⟶ a:|p| ⟶ b:|p| ⟶ (↓True) ⟶ 𝔹
Proof
Definitions occuring in Statement :
set_blt: a <b b,
set_car: |p|,
poset_sig: PosetSig,
bool: 𝔹,
squash: ↓T,
true: True,
member: t ∈ T,
lambda: λx.A[x],
function: x:A ⟶ B[x]
Definitions unfolded in proof :
member: t ∈ T,
squash: ↓T,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
set_blt_wf,
squash_wf,
true_wf,
set_car_wf,
poset_sig_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
sqequalHypSubstitution,
imageElimination,
cut,
lemma_by_obid,
isectElimination,
thin,
hypothesisEquality,
equalityTransitivity,
hypothesis,
equalitySymmetry
Latex:
\mlambda{}p,a,b,z. (a <\msubb{} b) \mmember{} p:PosetSig {}\mrightarrow{} a:|p| {}\mrightarrow{} b:|p| {}\mrightarrow{} (\mdownarrow{}True) {}\mrightarrow{} \mBbbB{}
Date html generated:
2016_05_15-PM-00_04_17
Last ObjectModification:
2015_12_26-PM-11_28_40
Theory : sets_1
Home
Index