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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ispoint.p ⊢ 𝑃 = ( Points ‘ 𝐾 )
Assertion ispointN ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝐴 𝑋 = { 𝑎 } ) )

Proof

Step Hyp Ref Expression
1 ispoint.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 ispoint.p ⊢ 𝑃 = ( Points ‘ 𝐾 )
3 1 2 pointsetN ⊢ ( 𝐾 ∈ 𝐷 → 𝑃 = { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = { 𝑎 } } )
4 3 eleq2d ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑃 ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = { 𝑎 } } ) )
5 vsnex ⊢ { 𝑎 } ∈ V
6 eleq1 ⊢ ( 𝑋 = { 𝑎 } → ( 𝑋 ∈ V ↔ { 𝑎 } ∈ V ) )
7 5 6 mpbiri ⊢ ( 𝑋 = { 𝑎 } → 𝑋 ∈ V )
8 7 rexlimivw ⊢ ( ∃ 𝑎 ∈ 𝐴 𝑋 = { 𝑎 } → 𝑋 ∈ V )
9 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = { 𝑎 } ↔ 𝑋 = { 𝑎 } ) )
10 9 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑎 ∈ 𝐴 𝑥 = { 𝑎 } ↔ ∃ 𝑎 ∈ 𝐴 𝑋 = { 𝑎 } ) )
11 8 10 elab3 ⊢ ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = { 𝑎 } } ↔ ∃ 𝑎 ∈ 𝐴 𝑋 = { 𝑎 } )
12 4 11 bitrdi ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝐴 𝑋 = { 𝑎 } ) )