Definition df-lcv

Description: Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of PtakPulmannova p. 68. Ptak/Pulmannova's notation A ( W ) B is read " B covers A " or " A is covered by B " , and it means that B is larger than A and there is nothing in between. See lcvbr for binary relation. ( df-cv analog.) (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Assertion	df-lcv	⊢ ⋖L = ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clcv	⊢ ⋖L
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vt	⊢ 𝑡
4		vu	⊢ 𝑢
5	3	cv	⊢ 𝑡
6		clss	⊢ LSubSp
7	1	cv	⊢ 𝑤
8	7 6	cfv	⊢ ( LSubSp ‘ 𝑤 )
9	5 8	wcel	⊢ 𝑡 ∈ ( LSubSp ‘ 𝑤 )
10	4	cv	⊢ 𝑢
11	10 8	wcel	⊢ 𝑢 ∈ ( LSubSp ‘ 𝑤 )
12	9 11	wa	⊢ ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) )
13	5 10	wpss	⊢ 𝑡 ⊊ 𝑢
14		vs	⊢ 𝑠
15	14	cv	⊢ 𝑠
16	5 15	wpss	⊢ 𝑡 ⊊ 𝑠
17	15 10	wpss	⊢ 𝑠 ⊊ 𝑢
18	16 17	wa	⊢ ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 )
19	18 14 8	wrex	⊢ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 )
20	19	wn	⊢ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 )
21	13 20	wa	⊢ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) )
22	12 21	wa	⊢ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) )
23	22 3 4	copab	⊢ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) }
24	1 2 23	cmpt	⊢ ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )
25	0 24	wceq	⊢ ⋖L = ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡 ⊊ 𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )