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	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴 ) → { 𝑋 } ∈ 𝑃 )