pexmidlem8N

Description: Lemma for pexmidN . The contradiction of pexmidlem6N and pexmidlem7N shows that there can be no atom p that is not in X .+ ( ._|_X ) , which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidALT.a	$⊢ A = Atoms (K)$
	pexmidALT.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	pexmidALT.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	pexmidlem8N	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$

Proof

Step	Hyp	Ref	Expression
1		pexmidALT.a	$⊢ A = Atoms (K)$
2		pexmidALT.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		pexmidALT.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
4		nonconne	$⊢ \neg (X = X \land X \neq X)$
5		simpll	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to K \in HL$
6		simplr	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to X \subseteq A$
7	1 3	polssatN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
8	7	adantr	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to \underset{˙}{⊥} (X) \subseteq A$
9	1 2	paddssat	$⊢ (K \in HL \land X \subseteq A \land \underset{˙}{⊥} (X) \subseteq A) \to X \underset{˙}{+} \underset{˙}{⊥} (X) \subseteq A$
10	5 6 8 9	syl3anc	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to X \underset{˙}{+} \underset{˙}{⊥} (X) \subseteq A$
11		df-pss	$⊢ X \underset{˙}{+} \underset{˙}{⊥} (X) \subset A \leftrightarrow (X \underset{˙}{+} \underset{˙}{⊥} (X) \subseteq A \land X \underset{˙}{+} \underset{˙}{⊥} (X) \neq A)$
12		pssnel	$⊢ X \underset{˙}{+} \underset{˙}{⊥} (X) \subset A \to \exists p (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
13	11 12	sylbir	$⊢ (X \underset{˙}{+} \underset{˙}{⊥} (X) \subseteq A \land X \underset{˙}{+} \underset{˙}{⊥} (X) \neq A) \to \exists p (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
14		df-rex	$⊢ \exists p \in A \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)) \leftrightarrow \exists p (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))$
15	13 14	sylibr	$⊢ (X \underset{˙}{+} \underset{˙}{⊥} (X) \subseteq A \land X \underset{˙}{+} \underset{˙}{⊥} (X) \neq A) \to \exists p \in A \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
16		simplll	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to K \in HL$
17		simpllr	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \subseteq A$
18		simprl	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to p \in A$
19		simplrl	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
20		simplrr	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to X \neq \emptyset$
21		simprr	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
22		eqid	$⊢ \leq_{K} = \leq_{K}$
23		eqid	$⊢ join (K) = join (K)$
24		eqid	$⊢ X \underset{˙}{+} \{p\} = X \underset{˙}{+} \{p\}$
25	22 23 1 2 3 24	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 X \underset{˙}{+} \{p\} = X$
26	22 23 1 2 3 24	pexmidlem7N	$⊢ ((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\} \neq X$
27	25 26	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 \underset{˙}{+} \{p\} = X \land X \underset{˙}{+} \{p\} \neq X)$
28	16 17 18 19 20 21 27	syl33anc	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to (X \underset{˙}{+} \{p\} = X \land X \underset{˙}{+} \{p\} \neq X)$
29		nonconne	$⊢ \neg (X \underset{˙}{+} \{p\} = X \land X \underset{˙}{+} \{p\} \neq X)$
30	29 4	2false	$⊢ (X \underset{˙}{+} \{p\} = X \land X \underset{˙}{+} \{p\} \neq X) \leftrightarrow (X = X \land X \neq X)$
31	28 30	sylib	$⊢ (((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \land (p \in A \land \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)))) \to (X = X \land X \neq X)$
32	31	rexlimdvaa	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to (\exists p \in A \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X)) \to (X = X \land X \neq X))$
33	15 32	syl5	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to ((X \underset{˙}{+} \underset{˙}{⊥} (X) \subseteq A \land X \underset{˙}{+} \underset{˙}{⊥} (X) \neq A) \to (X = X \land X \neq X))$
34	10 33	mpand	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to (X \underset{˙}{+} \underset{˙}{⊥} (X) \neq A \to (X = X \land X \neq X))$
35	34	necon1bd	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to (\neg (X = X \land X \neq X) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A)$
36	4 35	mpi	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$

Metamath Proof Explorer

Theorem pexmidlem8N

Proof