Definition df-psubclN

Description: Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in Holland95 p. 223. (Contributed by NM, 23-Jan-2012)

	Ref	Expression
Assertion	df-psubclN	⊢ PSubCl = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpscN	⊢ PSubCl
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vs	⊢ 𝑠
4	3	cv	⊢ 𝑠
5		catm	⊢ Atoms
6	1	cv	⊢ 𝑘
7	6 5	cfv	⊢ ( Atoms ‘ 𝑘 )
8	4 7	wss	⊢ 𝑠 ⊆ ( Atoms ‘ 𝑘 )
9		cpolN	⊢ ⊥𝑃
10	6 9	cfv	⊢ ( ⊥𝑃 ‘ 𝑘 )
11	4 10	cfv	⊢ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 )
12	11 10	cfv	⊢ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) )
13	12 4	wceq	⊢ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠
14	8 13	wa	⊢ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 )
15	14 3	cab	⊢ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) }
16	1 2 15	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) } )
17	0 16	wceq	⊢ PSubCl = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) } )