Nuprl Lemma : rec-combined-class-2-classrel
∀[B,F,X,Y,es,e,v:Top].  (v ∈ F|X, Y, Prior(self)|(e) ~ v ∈ F|X, Y, Y|(e))
Proof
Definitions occuring in Statement : 
simple-comb-3: F|X, Y, Y|
, 
rec-combined-class-2: F|X, Y, Prior(self)|
, 
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-2: F|X, Y, Prior(self)|
, 
simple-comb-3: F|X, Y, Y|
, 
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,es,e,v:Top].    (v  \mmember{}  F|X,  Y,  Prior(self)|(e)  \msim{}  v  \mmember{}  F|X,  Y,  Y|(e))
Date html generated:
2016_05_17-AM-09_27_38
Last ObjectModification:
2015_12_29-PM-04_03_05
Theory : classrel!lemmas
Home
Index