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

Metamath Proof Explorer

Theorem atpointN

Description: The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses ispoint.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ispoint.p ⊢ 𝑃 = ( Points ‘ 𝐾 )
Assertion atpointN ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴 ) → { 𝑋 } ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 ispoint.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 ispoint.p ⊢ 𝑃 = ( Points ‘ 𝐾 )
3 eqid ⊢ { 𝑋 } = { 𝑋 }
4 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
5 4 rspceeqv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ { 𝑋 } = { 𝑋 } ) → ∃ 𝑥 ∈ 𝐴 { 𝑋 } = { 𝑥 } )
6 3 5 mpan2 ⊢ ( 𝑋 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 { 𝑋 } = { 𝑥 } )
7 6 adantl ⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 { 𝑋 } = { 𝑥 } )
8 1 2 ispointN ⊢ ( 𝐾 ∈ 𝐷 → ( { 𝑋 } ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐴 { 𝑋 } = { 𝑥 } ) )
9 8 adantr ⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴 ) → ( { 𝑋 } ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐴 { 𝑋 } = { 𝑥 } ) )
10 7 9 mpbird ⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴 ) → { 𝑋 } ∈ 𝑃 )