osumcllem10N

Description: Lemma for osumclN . Contradict osumcllem9N . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osumcllem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	osumcllem.j	$⊢ \underset{˙}{\lor} = join (K)$
	osumcllem.a	$⊢ A = Atoms (K)$
	osumcllem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	osumcllem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	osumcllem.c	$⊢ C = PSubCl (K)$
	osumcllem.m	$⊢ M = X \underset{˙}{+} \{p\}$
	osumcllem.u	$⊢ U = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
Assertion	osumcllem10N	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to M \neq X$

Proof

Step	Hyp	Ref	Expression
1		osumcllem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		osumcllem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		osumcllem.a	$⊢ A = Atoms (K)$
4		osumcllem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		osumcllem.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		osumcllem.c	$⊢ C = PSubCl (K)$
7		osumcllem.m	$⊢ M = X \underset{˙}{+} \{p\}$
8		osumcllem.u	$⊢ U = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
9		simp11	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to K \in HL$
10		simp2	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to p \in A$
11	10	snssd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to \{p\} \subseteq A$
12		simp12	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to X \subseteq A$
13	3 4	sspadd2	$⊢ (K \in HL \land \{p\} \subseteq A \land X \subseteq A) \to \{p\} \subseteq X \underset{˙}{+} \{p\}$
14	9 11 12 13	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to \{p\} \subseteq X \underset{˙}{+} \{p\}$
15		vex	$⊢ p \in V$
16	15	snss	$⊢ p \in (X \underset{˙}{+} \{p\}) \leftrightarrow \{p\} \subseteq X \underset{˙}{+} \{p\}$
17	14 16	sylibr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to p \in (X \underset{˙}{+} \{p\})$
18	17 7	eleqtrrdi	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to p \in M$
19	3 4	sspadd1	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \subseteq X \underset{˙}{+} Y$
20	19	3ad2ant1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to X \subseteq X \underset{˙}{+} Y$
21		simp3	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to \neg p \in (X \underset{˙}{+} Y)$
22	20 21	ssneldd	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to \neg p \in X$
23		nelne1	$⊢ (p \in M \land \neg p \in X) \to M \neq X$
24	18 22 23	syl2anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land p \in A \land \neg p \in (X \underset{˙}{+} Y)) \to M \neq X$

Metamath Proof Explorer

Theorem osumcllem10N

Proof