Definition df-watsN

Description: Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" d . These are all atoms not in the polarity of { d } ) , which is the hyperplane determined by d . Definition of set W in Crawley p. 111. (Contributed by NM, 26-Jan-2012)

	Ref	Expression
Assertion	df-watsN	⊢ WAtoms = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwpointsN	⊢ WAtoms
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		catm	⊢ Atoms
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Atoms ‘ 𝑘 )
7		cpolN	⊢ ⊥𝑃
8	5 7	cfv	⊢ ( ⊥𝑃 ‘ 𝑘 )
9	3	cv	⊢ 𝑑
10	9	csn	⊢ { 𝑑 }
11	10 8	cfv	⊢ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } )
12	6 11	cdif	⊢ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) )
13	3 6 12	cmpt	⊢ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) )
14	1 2 13	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ) )
15	0 14	wceq	⊢ WAtoms = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ ( ( Atoms ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ) )