Metamath Proof Explorer

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 = w ∈ V ⟼ t u | t ∈ LSubSp ⁡ w ∧ u ∈ LSubSp ⁡ w ∧ t ⊂ u ∧ ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcv class ⋖ L
1 vw setvar w
2 cvv class V
3 vt setvar t
4 vu setvar u
5 3 cv setvar t
6 clss class LSubSp
7 1 cv setvar w
8 7 6 cfv class LSubSp ⁡ w
9 5 8 wcel wff t ∈ LSubSp ⁡ w
10 4 cv setvar u
11 10 8 wcel wff u ∈ LSubSp ⁡ w
12 9 11 wa wff t ∈ LSubSp ⁡ w ∧ u ∈ LSubSp ⁡ w
13 5 10 wpss wff t ⊂ u
14 vs setvar s
15 14 cv setvar s
16 5 15 wpss wff t ⊂ s
17 15 10 wpss wff s ⊂ u
18 16 17 wa wff t ⊂ s ∧ s ⊂ u
19 18 14 8 wrex wff ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u
20 19 wn wff ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u
21 13 20 wa wff t ⊂ u ∧ ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u
22 12 21 wa wff t ∈ LSubSp ⁡ w ∧ u ∈ LSubSp ⁡ w ∧ t ⊂ u ∧ ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u
23 22 3 4 copab class t u | t ∈ LSubSp ⁡ w ∧ u ∈ LSubSp ⁡ w ∧ t ⊂ u ∧ ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u
24 1 2 23 cmpt class w ∈ V ⟼ t u | t ∈ LSubSp ⁡ w ∧ u ∈ LSubSp ⁡ w ∧ t ⊂ u ∧ ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u
25 0 24 wceq wff ⋖ L = w ∈ V ⟼ t u | t ∈ LSubSp ⁡ w ∧ u ∈ LSubSp ⁡ w ∧ t ⊂ u ∧ ¬ ∃ s ∈ LSubSp ⁡ w t ⊂ s ∧ s ⊂ u