Nuprl Lemma : fset-antichain-add
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(fset(T))]. ∀[x:fset(T)].
uiff(↑fset-antichain(eq;fset-add(deq-fset(eq);x;s));(↑fset-antichain(eq;s))
∧ (∀xs:fset(T). (¬xs ⊆≠ x) ∧ (¬x ⊆≠ xs) supposing xs ∈ s))
Proof
Definitions occuring in Statement :
fset-antichain: fset-antichain(eq;ac),
f-proper-subset: xs ⊆≠ ys,
deq-fset: deq-fset(eq),
fset-add: fset-add(eq;x;s),
fset-member: a ∈ s,
fset: fset(T),
deq: EqDecider(T),
assert: ↑b,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
universe: Type
Definitions unfolded in proof :
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
member: t ∈ T,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
false: False,
or: P ∨ Q,
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
f-proper-subset: xs ⊆≠ ys
Lemmas referenced :
f-proper-subset_wf,
fset-member_wf,
fset_wf,
deq-fset_wf,
istype-void,
assert_wf,
fset-antichain_wf,
fset-add_wf,
not_wf,
equal_wf,
istype-assert,
deq_wf,
istype-universe,
assert_witness,
iff_transitivity,
iff_weakening_uiff,
assert-fset-antichain,
member-fset-add
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
independent_pairFormation,
Error :isect_memberFormation_alt,
introduction,
cut,
Error :lambdaFormation_alt,
thin,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
hypothesisEquality,
independent_isectElimination,
Error :inrFormation_alt,
Error :equalityIstype,
Error :inhabitedIsType,
because_Cache,
independent_functionElimination,
voidElimination,
Error :universeIsType,
extract_by_obid,
isectElimination,
sqequalRule,
Error :lambdaEquality_alt,
Error :functionIsTypeImplies,
Error :isect_memberEquality_alt,
Error :isectIsTypeImplies,
Error :inlFormation_alt,
productElimination,
independent_pairEquality,
Error :functionIsType,
Error :isectIsType,
Error :unionIsType,
unionElimination,
Error :productIsType,
functionEquality,
isectEquality,
unionEquality,
instantiate,
universeEquality,
promote_hyp,
equalityTransitivity,
equalitySymmetry,
hyp_replacement,
Error :dependent_set_memberEquality_alt,
applyLambdaEquality,
setElimination,
rename
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[s:fset(fset(T))]. \mforall{}[x:fset(T)].
uiff(\muparrow{}fset-antichain(eq;fset-add(deq-fset(eq);x;s));(\muparrow{}fset-antichain(eq;s))
\mwedge{} (\mforall{}xs:fset(T). (\mneg{}xs \msubseteq{}\mneq{} x) \mwedge{} (\mneg{}x \msubseteq{}\mneq{} xs) supposing xs \mmember{} s))
Date html generated:
2019_06_20-PM-01_59_30
Last ObjectModification:
2018_12_07-AM-10_21_49
Theory : finite!sets
Home
Index