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