Metamath Proof Explorer


Definition df-psubsp

Description: Define set of all projective subspaces. Based on definition of subspace in Holland95 p. 212. (Contributed by NM, 2-Oct-2011)

Ref Expression
Assertion df-psubsp PSubSp=kVs|sAtomskpsqsrAtomskrkpjoinkqrs

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsubsp classPSubSp
1 vk setvark
2 cvv classV
3 vs setvars
4 3 cv setvars
5 catm classAtoms
6 1 cv setvark
7 6 5 cfv classAtomsk
8 4 7 wss wffsAtomsk
9 vp setvarp
10 vq setvarq
11 vr setvarr
12 11 cv setvarr
13 cple classle
14 6 13 cfv classk
15 9 cv setvarp
16 cjn classjoin
17 6 16 cfv classjoink
18 10 cv setvarq
19 15 18 17 co classpjoinkq
20 12 19 14 wbr wffrkpjoinkq
21 12 4 wcel wffrs
22 20 21 wi wffrkpjoinkqrs
23 22 11 7 wral wffrAtomskrkpjoinkqrs
24 23 10 4 wral wffqsrAtomskrkpjoinkqrs
25 24 9 4 wral wffpsqsrAtomskrkpjoinkqrs
26 8 25 wa wffsAtomskpsqsrAtomskrkpjoinkqrs
27 26 3 cab classs|sAtomskpsqsrAtomskrkpjoinkqrs
28 1 2 27 cmpt classkVs|sAtomskpsqsrAtomskrkpjoinkqrs
29 0 28 wceq wffPSubSp=kVs|sAtomskpsqsrAtomskrkpjoinkqrs