pexmidlem7N

Description: Lemma for pexmidN . Contradict pexmidlem6N . (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	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 M \neq 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		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$
8		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$
9	8	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$
10		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$
11	3 4	sspadd2	$⊢ (K \in HL \land \{p\} \subseteq A \land X \subseteq A) \to \{p\} \subseteq X \underset{˙}{+} \{p\}$
12	7 9 10 11	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 \{p\} \subseteq X \underset{˙}{+} \{p\}$
13		vex	$⊢ p \in V$
14	13	snss	$⊢ p \in (X \underset{˙}{+} \{p\}) \leftrightarrow \{p\} \subseteq X \underset{˙}{+} \{p\}$
15	12 14	sylibr	$⊢ ((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 (X \underset{˙}{+} \{p\})$
16	15 6	eleqtrrdi	$⊢ ((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 M$
17	3 5	polssatN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
18	7 10 17	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{˙}{⊥} (X) \subseteq A$
19	3 4	sspadd1	$⊢ (K \in HL \land X \subseteq A \land \underset{˙}{⊥} (X) \subseteq A) \to X \subseteq X \underset{˙}{+} \underset{˙}{⊥} (X)$
20	7 10 18 19	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{˙}{+} \underset{˙}{⊥} (X)$
21		simpr3	$⊢ ((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 \neg p \in (X \underset{˙}{+} \underset{˙}{⊥} (X))$
22	20 21	ssneldd	$⊢ ((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 \neg p \in X$
23		nelne1	$⊢ (p \in M \land \neg p \in X) \to M \neq X$
24	16 22 23	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 M \neq X$

Metamath Proof Explorer

Theorem pexmidlem7N

Proof