Nuprl Lemma : set-axiom-of-choice-is-false
¬Set-AC
Proof
Definitions occuring in Statement :
set-axiom-of-choice: Set-AC,
not: ¬A
Definitions unfolded in proof :
not: ¬A,
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
false: False
Lemmas referenced :
set-axiom-of-choice-implies-xmiddle,
set-axiom-of-choice_wf,
no-excluded-middle-using-partial2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
independent_functionElimination,
thin,
hypothesis,
voidElimination
Latex:
\mneg{}Set-AC
Date html generated:
2016_12_12-AM-09_14_55
Last ObjectModification:
2016_11_23-PM-05_31_06
Theory : partial_1
Home
Index