Metamath Proof Explorer

Theorem lcvbr2

Description: The covers relation for a left vector space (or a left module). ( cvbr2 analog.) (Contributed by NM, 9-Jan-2015)

		Ref	Expression
	Hypotheses	lcvfbr.s	$⊢ S = LSubSp (W)$
		lcvfbr.c	$⊢ C = ⋖_{L} (W)$
		lcvfbr.w	$⊢ φ \to W \in X$
		lcvfbr.t	$⊢ φ \to T \in S$
		lcvfbr.u	$⊢ φ \to U \in S$
	Assertion	lcvbr2	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \forall s \in S ((T \subset s \land s \subseteq U) \to s = U)))$

Proof

Step	Hyp	Ref	Expression
1		lcvfbr.s	$⊢ S = LSubSp (W)$
2		lcvfbr.c	$⊢ C = ⋖_{L} (W)$
3		lcvfbr.w	$⊢ φ \to W \in X$
4		lcvfbr.t	$⊢ φ \to T \in S$
5		lcvfbr.u	$⊢ φ \to U \in S$
6	1 2 3 4 5	lcvbr	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \neg \exists s \in S (T \subset s \land s \subset U)))$
7		iman	$⊢ ((T \subset s \land s \subseteq U) \to s = U) \leftrightarrow \neg ((T \subset s \land s \subseteq U) \land \neg s = U)$
8		anass	$⊢ ((T \subset s \land s \subseteq U) \land \neg s = U) \leftrightarrow (T \subset s \land (s \subseteq U \land \neg s = U))$
9		dfpss2	$⊢ s \subset U \leftrightarrow (s \subseteq U \land \neg s = U)$
10	9	anbi2i	$⊢ (T \subset s \land s \subset U) \leftrightarrow (T \subset s \land (s \subseteq U \land \neg s = U))$
11	8 10	bitr4i	$⊢ ((T \subset s \land s \subseteq U) \land \neg s = U) \leftrightarrow (T \subset s \land s \subset U)$
12	7 11	xchbinx	$⊢ ((T \subset s \land s \subseteq U) \to s = U) \leftrightarrow \neg (T \subset s \land s \subset U)$
13	12	ralbii	$⊢ \forall s \in S ((T \subset s \land s \subseteq U) \to s = U) \leftrightarrow \forall s \in S \neg (T \subset s \land s \subset U)$
14		ralnex	$⊢ \forall s \in S \neg (T \subset s \land s \subset U) \leftrightarrow \neg \exists s \in S (T \subset s \land s \subset U)$
15	13 14	bitri	$⊢ \forall s \in S ((T \subset s \land s \subseteq U) \to s = U) \leftrightarrow \neg \exists s \in S (T \subset s \land s \subset U)$
16	15	anbi2i	$⊢ (T \subset U \land \forall s \in S ((T \subset s \land s \subseteq U) \to s = U)) \leftrightarrow (T \subset U \land \neg \exists s \in S (T \subset s \land s \subset U))$
17	6 16	syl6bbr	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \forall s \in S ((T \subset s \land s \subseteq U) \to s = U)))$