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 \in V ⟼ \{⟨t, u⟩ \| ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset 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 \in LSubSp (w)$
10	4	cv	$setvar u$
11	10 8	wcel	$wff u \in LSubSp (w)$
12	9 11	wa	$wff (t \in LSubSp (w) \land u \in LSubSp (w))$
13	5 10	wpss	$wff t \subset u$
14		vs	$setvar s$
15	14	cv	$setvar s$
16	5 15	wpss	$wff t \subset s$
17	15 10	wpss	$wff s \subset u$
18	16 17	wa	$wff (t \subset s \land s \subset u)$
19	18 14 8	wrex	$wff \exists s \in LSubSp (w) (t \subset s \land s \subset u)$
20	19	wn	$wff \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)$
21	13 20	wa	$wff (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u))$
22	12 21	wa	$wff ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)))$
23	22 3 4	copab	$class \{⟨t, u⟩ \| ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)))\}$
24	1 2 23	cmpt	$class (w \in V ⟼ \{⟨t, u⟩ \| ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)))\})$
25	0 24	wceq	$wff ⋖_{L} = (w \in V ⟼ \{⟨t, u⟩ \| ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)))\})$

Metamath Proof Explorer

Definition df-lcv

Detailed syntax breakdown