Nuprl Lemma : rec-combined-class-3-classrel
∀[B,F,X,Y,Z,es,e,v:Top].
(v ∈ rec-combined-class-3(F;X;Y;Z)(e) ~ v ∈ simple-comb-4(F;X;Y;Z;Prior(rec-combined-class-3(F;X;Y;Z)))(e))
Proof
Definitions occuring in Statement :
simple-comb-4: simple-comb-4(F;W;X;Y;Z),
rec-combined-class-3: rec-combined-class-3(F;X;Y;Z),
primed-class: Prior(X),
classrel: v ∈ X(e),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
rec-combined-class-3: rec-combined-class-3(F;X;Y;Z),
simple-comb-4: simple-comb-4(F;W;X;Y;Z),
classrel: v ∈ X(e),
simple-comb: simple-comb(F;Xs),
select: L[n],
cons: [a / b],
subtract: n - m,
rec-combined-class: f|X,(self)'|,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Latex:
\mforall{}[B,F,X,Y,Z,es,e,v:Top].
(v \mmember{} rec-combined-class-3(F;X;Y;Z)(e)
\msim{} v \mmember{} simple-comb-4(F;X;Y;Z;Prior(rec-combined-class-3(F;X;Y;Z)))(e))
Date html generated:
2016_05_17-AM-09_27_47
Last ObjectModification:
2015_12_29-PM-04_02_45
Theory : classrel!lemmas
Home
Index