Definition df-lcv 40056

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 𝐴( ⋖_L ‘𝑊)𝐵 is read "𝐵 covers 𝐴 " or "𝐴 is covered by 𝐵 " , and it means that 𝐵 is larger than 𝐴 and there is nothing in between. See lcvbr 40058 for binary relation. (df-cv 32874 analog.) (Contributed by NM, 7-Jan-2015.)

Assertion

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

Distinct variable group:   𝑡,𝑠,𝑢,𝑤

Detailed syntax breakdown of Definition df-lcv

Step	Hyp	Ref	Expression
1		clcv 40055	. 2 class ⋖L
2		vw	. . 3 setvar 𝑤
3		cvv 3451	. . 3 class V
4		vt	. . . . . . . 8 setvar 𝑡
5	4	cv 1569	. . . . . . 7 class 𝑡
6	2	cv 1569	. . . . . . . 8 class 𝑤
7		clss 21199	. . . . . . . 8 class LSubSp
8	6, 7	cfv 6537	. . . . . . 7 class (LSubSp‘𝑤)
9	5, 8	wcel 2145	. . . . . 6 wff 𝑡 ∈ (LSubSp‘𝑤)
10		vu	. . . . . . . 8 setvar 𝑢
11	10	cv 1569	. . . . . . 7 class 𝑢
12	11, 8	wcel 2145	. . . . . 6 wff 𝑢 ∈ (LSubSp‘𝑤)
13	9, 12	wa 401	. . . . 5 wff (𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤))
14	5, 11	wpss 3900	. . . . . 6 wff 𝑡 ⊊ 𝑢
15		vs	. . . . . . . . . . 11 setvar 𝑠
16	15	cv 1569	. . . . . . . . . 10 class 𝑠
17	5, 16	wpss 3900	. . . . . . . . 9 wff 𝑡 ⊊ 𝑠
18	16, 11	wpss 3900	. . . . . . . . 9 wff 𝑠 ⊊ 𝑢
19	17, 18	wa 401	. . . . . . . 8 wff (𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)
20	19, 15, 8	wrex 3087	. . . . . . 7 wff ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)
21	20	wn 3	. . . . . 6 wff ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)
22	14, 21	wa 401	. . . . 5 wff (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢))
23	13, 22	wa 401	. . . 4 wff ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))
24	23, 4, 10	copab 5167	. . 3 class {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))}
25	2, 3, 24	cmpt 5186	. 2 class (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})
26	1, 25	wceq 1570	1 wff ⋖L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡 ⊊ 𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢)))})

This definition is used by:  lcvfbr  40057