Metamath Proof Explorer

Theorem lssnle

Description: Equivalent expressions for "not less than". ( chnlei analog.) (Contributed by NM, 10-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

		Ref	Expression
	Hypotheses	lssnle.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
		lssnle.t	$⊢ φ \to T \in SubGrp (G)$
		lssnle.u	$⊢ φ \to U \in SubGrp (G)$
	Assertion	lssnle	$⊢ φ \to (\neg U \subseteq T \leftrightarrow T \subset T \underset{˙}{\oplus} U)$

Proof

Step	Hyp	Ref	Expression
1		lssnle.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lssnle.t	$⊢ φ \to T \in SubGrp (G)$
3		lssnle.u	$⊢ φ \to U \in SubGrp (G)$
4	1	lsmss2b	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (U \subseteq T \leftrightarrow T \underset{˙}{\oplus} U = T)$
5	2 3 4	syl2anc	$⊢ φ \to (U \subseteq T \leftrightarrow T \underset{˙}{\oplus} U = T)$
6		eqcom	$⊢ T \underset{˙}{\oplus} U = T \leftrightarrow T = T \underset{˙}{\oplus} U$
7	5 6	bitrdi	$⊢ φ \to (U \subseteq T \leftrightarrow T = T \underset{˙}{\oplus} U)$
8	7	necon3bbid	$⊢ φ \to (\neg U \subseteq T \leftrightarrow T \neq T \underset{˙}{\oplus} U)$
9	1	lsmub1	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to T \subseteq T \underset{˙}{\oplus} U$
10	2 3 9	syl2anc	$⊢ φ \to T \subseteq T \underset{˙}{\oplus} U$
11		df-pss	$⊢ T \subset T \underset{˙}{\oplus} U \leftrightarrow (T \subseteq T \underset{˙}{\oplus} U \land T \neq T \underset{˙}{\oplus} U)$
12	11	baib	$⊢ T \subseteq T \underset{˙}{\oplus} U \to (T \subset T \underset{˙}{\oplus} U \leftrightarrow T \neq T \underset{˙}{\oplus} U)$
13	10 12	syl	$⊢ φ \to (T \subset T \underset{˙}{\oplus} U \leftrightarrow T \neq T \underset{˙}{\oplus} U)$
14	8 13	bitr4d	$⊢ φ \to (\neg U \subseteq T \leftrightarrow T \subset T \underset{˙}{\oplus} U)$