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 = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsubsp	⊢ PSubSp
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vs	⊢ 𝑠
4	3	cv	⊢ 𝑠
5		catm	⊢ Atoms
6	1	cv	⊢ 𝑘
7	6 5	cfv	⊢ ( Atoms ‘ 𝑘 )
8	4 7	wss	⊢ 𝑠 ⊆ ( Atoms ‘ 𝑘 )
9		vp	⊢ 𝑝
10		vq	⊢ 𝑞
11		vr	⊢ 𝑟
12	11	cv	⊢ 𝑟
13		cple	⊢ le
14	6 13	cfv	⊢ ( le ‘ 𝑘 )
15	9	cv	⊢ 𝑝
16		cjn	⊢ join
17	6 16	cfv	⊢ ( join ‘ 𝑘 )
18	10	cv	⊢ 𝑞
19	15 18 17	co	⊢ ( 𝑝 ( join ‘ 𝑘 ) 𝑞 )
20	12 19 14	wbr	⊢ 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 )
21	12 4	wcel	⊢ 𝑟 ∈ 𝑠
22	20 21	wi	⊢ ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 )
23	22 11 7	wral	⊢ ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 )
24	23 10 4	wral	⊢ ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 )
25	24 9 4	wral	⊢ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 )
26	8 25	wa	⊢ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) )
27	26 3	cab	⊢ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) }
28	1 2 27	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )
29	0 28	wceq	⊢ PSubSp = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )