lpssat

Description: Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. ( chpssati analog.) (Contributed by NM, 11-Jan-2015)

	Ref	Expression
Hypotheses	lpssat.s	$⊢ S = LSubSp (W)$
	lpssat.a	$⊢ A = LSAtoms (W)$
	lpssat.w	$⊢ φ \to W \in LMod$
	lpssat.t	$⊢ φ \to T \in S$
	lpssat.u	$⊢ φ \to U \in S$
	lpssat.l	$⊢ φ \to T \subset U$
Assertion	lpssat	$⊢ φ \to \exists q \in A (q \subseteq U \land \neg q \subseteq T)$

Proof

Step	Hyp	Ref	Expression
1		lpssat.s	$⊢ S = LSubSp (W)$
2		lpssat.a	$⊢ A = LSAtoms (W)$
3		lpssat.w	$⊢ φ \to W \in LMod$
4		lpssat.t	$⊢ φ \to T \in S$
5		lpssat.u	$⊢ φ \to U \in S$
6		lpssat.l	$⊢ φ \to T \subset U$
7		dfpss3	$⊢ T \subset U \leftrightarrow (T \subseteq U \land \neg U \subseteq T)$
8	7	simprbi	$⊢ T \subset U \to \neg U \subseteq T$
9	6 8	syl	$⊢ φ \to \neg U \subseteq T$
10		iman	$⊢ (q \subseteq U \to q \subseteq T) \leftrightarrow \neg (q \subseteq U \land \neg q \subseteq T)$
11	10	ralbii	$⊢ \forall q \in A (q \subseteq U \to q \subseteq T) \leftrightarrow \forall q \in A \neg (q \subseteq U \land \neg q \subseteq T)$
12		ss2rab	$⊢ \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\} \leftrightarrow \forall q \in A (q \subseteq U \to q \subseteq T)$
13	3	adantr	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to W \in LMod$
14	1 2	lsatlss	$⊢ W \in LMod \to A \subseteq S$
15		rabss2	$⊢ A \subseteq S \to \{q \in A \| q \subseteq T\} \subseteq \{q \in S \| q \subseteq T\}$
16		uniss	$⊢ \{q \in A \| q \subseteq T\} \subseteq \{q \in S \| q \subseteq T\} \to ⋃ \{q \in A \| q \subseteq T\} \subseteq ⋃ \{q \in S \| q \subseteq T\}$
17	3 14 15 16	4syl	$⊢ φ \to ⋃ \{q \in A \| q \subseteq T\} \subseteq ⋃ \{q \in S \| q \subseteq T\}$
18		unimax	$⊢ T \in S \to ⋃ \{q \in S \| q \subseteq T\} = T$
19	4 18	syl	$⊢ φ \to ⋃ \{q \in S \| q \subseteq T\} = T$
20		eqid	$⊢ {Base}_{W} = {Base}_{W}$
21	20 1	lssss	$⊢ T \in S \to T \subseteq {Base}_{W}$
22	4 21	syl	$⊢ φ \to T \subseteq {Base}_{W}$
23	19 22	eqsstrd	$⊢ φ \to ⋃ \{q \in S \| q \subseteq T\} \subseteq {Base}_{W}$
24	17 23	sstrd	$⊢ φ \to ⋃ \{q \in A \| q \subseteq T\} \subseteq {Base}_{W}$
25	24	adantr	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to ⋃ \{q \in A \| q \subseteq T\} \subseteq {Base}_{W}$
26		uniss	$⊢ \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\} \to ⋃ \{q \in A \| q \subseteq U\} \subseteq ⋃ \{q \in A \| q \subseteq T\}$
27	26	adantl	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to ⋃ \{q \in A \| q \subseteq U\} \subseteq ⋃ \{q \in A \| q \subseteq T\}$
28		eqid	$⊢ LSpan (W) = LSpan (W)$
29	20 28	lspss	$⊢ (W \in LMod \land ⋃ \{q \in A \| q \subseteq T\} \subseteq {Base}_{W} \land ⋃ \{q \in A \| q \subseteq U\} \subseteq ⋃ \{q \in A \| q \subseteq T\}) \to LSpan (W) (⋃ \{q \in A \| q \subseteq U\}) \subseteq LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
30	13 25 27 29	syl3anc	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to LSpan (W) (⋃ \{q \in A \| q \subseteq U\}) \subseteq LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
31	1 28 2	lssats	$⊢ (W \in LMod \land U \in S) \to U = LSpan (W) (⋃ \{q \in A \| q \subseteq U\})$
32	3 5 31	syl2anc	$⊢ φ \to U = LSpan (W) (⋃ \{q \in A \| q \subseteq U\})$
33	32	adantr	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to U = LSpan (W) (⋃ \{q \in A \| q \subseteq U\})$
34	1 28 2	lssats	$⊢ (W \in LMod \land T \in S) \to T = LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
35	3 4 34	syl2anc	$⊢ φ \to T = LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
36	35	adantr	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to T = LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
37	30 33 36	3sstr4d	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to U \subseteq T$
38	37	ex	$⊢ φ \to (\{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\} \to U \subseteq T)$
39	12 38	syl5bir	$⊢ φ \to (\forall q \in A (q \subseteq U \to q \subseteq T) \to U \subseteq T)$
40	11 39	syl5bir	$⊢ φ \to (\forall q \in A \neg (q \subseteq U \land \neg q \subseteq T) \to U \subseteq T)$
41	9 40	mtod	$⊢ φ \to \neg \forall q \in A \neg (q \subseteq U \land \neg q \subseteq T)$
42		dfrex2	$⊢ \exists q \in A (q \subseteq U \land \neg q \subseteq T) \leftrightarrow \neg \forall q \in A \neg (q \subseteq U \land \neg q \subseteq T)$
43	41 42	sylibr	$⊢ φ \to \exists q \in A (q \subseteq U \land \neg q \subseteq T)$

Metamath Proof Explorer

Theorem lpssat

Proof