Nuprl Lemma : transitive-set-iff2

s:Set{i:l}. (transitive-set(s) ⇐⇒ ∀x:Set{i:l}. ((x ∈ s)  (x ⊆ s)))


Proof




Definitions occuring in Statement :  transitive-set: transitive-set(s) setsubset: (a ⊆ b) Set: Set{i:l} setmem: (x ∈ s) all: x:A. B[x] iff: ⇐⇒ Q implies:  Q
Definitions unfolded in proof :  exists: x:A. B[x] uimplies: supposing a guard: {T} set-predicate: set-predicate{i:l}(s;a.P[a]) rev_implies:  Q so_apply: x[s] so_lambda: λ2x.t[x] subtype_rel: A ⊆B uall: [x:A]. B[x] prop: member: t ∈ T implies:  Q and: P ∧ Q iff: ⇐⇒ Q transitive-set: transitive-set(s) all: x:A. B[x]
Lemmas referenced :  coSet-mem-Set-implies-Set iff_wf allsetmem_wf seteq_wf seteq_weakening setsubset_functionality allsetmem-iff setsubset_wf coSet_wf all_wf Set_wf set-subtype-coSet setmem_wf
Rules used in proof :  dependent_pairFormation independent_isectElimination independent_functionElimination setEquality rename setElimination dependent_functionElimination impliesFunctionality productElimination addLevel functionEquality cumulativity lambdaEquality instantiate because_Cache sqequalRule hypothesis applyEquality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction independent_pairFormation cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}s:Set\{i:l\}.  (transitive-set(s)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:Set\{i:l\}.  ((x  \mmember{}  s)  {}\mRightarrow{}  (x  \msubseteq{}  s)))



Date html generated: 2018_07_29-AM-10_02_46
Last ObjectModification: 2018_07_18-PM-10_06_18

Theory : constructive!set!theory


Home Index