Definition df-psubsp 37524

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 37517	. 2 class PSubSp
2		vk	. . 3 setvar 𝑘
3		cvv 3433	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1538	. . . . . 6 class 𝑠
6	2	cv 1538	. . . . . . 7 class 𝑘
7		catm 37284	. . . . . . 7 class Atoms
8	6, 7	cfv 6437	. . . . . 6 class (Atoms‘𝑘)
9	5, 8	wss 3888	. . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10		vr	. . . . . . . . . . 11 setvar 𝑟
11	10	cv 1538	. . . . . . . . . 10 class 𝑟
12		vp	. . . . . . . . . . . 12 setvar 𝑝
13	12	cv 1538	. . . . . . . . . . 11 class 𝑝
14		vq	. . . . . . . . . . . 12 setvar 𝑞
15	14	cv 1538	. . . . . . . . . . 11 class 𝑞
16		cjn 18038	. . . . . . . . . . . 12 class join
17	6, 16	cfv 6437	. . . . . . . . . . 11 class (join‘𝑘)
18	13, 15, 17	co 7284	. . . . . . . . . 10 class (𝑝(join‘𝑘)𝑞)
19		cple 16978	. . . . . . . . . . 11 class le
20	6, 19	cfv 6437	. . . . . . . . . 10 class (le‘𝑘)
21	11, 18, 20	wbr 5075	. . . . . . . . 9 wff 𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞)
22	10, 4	wel 2108	. . . . . . . . 9 wff 𝑟 ∈ 𝑠
23	21, 22	wi 4	. . . . . . . 8 wff (𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
24	23, 10, 8	wral 3065	. . . . . . 7 wff ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
25	24, 14, 5	wral 3065	. . . . . 6 wff ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
26	25, 12, 5	wral 3065	. . . . 5 wff ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠)
27	9, 26	wa 396	. . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))
28	27, 4	cab 2716	. . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))}
29	2, 3, 28	cmpt 5158	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))})
30	1, 29	wceq 1539	1 wff PSubSp = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟 ∈ 𝑠))})

This definition is referenced by:  psubspset  37765