Nuprl Lemma : projective-plane-subtype-basic
ProjectivePlane ⊆r BasicProjectivePlane
Proof
Definitions occuring in Statement :
projective-plane: ProjectivePlane,
basic-projective-plane: BasicProjectivePlane,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
prop: ℙ,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
basic-projective-plane: BasicProjectivePlane,
projective-plane: ProjectivePlane,
member: t ∈ T,
subtype_rel: A ⊆r B
Lemmas referenced :
projective-plane_wf,
projective-plane-structure_subtype,
basic-pgeo-axioms_wf,
projective-plane-structure-complete_subtype
Rules used in proof :
isectElimination,
sqequalRule,
hypothesis,
extract_by_obid,
introduction,
applyEquality,
hypothesisEquality,
productElimination,
dependent_set_memberEquality,
cut,
rename,
thin,
setElimination,
sqequalHypSubstitution,
lambdaEquality,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
ProjectivePlane \msubseteq{}r BasicProjectivePlane
Date html generated:
2018_05_22-PM-00_41_14
Last ObjectModification:
2017_11_28-PM-04_19_46
Theory : euclidean!plane!geometry
Home
Index