This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 e. D -> ( X e. P <-> E. a e. 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 e. D -> P = { x | E. a e. A x = { a } } )
4 3 eleq2d 
 |-  ( K e. D -> ( X e. P <-> X e. { x | E. a e. A x = { a } } ) )
5 vsnex 
 |-  { a } e. _V
6 eleq1 
 |-  ( X = { a } -> ( X e. _V <-> { a } e. _V ) )
7 5 6 mpbiri 
 |-  ( X = { a } -> X e. _V )
8 7 rexlimivw 
 |-  ( E. a e. A X = { a } -> X e. _V )
9 eqeq1 
 |-  ( x = X -> ( x = { a } <-> X = { a } ) )
10 9 rexbidv 
 |-  ( x = X -> ( E. a e. A x = { a } <-> E. a e. A X = { a } ) )
11 8 10 elab3 
 |-  ( X e. { x | E. a e. A x = { a } } <-> E. a e. A X = { a } )
12 4 11 bitrdi 
 |-  ( K e. D -> ( X e. P <-> E. a e. A X = { a } ) )