pexmidlem6N

Description: Lemma for pexmidN . (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pexmidlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	pexmidlem.a	$⊢ A = Atoms (K)$
	pexmidlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	pexmidlem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	pexmidlem.m	$⊢ M = X \underset{˙}{+} \{p\}$
Assertion	pexmidlem6N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to M = X$

Proof

Step	Hyp	Ref	Expression
1		pexmidlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		pexmidlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pexmidlem.a	$⊢ A = Atoms (K)$
4		pexmidlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		pexmidlem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		pexmidlem.m	$⊢ M = X \underset{˙}{+} \{p\}$
7	1 2 3 4 5 6	pexmidlem5N	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (X) \cap M = \emptyset$
8	7	3adantr1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (X) \cap M = \emptyset$
9	8	fveq2d	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) = \underset{˙}{⊥} (\emptyset)$
10		simpl1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to K \in HL$
11	3 5	pol0N	$⊢ K \in HL \to \underset{˙}{⊥} (\emptyset) = A$
12	10 11	syl	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\emptyset) = A$
13	9 12	eqtrd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) = A$
14	13	ineq1d	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) \cap M = A \cap M$
15		simpl2	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \subseteq A$
16		simpl3	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to p \in A$
17	16	snssd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \{p\} \subseteq A$
18	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land \{p\} \subseteq A) \to X \underset{˙}{+} \{p\} \subseteq A$
19	10 15 17 18	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \underset{˙}{+} \{p\} \subseteq A$
20	6 19	eqsstrid	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to M \subseteq A$
21	10 15 20	3jca	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to (K \in HL \land X \subseteq A \land M \subseteq A)$
22	3 4	sspadd1	$⊢ (K \in HL \land X \subseteq A \land \{p\} \subseteq A) \to X \subseteq X \underset{˙}{+} \{p\}$
23	10 15 17 22	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \subseteq X \underset{˙}{+} \{p\}$
24	23 6	sseqtrrdi	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \subseteq M$
25		simpr1	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
26		eqid	$⊢ PSubCl (K) = PSubCl (K)$
27	3 5 26	ispsubclN	$⊢ K \in HL \to (X \in PSubCl (K) \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$
28	10 27	syl	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to (X \in PSubCl (K) \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$
29	15 25 28	mpbir2and	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \in PSubCl (K)$
30	3 4 26	paddatclN	$⊢ (K \in HL \land X \in PSubCl (K) \land p \in A) \to X \underset{˙}{+} \{p\} \in PSubCl (K)$
31	10 29 16 30	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \underset{˙}{+} \{p\} \in PSubCl (K)$
32	6 31	eqeltrid	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to M \in PSubCl (K)$
33	5 26	psubcli2N	$⊢ (K \in HL \land M \in PSubCl (K)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (M)) = M$
34	10 32 33	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (M)) = M$
35	24 34	jca	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to (X \subseteq M \land \underset{˙}{⊥} (\underset{˙}{⊥} (M)) = M)$
36	3 5	poml4N	$⊢ (K \in HL \land X \subseteq A \land M \subseteq A) \to ((X \subseteq M \land \underset{˙}{⊥} (\underset{˙}{⊥} (M)) = M) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) \cap M = \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
37	21 35 36	sylc	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap M) \cap M = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
38		sseqin2	$⊢ M \subseteq A \leftrightarrow A \cap M = M$
39	20 38	sylib	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to A \cap M = M$
40	14 37 39	3eqtr3rd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to M = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
41	40 25	eqtrd	$⊢ ((K \in HL \land X \subseteq A \land p \in A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to M = X$

Metamath Proof Explorer

Theorem pexmidlem6N

Proof