Nuprl Lemma : or-quotient-true-subtype

P:ℙ(⇃(P ∨ P)) ⊆(⇃(P) ∨ ⇃P)))


Proof




Definitions occuring in Statement :  quotient: x,y:A//B[x; y] subtype_rel: A ⊆B prop: all: x:A. B[x] not: ¬A or: P ∨ Q true: True
Definitions unfolded in proof :  all: x:A. B[x] or: P ∨ Q uall: [x:A]. B[x] member: t ∈ T prop: uimplies: supposing a not: ¬A implies:  Q and: P ∧ Q false: False so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  disjoint-quotient_subtype not_wf and_wf true_wf equiv_rel_true
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalRule cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination productElimination independent_functionElimination voidElimination lambdaEquality unionEquality universeEquality

Latex:
\mforall{}P:\mBbbP{}.  (\00D9(P  \mvee{}  (\mneg{}P))  \msubseteq{}r  (\00D9(P)  \mvee{}  \00D9(\mneg{}P)))



Date html generated: 2016_05_14-AM-06_08_53
Last ObjectModification: 2015_12_26-AM-11_48_11

Theory : quot_1


Home Index