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

Metamath Proof Explorer

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 ‘ 𝑘 ) ∖ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) ) )