Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
ispointN
Next ⟩
atpointN
Metamath Proof Explorer
Ascii
Unicode
Theorem
ispointN
Description:
The predicate "is a point".
(Contributed by
NM
, 2-Oct-2011)
(New usage is discouraged.)
Ref
Expression
Hypotheses
ispoint.a
⊢
A
=
Atoms
⁡
K
ispoint.p
⊢
P
=
Points
⁡
K
Assertion
ispointN
⊢
K
∈
D
→
X
∈
P
↔
∃
a
∈
A
X
=
a
Proof
Step
Hyp
Ref
Expression
1
ispoint.a
⊢
A
=
Atoms
⁡
K
2
ispoint.p
⊢
P
=
Points
⁡
K
3
1
2
pointsetN
⊢
K
∈
D
→
P
=
x
|
∃
a
∈
A
x
=
a
4
3
eleq2d
⊢
K
∈
D
→
X
∈
P
↔
X
∈
x
|
∃
a
∈
A
x
=
a
5
snex
⊢
a
∈
V
6
eleq1
⊢
X
=
a
→
X
∈
V
↔
a
∈
V
7
5
6
mpbiri
⊢
X
=
a
→
X
∈
V
8
7
rexlimivw
⊢
∃
a
∈
A
X
=
a
→
X
∈
V
9
eqeq1
⊢
x
=
X
→
x
=
a
↔
X
=
a
10
9
rexbidv
⊢
x
=
X
→
∃
a
∈
A
x
=
a
↔
∃
a
∈
A
X
=
a
11
8
10
elab3
⊢
X
∈
x
|
∃
a
∈
A
x
=
a
↔
∃
a
∈
A
X
=
a
12
4
11
bitrdi
⊢
K
∈
D
→
X
∈
P
↔
∃
a
∈
A
X
=
a