This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑘 ∈ 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 ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )