Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-psubsp Structured version   Visualization version   GIF version

Definition df-psubsp 35107
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
StepHypRef Expression
1 cpsubsp 35100 . 2 class PSubSp
2 vk . . 3 setvar 𝑘
3 cvv 3231 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1522 . . . . . 6 class 𝑠
62cv 1522 . . . . . . 7 class 𝑘
7 catm 34868 . . . . . . 7 class Atoms
86, 7cfv 5926 . . . . . 6 class (Atoms‘𝑘)
95, 8wss 3607 . . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10 vr . . . . . . . . . . 11 setvar 𝑟
1110cv 1522 . . . . . . . . . 10 class 𝑟
12 vp . . . . . . . . . . . 12 setvar 𝑝
1312cv 1522 . . . . . . . . . . 11 class 𝑝
14 vq . . . . . . . . . . . 12 setvar 𝑞
1514cv 1522 . . . . . . . . . . 11 class 𝑞
16 cjn 16991 . . . . . . . . . . . 12 class join
176, 16cfv 5926 . . . . . . . . . . 11 class (join‘𝑘)
1813, 15, 17co 6690 . . . . . . . . . 10 class (𝑝(join‘𝑘)𝑞)
19 cple 15995 . . . . . . . . . . 11 class le
206, 19cfv 5926 . . . . . . . . . 10 class (le‘𝑘)
2111, 18, 20wbr 4685 . . . . . . . . 9 wff 𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞)
2210, 4wel 2031 . . . . . . . . 9 wff 𝑟𝑠
2321, 22wi 4 . . . . . . . 8 wff (𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠)
2423, 10, 8wral 2941 . . . . . . 7 wff 𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠)
2524, 14, 5wral 2941 . . . . . 6 wff 𝑞𝑠𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠)
2625, 12, 5wral 2941 . . . . 5 wff 𝑝𝑠𝑞𝑠𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠)
279, 26wa 383 . . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝𝑠𝑞𝑠𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠))
2827, 4cab 2637 . . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝𝑠𝑞𝑠𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠))}
292, 3, 28cmpt 4762 . 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝𝑠𝑞𝑠𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠))})
301, 29wceq 1523 1 wff PSubSp = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ∀𝑝𝑠𝑞𝑠𝑟 ∈ (Atoms‘𝑘)(𝑟(le‘𝑘)(𝑝(join‘𝑘)𝑞) → 𝑟𝑠))})
Colors of variables: wff setvar class
This definition is referenced by:  psubspset  35348
  Copyright terms: Public domain W3C validator