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

Metamath Proof Explorer

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 ‘ 𝑘 ) ∧ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ 𝑠 ) ) = 𝑠 ) } )