osumcllem4N

Description: Lemma for osumclN . (Contributed by NM, 24-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	osumcllem4N	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to q \neq r$

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		n0i	$⊢ r \in (X \cap Y) \to \neg X \cap Y = \emptyset$
10		incom	$⊢ X \cap Y = Y \cap X$
11		sslin	$⊢ X \subseteq \underset{˙}{⊥} (Y) \to Y \cap X \subseteq Y \cap \underset{˙}{⊥} (Y)$
12	11	3ad2ant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \cap X \subseteq Y \cap \underset{˙}{⊥} (Y)$
13	10 12	eqsstrid	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to X \cap Y \subseteq Y \cap \underset{˙}{⊥} (Y)$
14	3 5	pnonsingN	$⊢ (K \in HL \land Y \subseteq A) \to Y \cap \underset{˙}{⊥} (Y) = \emptyset$
15	14	3adant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \cap \underset{˙}{⊥} (Y) = \emptyset$
16	13 15	sseqtrd	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to X \cap Y \subseteq \emptyset$
17		ss0b	$⊢ X \cap Y \subseteq \emptyset \leftrightarrow X \cap Y = \emptyset$
18	16 17	sylib	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to X \cap Y = \emptyset$
19	18	adantr	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to X \cap Y = \emptyset$
20	9 19	nsyl3	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to \neg r \in (X \cap Y)$
21		simprr	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to q \in Y$
22		eleq1w	$⊢ q = r \to (q \in Y \leftrightarrow r \in Y)$
23	21 22	syl5ibcom	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to (q = r \to r \in Y)$
24		simprl	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to r \in X$
25	23 24	jctild	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to (q = r \to (r \in X \land r \in Y))$
26		elin	$⊢ r \in (X \cap Y) \leftrightarrow (r \in X \land r \in Y)$
27	25 26	imbitrrdi	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to (q = r \to r \in (X \cap Y))$
28	27	necon3bd	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to (\neg r \in (X \cap Y) \to q \neq r)$
29	20 28	mpd	$⊢ ((K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \land (r \in X \land q \in Y)) \to q \neq r$

Metamath Proof Explorer

Theorem osumcllem4N

Proof