Theorem pointsetN

Description: The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pointset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pointset.p	⊢ 𝑃 = ( Points ‘ 𝐾 )
Assertion	pointsetN	⊢ ( 𝐾 ∈ 𝐵 → 𝑃 = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )

Proof

Step	Hyp	Ref	Expression
1		pointset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pointset.p	⊢ 𝑃 = ( Points ‘ 𝐾 )
3		elex	⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
4		fveq2	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
5	4 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
6	5	rexeqdv	⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑎 ∈ ( Atoms ‘ 𝑘 ) 𝑝 = { 𝑎 } ↔ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } ) )
7	6	abbidv	⊢ ( 𝑘 = 𝐾 → { 𝑝 ∣ ∃ 𝑎 ∈ ( Atoms ‘ 𝑘 ) 𝑝 = { 𝑎 } } = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )
8		df-pointsN	⊢ Points = ( 𝑘 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ ( Atoms ‘ 𝑘 ) 𝑝 = { 𝑎 } } )
9	1	fvexi	⊢ 𝐴 ∈ V
10	9	abrexex	⊢ { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } ∈ V
11	7 8 10	fvmpt	⊢ ( 𝐾 ∈ V → ( Points ‘ 𝐾 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )
12	2 11	syl5eq	⊢ ( 𝐾 ∈ V → 𝑃 = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )
13	3 12	syl	⊢ ( 𝐾 ∈ 𝐵 → 𝑃 = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )