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	1 2	lsatlss	$⊢ W \in LMod \to A \subseteq S$
14		rabss2	$⊢ A \subseteq S \to \{q \in A \| q \subseteq T\} \subseteq \{q \in S \| q \subseteq T\}$
15		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\}$
16	3 13 14 15	4syl	$⊢ φ \to ⋃ \{q \in A \| q \subseteq T\} \subseteq ⋃ \{q \in S \| q \subseteq T\}$
17		unimax	$⊢ T \in S \to ⋃ \{q \in S \| q \subseteq T\} = T$
18	4 17	syl	$⊢ φ \to ⋃ \{q \in S \| q \subseteq T\} = T$
19		eqid	$⊢ {Base}_{W} = {Base}_{W}$
20	19 1	lssss	$⊢ T \in S \to T \subseteq {Base}_{W}$
21	4 20	syl	$⊢ φ \to T \subseteq {Base}_{W}$
22	18 21	eqsstrd	$⊢ φ \to ⋃ \{q \in S \| q \subseteq T\} \subseteq {Base}_{W}$
23	16 22	sstrd	$⊢ φ \to ⋃ \{q \in A \| q \subseteq T\} \subseteq {Base}_{W}$
24		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\}$
25		eqid	$⊢ LSpan (W) = LSpan (W)$
26	19 25	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\})$
27	3 23 24 26	syl2an3an	$⊢ (φ \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\})$
28	1 25 2	lssats	$⊢ (W \in LMod \land U \in S) \to U = LSpan (W) (⋃ \{q \in A \| q \subseteq U\})$
29	3 5 28	syl2anc	$⊢ φ \to U = LSpan (W) (⋃ \{q \in A \| q \subseteq U\})$
30	29	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\})$
31	1 25 2	lssats	$⊢ (W \in LMod \land T \in S) \to T = LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
32	3 4 31	syl2anc	$⊢ φ \to T = LSpan (W) (⋃ \{q \in A \| q \subseteq T\})$
33	32	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\})$
34	27 30 33	3sstr4d	$⊢ (φ \land \{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\}) \to U \subseteq T$
35	34	ex	$⊢ φ \to (\{q \in A \| q \subseteq U\} \subseteq \{q \in A \| q \subseteq T\} \to U \subseteq T)$
36	12 35	biimtrrid	$⊢ φ \to (\forall q \in A (q \subseteq U \to q \subseteq T) \to U \subseteq T)$
37	11 36	biimtrrid	$⊢ φ \to (\forall q \in A \neg (q \subseteq U \land \neg q \subseteq T) \to U \subseteq T)$
38	9 37	mtod	$⊢ φ \to \neg \forall q \in A \neg (q \subseteq U \land \neg q \subseteq T)$
39		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)$
40	38 39	sylibr	$⊢ φ \to \exists q \in A (q \subseteq U \land \neg q \subseteq T)$

Metamath Proof Explorer

Theorem lpssat

Proof