### Nuprl Lemma : power-set-lift-well-founded-implies

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  ((∀x:T. (R x x))`
`  `` (∀f:ℕ ⟶ P(T). (↓∃n:ℕ. ((power-set-lift(T;R) (f (n + 1)) (f n)) `` (power-set-lift(T;R) (f n) (f (n + 1))))))`
`  `` AFx,y:T.R[x;y])`

Proof

Definitions occuring in Statement :  power-set-lift: `power-set-lift(T;R)` power-set: `P(T)` almost-full: `AFx,y:T.R[x; y]` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` almost-full: `AFx,y:T.R[x; y]` all: `∀x:A. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` uimplies: `b supposing a` sq_stable: `SqStable(P)` squash: `↓T` subtract: `n - m` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` so_apply: `x[s]` exists: `∃x:A. B[x]` power-set: `P(T)` power-set-lift: `power-set-lift(T;R)` set-member: `(x ∈ s)` cand: `A c∧ B` guard: `{T}` int_upper: `{i...}` so_apply: `x[s1;s2]`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation functionEquality lemma_by_obid hypothesis hypothesisEquality thin instantiate sqequalHypSubstitution isectElimination applyEquality lambdaEquality cumulativity universeEquality sqequalRule dependent_set_memberEquality addEquality setElimination rename natural_numberEquality dependent_functionElimination unionElimination independent_pairFormation voidElimination productElimination independent_functionElimination independent_isectElimination imageMemberEquality baseClosed imageElimination isect_memberEquality voidEquality intEquality because_Cache minusEquality dependent_pairEquality dependent_pairFormation multiplyEquality baseApply closedConclusion productEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x:T.  (R  x  x))
{}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  P(T)
(\mdownarrow{}\mexists{}n:\mBbbN{}
((power-set-lift(T;R)  (f  (n  +  1))  (f  n))  {}\mRightarrow{}  (power-set-lift(T;R)  (f  n)  (f  (n  +  1))))))
{}\mRightarrow{}  AFx,y:T.R[x;y])

Date html generated: 2016_05_13-PM-03_51_45
Last ObjectModification: 2016_01_14-PM-07_00_34

Theory : bar-induction

Home Index