Definition df-psubsp 39505

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

Assertion

Ref	Expression
df-psubsp	⊢ PSubSp = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))})

Distinct variable group:   𝑘,𝑝,𝑞,𝑟,𝑠

Detailed syntax breakdown of Definition df-psubsp

Step	Hyp	Ref	Expression
1		cpsubsp 39498	. 2 class PSubSp
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1539	. . . . . 6 class 𝑠
6	2	cv 1539	. . . . . . 7 class 𝑘
7		catm 39264	. . . . . . 7 class Atoms
8	6, 7	cfv 6561	. . . . . 6 class (Atoms‘𝑘)
9	5, 8	wss 3951	. . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10		vr	. . . . . . . . . . 11 setvar 𝑟
11	10	cv 1539	. . . . . . . . . 10 class 𝑟
12		vp	. . . . . . . . . . . 12 setvar 𝑝
13	12	cv 1539	. . . . . . . . . . 11 class 𝑝
14		vq	. . . . . . . . . . . 12 setvar 𝑞
15	14	cv 1539	. . . . . . . . . . 11 class 𝑞
16		cjn 18357	. . . . . . . . . . . 12 class join
17	6, 16	cfv 6561	. . . . . . . . . . 11 class (join‘𝑘)
18	13, 15, 17	co 7431	. . . . . . . . . 10 class (𝑝(join‘𝑘)𝑞)
19		cple 17304	. . . . . . . . . . 11 class le
20	6, 19	cfv 6561	. . . . . . . . . 10 class (le‘𝑘)
21	11, 18, 20	wbr 5143	. . . . . . . . 9 wff 𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞)
22	10, 4	wel 2109	. . . . . . . . 9 wff 𝑟 ∈ 𝑠
23	21, 22	wi 4	. . . . . . . 8 wff (𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
24	23, 10, 8	wral 3061	. . . . . . 7 wff ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
25	24, 14, 5	wral 3061	. . . . . 6 wff ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
26	25, 12, 5	wral 3061	. . . . 5 wff ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
27	9, 26	wa 395	. . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))
28	27, 4	cab 2714	. . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))}
29	2, 3, 28	cmpt 5225	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))})
30	1, 29	wceq 1540	1 wff PSubSp = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))})

This definition is referenced by:  psubspset  39746