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 = k ∈ V ⟼ s | s ⊆ Atoms ⁡ k ∧ ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s = s

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpscN class PSubCl
1 vk setvar k
2 cvv class V
3 vs setvar s
4 3 cv setvar s
5 catm class Atoms
6 1 cv setvar k
7 6 5 cfv class Atoms ⁡ k
8 4 7 wss wff s ⊆ Atoms ⁡ k
9 cpolN class ⊥ 𝑃
10 6 9 cfv class ⊥ 𝑃 ⁡ k
11 4 10 cfv class ⊥ 𝑃 ⁡ k ⁡ s
12 11 10 cfv class ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s
13 12 4 wceq wff ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s = s
14 8 13 wa wff s ⊆ Atoms ⁡ k ∧ ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s = s
15 14 3 cab class s | s ⊆ Atoms ⁡ k ∧ ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s = s
16 1 2 15 cmpt class k ∈ V ⟼ s | s ⊆ Atoms ⁡ k ∧ ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s = s
17 0 16 wceq wff PSubCl = k ∈ V ⟼ s | s ⊆ Atoms ⁡ k ∧ ⊥ 𝑃 ⁡ k ⁡ ⊥ 𝑃 ⁡ k ⁡ s = s