Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
dalem-ccly
Next ⟩
dalem-ddly
Metamath Proof Explorer
Ascii
Unicode
Theorem
dalem-ccly
Description:
Lemma for
dath
. Frequently-used utility lemma.
(Contributed by
NM
, 15-Aug-2012)
Ref
Expression
Hypothesis
da.ps0
⊢
ψ
↔
c
∈
A
∧
d
∈
A
∧
¬
c
≤
˙
Y
∧
d
≠
c
∧
¬
d
≤
˙
Y
∧
C
≤
˙
c
∨
˙
d
Assertion
dalem-ccly
⊢
ψ
→
¬
c
≤
˙
Y
Proof
Step
Hyp
Ref
Expression
1
da.ps0
⊢
ψ
↔
c
∈
A
∧
d
∈
A
∧
¬
c
≤
˙
Y
∧
d
≠
c
∧
¬
d
≤
˙
Y
∧
C
≤
˙
c
∨
˙
d
2
1
simp2bi
⊢
ψ
→
¬
c
≤
˙
Y