Nuprl Lemma : cantor-theorem-on-power-set

[T:Type]. powerset(T))


This theorem is one of freek's list of 100 theorems



Proof




Definitions occuring in Statement :  powerset: powerset(T) equipollent: B uall: [x:A]. B[x] not: ¬A universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T not: ¬A implies:  Q false: False equipollent: B exists: x:A. B[x] biject: Bij(A;B;f) and: P ∧ Q surject: Surj(A;B;f) all: x:A. B[x] squash: T prop: bnot: ¬bb ifthenelse: if then else fi  true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) bfalse: ff or: P ∨ Q sq_type: SQType(T) assert: b powerset: powerset(T)
Lemmas referenced :  equipollent_wf powerset_wf bool_wf bnot_wf equal_wf squash_wf true_wf iff_weakening_equal eqtt_to_assert btrue_neq_bfalse equal-wf-base eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot int_seg_wf equipollent_functionality_wrt_equipollent2 function_functionality_wrt_equipollent_right equipollent-two
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination because_Cache universeEquality functionEquality productElimination applyEquality functionExtensionality imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed independent_isectElimination unionElimination equalityElimination dependent_pairFormation promote_hyp instantiate

Latex:
\mforall{}[T:Type].  (\mneg{}T  \msim{}  powerset(T))



Date html generated: 2018_05_21-PM-08_36_26
Last ObjectModification: 2017_07_26-PM-06_00_58

Theory : general


Home Index