Nuprl Lemma : predicate-or_wf

[T,S:Type]. ∀[A:T ⟶ ℙ]. ∀[B:S ⟶ ℙ].  (predicate-or(A;B) ∈ (T × S) ⟶ ℙ)


Proof




Definitions occuring in Statement :  predicate-or: predicate-or(A;B) uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T predicate-or: predicate-or(A;B) prop:
Lemmas referenced :  or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality spreadEquality hypothesisEquality lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesis productEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[T,S:Type].  \mforall{}[A:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:S  {}\mrightarrow{}  \mBbbP{}].    (predicate-or(A;B)  \mmember{}  (T  \mtimes{}  S)  {}\mrightarrow{}  \mBbbP{})



Date html generated: 2016_05_14-PM-04_09_05
Last ObjectModification: 2015_12_26-PM-07_54_43

Theory : fan-theorem


Home Index