Nuprl Lemma : stable-union-decomp
∀[X,T:Type]. ∀[P:T ⟶ X ⟶ ℙ]. ∀[S:T ⟶ Type]. ∀[Q:i:T ⟶ S[i] ⟶ X ⟶ ℙ].
stable-union(X;T;i,x.P[i;x]) ≡ stable-union(X;i:T × S[i];p,x.Q[fst(p);snd(p);x])
supposing (∀x:X. ∀i:T. ∀s:S[i]. (Q[i;s;x] ⇒ (¬¬P[i;x]))) ∧ (∀x:X. ∀i:T. (P[i;x] ⇒ (¬¬(∃s:S[i]. Q[i;s;x]))))
Proof
Definitions occuring in Statement :
stable-union: stable-union(X;T;i,x.P[i; x]),
ext-eq: A ≡ B,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
ext-eq: A ≡ B,
subtype_rel: A ⊆r B,
stable-union: stable-union(X;T;i,x.P[i; x]),
prop: ℙ,
exists: ∃x:A. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
so_apply: x[s1;s2;s3],
so_lambda: λ2x.t[x],
implies: P ⇒ Q,
not: ¬A,
false: False,
so_lambda: λ2x y.t[x; y],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x]
Lemmas referenced :
double-negation-hyp-elim,
not_wf,
pi1_wf,
pi2_wf,
istype-void,
stable-union_wf,
subtype_rel_self,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairFormation,
lambdaEquality_alt,
setElimination,
rename,
dependent_set_memberEquality_alt,
hypothesisEquality,
extract_by_obid,
isectElimination,
sqequalRule,
productEquality,
applyEquality,
universeIsType,
hypothesis,
independent_functionElimination,
lambdaFormation_alt,
productIsType,
because_Cache,
functionIsType,
dependent_functionElimination,
dependent_pairFormation_alt,
voidElimination,
independent_pairEquality,
axiomEquality,
instantiate,
universeEquality,
isect_memberEquality_alt,
isectIsTypeImplies,
inhabitedIsType,
dependent_pairEquality_alt
Latex:
\mforall{}[X,T:Type]. \mforall{}[P:T {}\mrightarrow{} X {}\mrightarrow{} \mBbbP{}]. \mforall{}[S:T {}\mrightarrow{} Type]. \mforall{}[Q:i:T {}\mrightarrow{} S[i] {}\mrightarrow{} X {}\mrightarrow{} \mBbbP{}].
stable-union(X;T;i,x.P[i;x]) \mequiv{} stable-union(X;i:T \mtimes{} S[i];p,x.Q[fst(p);snd(p);x])
supposing (\mforall{}x:X. \mforall{}i:T. \mforall{}s:S[i]. (Q[i;s;x] {}\mRightarrow{} (\mneg{}\mneg{}P[i;x])))
\mwedge{} (\mforall{}x:X. \mforall{}i:T. (P[i;x] {}\mRightarrow{} (\mneg{}\mneg{}(\mexists{}s:S[i]. Q[i;s;x]))))
Date html generated:
2020_05_19-PM-09_36_17
Last ObjectModification:
2019_10_24-AM-10_17_20
Theory : int_1
Home
Index